internlm/Lean-Github huggingface dataset:
Theorem: SciLean.HAdd.hAdd.arg_a1.Diffeomorphism_rule
Proof 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.9828
inst✝⁵ : Vec K Z
W : Type ?u.9839
inst✝⁴ : Vec K W
ι : Type ?u.9850
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.9877
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
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.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.9828
inst✝⁵ : Vec K Z
W : Type ?u.9839
inst✝⁴ : Vec K W
ι : Type ?u.9850
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.9877
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.HAdd.hAdd.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.9828
inst✝⁵ : Vec K Z
W : Type ?u.9839
inst✝⁴ : Vec K W
ι : Type ?u.9850
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.9877
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.9828
inst✝⁵ : Vec K Z
W : Type ?u.9839
inst✝⁴ : Vec K W
ι : Type ?u.9850
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.9877
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.HAdd.hAdd.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.9828
inst✝⁵ : Vec K Z
W : Type ?u.9839
inst✝⁴ : Vec K W
ι : Type ?u.9850
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.9877
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.HSub.hSub.arg_a0.Diffeomorphism_rule
Proof 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
Proof 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
Theorem: SciLean.HSub.hSub.arg_a0.Diffeomorphism_rule
Proof 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
Proof 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)
Theorem: SciLean.HSub.hSub.arg_a0.Diffeomorphism_rule
Proof 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
Proof 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)
Theorem: SciLean.HSub.hSub.arg_a0.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.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
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.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)
Theorem: SciLean.HSub.hSub.arg_a0.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.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
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0.Diffeomorphism_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0.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.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
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0.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.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
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.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
Theorem: SciLean.HSub.hSub.arg_a0.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.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
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule
Proof 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
Proof 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
Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule
Proof 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
Proof 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)
Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule
Proof 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
Proof 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)
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

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
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 (cderiv K (fun x => y - f x) x)
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; fun_prop
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a1.Diffeomorphism_rule
Proof 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
Proof state after:
no goals