Theorem: SciLean.Function.invFun.arg_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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
⊢ (cderiv K fun x => invFun f (g x)) = fun x dx =>
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K (fun x => invFun f (g x)) x dx =
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K (fun x => invFun f (g x)) x dx =
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    dy
Tactic:
have H : (cderiv K (f ∘ invFun f) (g x))
         =
         id := by simp[show (f ∘ Function.invFun f) = id from sorry_proof]; unfold id; 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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
H : cderiv K (f ∘ invFun f) (g x) = id
⊢ cderiv K (fun x => invFun f (g x)) x dx =
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
H : cderiv K (f ∘ invFun f) (g x) = id
⊢ cderiv K (fun x => invFun f (g x)) x dx =
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    dy
Tactic:
have q : cderiv K f (invFun f (g x)) (cderiv K (fun x => invFun f (g x)) x dx) = cderiv K g x dx := sorry_proof
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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
H : cderiv K (f ∘ invFun f) (g x) = id
q : cderiv K f (invFun f (g x)) (cderiv K (fun x => invFun f (g x)) x dx) = cderiv K g x dx
⊢ cderiv K (fun x => invFun f (g x)) x dx =
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
H : cderiv K (f ∘ invFun f) (g x) = id
q : cderiv K f (invFun f (g x)) (cderiv K (fun x => invFun f (g x)) x dx) = cderiv K g x dx
⊢ cderiv K (fun x => invFun f (g x)) x dx =
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K (f ∘ invFun f) (g x) = id
Tactic:
simp[show (f ∘ Function.invFun f) = id from sorry_proof]
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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K id (g x) = id

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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K id (g x) = id
Tactic:
unfold id
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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K (fun a => a) (g x) = fun a => a

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.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K (fun a => a) (g x) = fun a => a
Tactic:
fun_trans
State after:
no goals