simp[ParametricInverseAt,arrayTypeCont]
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
⊢ let u := ∇ f 0;
  let dec := planeDecomposition u ⋯;
  ParametricInverseAt f c (fun x y t => dec (t, y)) (fun x x => (c - f 0) / ‖u‖₂[R]) fun x => ⊤
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