have : ‖(<∂ f 0).2 1‖₂[R] ≠ 0 := sorry_proof
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
this : ‖(<∂ f 0).2 1‖₂[R] ≠ 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c