Lean proof layout: totally umbilic surface ⇒ plane or sphere, with fderiv partials

Structure that worked (X : ℝ×ℝ → EuclideanSpace ℝ (Fin 3), C³, Xᵤ×Xᵥ ≠ 0 everywhere): (1) unit normal n is C² via ((hw.norm ℝ hreg).inv _).smul hw; (2) a tangent vector is determined by its inner products with Xᵤ, Xᵥ: apply the decomposition (EG-F²)z = ⟪z,w⟫w (z ⟂ Xᵤ,Xᵥ) to z = P - Q; so Weingarten + umbilic give nᵤ = -k Xᵤ, nᵥ = -k Xᵥ with k := L/E; (3) Schwarz for n gives kᵥXᵤ = kᵤXᵥ (cancel the k Xᵤᵥ terms with add_right_cancel), and independence follows by crossing both sides with Xᵥ resp. Xᵤ; (4) is_const_of_fderiv_eq_zero on ℝ×ℝ after proving fderiv f q = 0 from the two partials via ContinuousLinearMap.ext and x = x.1•(1,0)+x.2•(0,1); (5) k=0: ⟪X, n₀⟫ constant; k≠0: X + k⁻¹ n constant. Gotchas: rw [hkc] with hkc : ∀ q, k q = k 0 can rewrite k 0 itself (give the argument); DifferentiableAt.const_smul/.smul (differentiableAt_const _) produce Pi-form functions, so use by fun_prop for fun q ↦ c • n q; fderiv_fun_smul hc hf matches lambda products directly.