internlm/Lean-Github huggingface dataset:
Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule
Proof state before:
case differentiable
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.16406
inst✝⁵ : Vec K Z
W : Type ?u.16417
inst✝⁴ : Vec K W
ι : Type ?u.16428
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.16455
inst✝ : (i : ι) → Vec K (E i)
y : Y
f : X → Y
hf : Diffeomorphism K f
bijective✝ : Function.Bijective f
differentiable✝ : CDifferentiable K f
locally_diffeo✝ : ∀ (x : X), Function.Bijective (cderiv K f x)
⊢ CDifferentiable K fun x => y - f x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule
Proof state before:
case locally_diffeo
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.16406
inst✝⁵ : Vec K Z
W : Type ?u.16417
inst✝⁴ : Vec K W
ι : Type ?u.16428
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.16455
inst✝ : (i : ι) → Vec K (E i)
y : Y
f : X → Y
hf : Diffeomorphism K f
bijective✝ : Function.Bijective f
differentiable✝ : CDifferentiable K f
locally_diffeo✝ : ∀ (x : X), Function.Bijective (cderiv K f x)
⊢ ∀ (x : X), Function.Bijective (cderiv K (fun x => y - f x) x)
Tactic:
fun_trans
Proof state after:
case locally_diffeo
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.16406
inst✝⁵ : Vec K Z
W : Type ?u.16417
inst✝⁴ : Vec K W
ι : Type ?u.16428
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.16455
inst✝ : (i : ι) → Vec K (E i)
y : Y
f : X → Y
hf : Diffeomorphism K f
bijective✝ : Function.Bijective f
differentiable✝ : CDifferentiable K f
locally_diffeo✝ : ∀ (x : X), Function.Bijective (cderiv K f x)
⊢ ∀ (x : X), Function.Bijective fun dx => -cderiv K (fun x => f x) x dx
Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule
Proof state before:
case locally_diffeo
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.16406
inst✝⁵ : Vec K Z
W : Type ?u.16417
inst✝⁴ : Vec K W
ι : Type ?u.16428
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.16455
inst✝ : (i : ι) → Vec K (E i)
y : Y
f : X → Y
hf : Diffeomorphism K f
bijective✝ : Function.Bijective f
differentiable✝ : CDifferentiable K f
locally_diffeo✝ : ∀ (x : X), Function.Bijective (cderiv K f x)
⊢ ∀ (x : X), Function.Bijective fun dx => -cderiv K (fun x => f x) x dx
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Function.invFun.arg_a1.cderiv_rule
Proof 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
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
⊢ 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
Theorem: SciLean.Function.invFun.arg_a1.cderiv_rule
Proof 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
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
⊢ 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
Theorem: SciLean.Function.invFun.arg_a1.cderiv_rule
Proof 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
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
Theorem: SciLean.Function.invFun.arg_a1.cderiv_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.Function.invFun.arg_a1.cderiv_rule
Proof 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]
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
Theorem: SciLean.Function.invFun.arg_a1.cderiv_rule
Proof 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
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 (fun a => a) (g x) = fun a => a
Theorem: SciLean.Function.invFun.arg_a1.cderiv_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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
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.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
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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
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.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
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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)]
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.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
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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]
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.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
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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
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.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)
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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]
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.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
Theorem: SciLean.Function.invFun.arg_f_a1.cderiv_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.Function.invFun.arg_f.cderiv_rule'
Proof 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
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.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
Theorem: SciLean.Function.invFun.arg_f.cderiv_rule'
Proof 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
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.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
Theorem: SciLean.Function.invFun.arg_f.cderiv_rule'
Proof 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)]
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.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