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✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
⊢ let u := ∇ f 0;
  let dec := planeDecomposition u hn;
  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✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
⊢ ∀ (x₁ : DataArrayN R (Fin n)), f ((planeDecomposition (∇ f 0) hn) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c