internlm/Lean-Github huggingface dataset:
Theorem: SciLean.fwdDeriv.Inner.inner.arg_a0a1.fwdDeriv_rule
Proof state before:
K : Type ?u.132059
inst✝¹¹ : RCLike K
X✝ : Type ?u.132065
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.132078
inst✝⁹ : Vec K Y✝
Z : Type ?u.132089
inst✝⁸ : Vec K Z
W : Type ?u.132100
inst✝⁷ : Vec K W
ι : Type ?u.132111
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.132138
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : CDifferentiable R f
hg : CDifferentiable R g
⊢ (fwdDeriv R fun x => ⟪f x, g x⟫_R) = fun x dx =>
    let y₁dy₁ := fwdDeriv R f x dx;
    let y₂dy₂ := fwdDeriv R g x dx;
    (⟪y₁dy₁.1, y₂dy₂.1⟫_R, ⟪y₁dy₁.2, y₂dy₂.1⟫_R + ⟪y₁dy₁.1, y₂dy₂.2⟫_R)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type ?u.132059
inst✝¹¹ : RCLike K
X✝ : Type ?u.132065
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.132078
inst✝⁹ : Vec K Y✝
Z : Type ?u.132089
inst✝⁸ : Vec K Z
W : Type ?u.132100
inst✝⁷ : Vec K W
ι : Type ?u.132111
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.132138
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : CDifferentiable R f
hg : CDifferentiable R g
⊢ (fun x dx => ((fun x => ⟪f x, g x⟫_R) x, cderiv R (fun x => ⟪f x, g x⟫_R) x dx)) = fun x dx =>
    let y₁dy₁ := (f x, cderiv R f x dx);
    let y₂dy₂ := (g x, cderiv R g x dx);
    (⟪y₁dy₁.1, y₂dy₂.1⟫_R, ⟪y₁dy₁.2, y₂dy₂.1⟫_R + ⟪y₁dy₁.1, y₂dy₂.2⟫_R)
Theorem: SciLean.fwdDeriv.Inner.inner.arg_a0a1.fwdDeriv_rule
Proof state before:
K : Type ?u.132059
inst✝¹¹ : RCLike K
X✝ : Type ?u.132065
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.132078
inst✝⁹ : Vec K Y✝
Z : Type ?u.132089
inst✝⁸ : Vec K Z
W : Type ?u.132100
inst✝⁷ : Vec K W
ι : Type ?u.132111
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.132138
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : CDifferentiable R f
hg : CDifferentiable R g
⊢ (fun x dx => ((fun x => ⟪f x, g x⟫_R) x, cderiv R (fun x => ⟪f x, g x⟫_R) x dx)) = fun x dx =>
    let y₁dy₁ := (f x, cderiv R f x dx);
    let y₂dy₂ := (g x, cderiv R g x dx);
    (⟪y₁dy₁.1, y₂dy₂.1⟫_R, ⟪y₁dy₁.2, y₂dy₂.1⟫_R + ⟪y₁dy₁.1, y₂dy₂.2⟫_R)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.SciLean.Norm2.norm2.arg_a0.fwdDeriv_rule_at
Proof state before:
K : Type ?u.135235
inst✝¹¹ : RCLike K
X✝ : Type ?u.135241
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.135254
inst✝⁹ : Vec K Y✝
Z : Type ?u.135265
inst✝⁸ : Vec K Z
W : Type ?u.135276
inst✝⁷ : Vec K W
ι : Type ?u.135287
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.135314
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiableAt R f x
⊢ fwdDeriv R (fun x => ‖f x‖₂²) x = fun dx =>
    let ydy := fwdDeriv R f x dx;
    (‖ydy.1‖₂², 2 * ⟪ydy.2, ydy.1⟫_R)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type ?u.135235
inst✝¹¹ : RCLike K
X✝ : Type ?u.135241
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.135254
inst✝⁹ : Vec K Y✝
Z : Type ?u.135265
inst✝⁸ : Vec K Z
W : Type ?u.135276
inst✝⁷ : Vec K W
ι : Type ?u.135287
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.135314
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiableAt R f x
⊢ (fun dx => ((fun x => ‖f x‖₂²) x, cderiv R (fun x => ‖f x‖₂²) x dx)) = fun dx =>
    let ydy := (f x, cderiv R f x dx);
    (‖ydy.1‖₂², 2 * ⟪ydy.2, ydy.1⟫_R)
Theorem: SciLean.fwdDeriv.SciLean.Norm2.norm2.arg_a0.fwdDeriv_rule_at
Proof state before:
K : Type ?u.135235
inst✝¹¹ : RCLike K
X✝ : Type ?u.135241
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.135254
inst✝⁹ : Vec K Y✝
Z : Type ?u.135265
inst✝⁸ : Vec K Z
W : Type ?u.135276
inst✝⁷ : Vec K W
ι : Type ?u.135287
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.135314
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiableAt R f x
⊢ (fun dx => ((fun x => ‖f x‖₂²) x, cderiv R (fun x => ‖f x‖₂²) x dx)) = fun dx =>
    let ydy := (f x, cderiv R f x dx);
    (‖ydy.1‖₂², 2 * ⟪ydy.2, ydy.1⟫_R)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.SciLean.Norm2.norm2.arg_a0.fwdDeriv_rule
Proof state before:
K : Type ?u.137880
inst✝¹¹ : RCLike K
X✝ : Type ?u.137886
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.137899
inst✝⁹ : Vec K Y✝
Z : Type ?u.137910
inst✝⁸ : Vec K Z
W : Type ?u.137921
inst✝⁷ : Vec K W
ι : Type ?u.137932
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.137959
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
⊢ (fwdDeriv R fun x => ‖f x‖₂²) = fun x dx =>
    let ydy := fwdDeriv R f x dx;
    (‖ydy.1‖₂², 2 * ⟪ydy.2, ydy.1⟫_R)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type ?u.137880
inst✝¹¹ : RCLike K
X✝ : Type ?u.137886
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.137899
inst✝⁹ : Vec K Y✝
Z : Type ?u.137910
inst✝⁸ : Vec K Z
W : Type ?u.137921
inst✝⁷ : Vec K W
ι : Type ?u.137932
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.137959
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
⊢ (fun x dx => ((fun x => ‖f x‖₂²) x, cderiv R (fun x => ‖f x‖₂²) x dx)) = fun x dx =>
    let ydy := (f x, cderiv R f x dx);
    (‖ydy.1‖₂², 2 * ⟪ydy.2, ydy.1⟫_R)
Theorem: SciLean.fwdDeriv.SciLean.Norm2.norm2.arg_a0.fwdDeriv_rule
Proof state before:
K : Type ?u.137880
inst✝¹¹ : RCLike K
X✝ : Type ?u.137886
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.137899
inst✝⁹ : Vec K Y✝
Z : Type ?u.137910
inst✝⁸ : Vec K Z
W : Type ?u.137921
inst✝⁷ : Vec K W
ι : Type ?u.137932
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.137959
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
⊢ (fun x dx => ((fun x => ‖f x‖₂²) x, cderiv R (fun x => ‖f x‖₂²) x dx)) = fun x dx =>
    let ydy := (f x, cderiv R f x dx);
    (‖ydy.1‖₂², 2 * ⟪ydy.2, ydy.1⟫_R)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.SciLean.norm₂.arg_x.fwdDeriv_rule_at
Proof state before:
K : Type ?u.140700
inst✝¹¹ : RCLike K
X✝ : Type ?u.140706
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.140719
inst✝⁹ : Vec K Y✝
Z : Type ?u.140730
inst✝⁸ : Vec K Z
W : Type ?u.140741
inst✝⁷ : Vec K W
ι : Type ?u.140752
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.140779
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiableAt R f x
hx : f x ≠ 0
⊢ fwdDeriv R (fun x => ‖f x‖₂[R]) x = fun dx =>
    let ydy := fwdDeriv R f x dx;
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type ?u.140700
inst✝¹¹ : RCLike K
X✝ : Type ?u.140706
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.140719
inst✝⁹ : Vec K Y✝
Z : Type ?u.140730
inst✝⁸ : Vec K Z
W : Type ?u.140741
inst✝⁷ : Vec K W
ι : Type ?u.140752
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.140779
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiableAt R f x
hx : f x ≠ 0
⊢ (fun dx => ((fun x => ‖f x‖₂[R]) x, cderiv R (fun x => ‖f x‖₂[R]) x dx)) = fun dx =>
    let ydy := (f x, cderiv R f x dx);
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Theorem: SciLean.fwdDeriv.SciLean.norm₂.arg_x.fwdDeriv_rule_at
Proof state before:
K : Type ?u.140700
inst✝¹¹ : RCLike K
X✝ : Type ?u.140706
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.140719
inst✝⁹ : Vec K Y✝
Z : Type ?u.140730
inst✝⁸ : Vec K Z
W : Type ?u.140741
inst✝⁷ : Vec K W
ι : Type ?u.140752
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.140779
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiableAt R f x
hx : f x ≠ 0
⊢ (fun dx => ((fun x => ‖f x‖₂[R]) x, cderiv R (fun x => ‖f x‖₂[R]) x dx)) = fun dx =>
    let ydy := (f x, cderiv R f x dx);
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Tactic:
fun_trans (disch:=assumption)
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.SciLean.norm₂.arg_x.fwdDeriv_rule_at
Proof state before:
case funProp.discharger
K : Type ?u.140700
inst✝¹¹ : RCLike K
X✝ : Type ?u.140706
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.140719
inst✝⁹ : Vec K Y✝
Z : Type ?u.140730
inst✝⁸ : Vec K Z
W : Type ?u.140741
inst✝⁷ : Vec K W
ι : Type ?u.140752
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.140779
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiableAt R f x
hx : f x ≠ 0
dx : X
⊢ f x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.SciLean.norm₂.arg_x.fwdDeriv_rule
Proof state before:
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
hx : ∀ (x : X), f x ≠ 0
⊢ (fwdDeriv R fun x => ‖f x‖₂[R]) = fun x dx =>
    let ydy := fwdDeriv R f x dx;
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
hx : ∀ (x : X), f x ≠ 0
⊢ (fun x dx => ((fun x => ‖f x‖₂[R]) x, cderiv R (fun x => ‖f x‖₂[R]) x dx)) = fun x dx =>
    let ydy := (f x, cderiv R f x dx);
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Theorem: SciLean.fwdDeriv.SciLean.norm₂.arg_x.fwdDeriv_rule
Proof state before:
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
hx : ∀ (x : X), f x ≠ 0
⊢ (fun x dx => ((fun x => ‖f x‖₂[R]) x, cderiv R (fun x => ‖f x‖₂[R]) x dx)) = fun x dx =>
    let ydy := (f x, cderiv R f x dx);
    let ynorm := ‖ydy.1‖₂[R];
    (ynorm, ynorm⁻¹ * ⟪ydy.2, ydy.1⟫_R)
Tactic:
fun_trans (disch:=assumption)
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.SciLean.norm₂.arg_x.fwdDeriv_rule
Proof state before:
case funProp.discharger
K : Type ?u.145640
inst✝¹¹ : RCLike K
X✝ : Type ?u.145646
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.145659
inst✝⁹ : Vec K Y✝
Z : Type ?u.145670
inst✝⁸ : Vec K Z
W : Type ?u.145681
inst✝⁷ : Vec K W
ι : Type ?u.145692
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.145719
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
hx : ∀ (x : X), f x ≠ 0
x dx : X
⊢ ∀ (x : X), f x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.Diffeomorphism.id_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type ?u.1190
inst✝⁶ : Vec K Y
Z : Type ?u.1201
inst✝⁵ : Vec K Z
W : Type ?u.1212
inst✝⁴ : Vec K W
ι : Type ?u.1223
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.1250
inst✝ : (i : ι) → Vec K (E i)
⊢ Diffeomorphism K fun x => x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Diffeomorphism.comp_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.1352
inst✝⁴ : Vec K W
ι : Type ?u.1363
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.1390
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : Diffeomorphism K f
hg : Diffeomorphism K g
⊢ Diffeomorphism K fun x => f (g x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.id.arg_a.Diffeomorphism_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type ?u.1550
inst✝⁶ : Vec K Y
Z : Type ?u.1561
inst✝⁵ : Vec K Z
W : Type ?u.1572
inst✝⁴ : Vec K W
ι : Type ?u.1583
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.1610
inst✝ : (i : ι) → Vec K (E i)
⊢ Diffeomorphism K fun x => id x
Tactic:
simp[id]
Proof state after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type ?u.1550
inst✝⁶ : Vec K Y
Z : Type ?u.1561
inst✝⁵ : Vec K Z
W : Type ?u.1572
inst✝⁴ : Vec K W
ι : Type ?u.1583
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.1610
inst✝ : (i : ι) → Vec K (E i)
⊢ Diffeomorphism K fun x => x
Theorem: SciLean.id.arg_a.Diffeomorphism_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type ?u.1550
inst✝⁶ : Vec K Y
Z : Type ?u.1561
inst✝⁵ : Vec K Z
W : Type ?u.1572
inst✝⁴ : Vec K W
ι : Type ?u.1583
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.1610
inst✝ : (i : ι) → Vec K (E i)
⊢ Diffeomorphism K fun x => x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Function.comp.arg_a0.Diffeomorphism_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.2340
inst✝⁴ : Vec K W
ι : Type ?u.2351
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.2378
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : Diffeomorphism K f
hg : Diffeomorphism K g
⊢ Diffeomorphism K fun x => (f ∘ g) x
Tactic:
simp[Function.comp]
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.2340
inst✝⁴ : Vec K W
ι : Type ?u.2351
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.2378
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : Diffeomorphism K f
hg : Diffeomorphism K g
⊢ Diffeomorphism K fun x => f (g x)
Theorem: SciLean.Function.comp.arg_a0.Diffeomorphism_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.2340
inst✝⁴ : Vec K W
ι : Type ?u.2351
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.2378
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : Diffeomorphism K f
hg : Diffeomorphism K g
⊢ Diffeomorphism K fun x => f (g x)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Neg.neg.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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : Diffeomorphism K f
⊢ Diffeomorphism K fun x => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -f x
Theorem: SciLean.Neg.neg.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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -f x) x)
Theorem: SciLean.Neg.neg.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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -f x) x)
Theorem: SciLean.Neg.neg.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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -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.3358
inst✝⁵ : Vec K Z
W : Type ?u.3369
inst✝⁴ : Vec K W
ι : Type ?u.3380
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3407
inst✝ : (i : ι) → Vec K (E i)
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 => -f x) x)