Theorem: SciLean.Function.invFun.arg_f.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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
⊢ (cderiv K fun x => invFun (f x) z) = fun x dx =>
    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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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) z) x dx =
    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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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) z) x dx =
    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)) <| z)
         =
         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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx =
    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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx =
    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) z) 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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - 0 =
    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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - 0 =
    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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) 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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) 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:
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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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)) z = 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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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) z) x dx = 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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : 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) z) x dx = 0
Tactic:
fun_trans
State after:
no goals