fun_trans [scalarGradient,planeDecomposition_orthogonal_dir]
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✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin n)),
    (fun x => ⟪∇ f 0, x⟫_R + f 0)
        ((planeDecomposition (∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)) hn)
          ((c - (fun x => ⟪∇ f 0, x⟫_R + f 0) 0) / ‖∇ (x:=0), (⟪∇ f 0, x⟫_R + 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✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
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