Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule (SciLean/Core/FunctionPropositions/Diffeomorphism.lean)

State before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
⊢ (cderiv K fun x z => invFun (f x) z) = fun x dx z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Tactic:
funext x dx
State after:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ cderiv K (fun x z => invFun (f x) z) x dx = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy

State before:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ cderiv K (fun x z => invFun (f x) z) x dx = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Tactic:
have H : ((cderiv K (fun x => invFun (f x) ∘ (f x)) x dx) ∘ (invFun (f x)))
         =
         0 := by simp[invFun_comp (hf _).1.1]; fun_trans
State after:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x z => invFun (f x) z) x dx = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy

State before:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x z => invFun (f x) z) x dx = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Tactic:
rw[← sub_zero (cderiv K (fun x => Function.invFun (f x)) x dx)]
State after:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - 0 = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy

State before:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - 0 = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Tactic:
rw[← H]
State after:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy

State before:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = fun z =>
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Tactic:
fun_trans
State after:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = fun z =>
    -invFun (cderiv K (f x) (invFun (f x) (f x (invFun (f x) z)))) (cderiv K (fun x' => f x' (invFun (f x) z)) x dx)

State before:
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = fun z =>
    -invFun (cderiv K (f x) (invFun (f x) (f x (invFun (f x) z)))) (cderiv K (fun x' => f x' (invFun (f x) z)) x dx)
Tactic:
sorry_proof
State after:
no goals

State before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = 0
Tactic:
simp[invFun_comp (hf _).1.1]
State after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ cderiv K (fun x => id) x dx ∘ invFun (f x) = 0

State before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ cderiv K (fun x => id) x dx ∘ invFun (f x) = 0
Tactic:
fun_trans
State after:
no goals