Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule (SciLean/Core/FunctionPropositions/Diffeomorphism.lean)

State before:
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
⊢ Diffeomorphism K fun x => y - f x
Tactic:
have ⟨_,_,_⟩ := hf
State after:
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)
⊢ Diffeomorphism K fun x => y - f x

State before:
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)
⊢ Diffeomorphism K fun x => y - f x
Tactic:
constructor
State after:
case bijective
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)
⊢ Function.Bijective fun x => y - f x

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

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)

State before:
case bijective
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)
⊢ Function.Bijective fun x => y - f x

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

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_prop
State after:
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

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)

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

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_prop
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 (cderiv K (fun x => y - f x) x)

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; fun_prop
State after:
no goals

State before:
case bijective
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)
⊢ Function.Bijective fun x => y - f x
Tactic:
fun_prop
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals