have h : f = fun x => ⟪(∇ f 0), x⟫ + f 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
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))), f ((planeDecomposition (∇ f 0) ⋯) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = 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
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))), f ((planeDecomposition (∇ f 0) ⋯) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c