Theorem: SciLean.parametric_inverse_affine (SciLean/Core/Integral/PlaneDecomposition.lean)

State before:
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 => ⊤
Tactic:
simp[ParametricInverseAt,arrayTypeCont]
State after:
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

State before:
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
Tactic:
have h : f = fun x => ⟪(∇ f 0), x⟫ + f 0 := sorry_proof
State after:
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)), f ((planeDecomposition (∇ f 0) hn) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c

State before:
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)), f ((planeDecomposition (∇ f 0) hn) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Tactic:
rw[h]
State after:
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

State before:
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
Tactic:
fun_trans [scalarGradient,planeDecomposition_orthogonal_dir]
State after:
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

State before:
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
Tactic:
have : ‖(<∂ f 0).2 1‖₂[R] ≠ 0 := sorry_proof
State after:
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
this : ‖(<∂ f 0).2 1‖₂[R] ≠ 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c

State before:
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
this : ‖(<∂ f 0).2 1‖₂[R] ≠ 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Tactic:
field_simp
State after:
no goals