Theorem: SciLean.HSub.hSub.arg_a0.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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
hf : Diffeomorphism K f
⊢ Diffeomorphism K fun x => f x - y
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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y

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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y
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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y

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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y

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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y) 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y

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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y

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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y) 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y

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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y) 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y

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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y) 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y) 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y) 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y
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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y
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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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 => f x - y) 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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.13361
inst✝⁵ : Vec K Z
W : Type ?u.13372
inst✝⁴ : Vec K W
ι : Type ?u.13383
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13410
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : 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