internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prod.snd.arg_self.cderiv_rule
Proof state before:
K✝ : Type ?u.30744
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.30750
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.30763
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.30774
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.30785
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.30796
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.30823
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.30880
inst✝⁴ : Vec K W
ι : Type ?u.30891
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.30918
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
⊢ (cderiv K fun x => (f x).2) = fun x dx => (cderiv K f x dx).2
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.30744
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.30750
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.30763
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.30774
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.30785
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.30796
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.30823
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.30880
inst✝⁴ : Vec K W
ι : Type ?u.30891
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.30918
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
x : X
⊢ cderiv K (fun x => (f x).2) x = fun dx => (cderiv K f x dx).2
Theorem: SciLean.Prod.snd.arg_self.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.30744
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.30750
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.30763
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.30774
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.30785
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.30796
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.30823
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.30880
inst✝⁴ : Vec K W
ι : Type ?u.30891
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.30918
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
x : X
⊢ cderiv K (fun x => (f x).2) x = fun dx => (cderiv K f x dx).2
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0a1.cderiv_rule_at
Proof state before:
K✝ : Type ?u.32112
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.32118
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.32131
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.32142
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.32153
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.32164
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.32191
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.32237
inst✝⁵ : Vec K Z
W : Type ?u.32248
inst✝⁴ : Vec K W
ι : Type ?u.32259
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.32286
inst✝ : (i : ι) → Vec K (E i)
x : X
f g : X → Y
hf : CDifferentiableAt K f x
hg : CDifferentiableAt K g x
⊢ cderiv K (fun x => f x + g x) x = fun dx => cderiv K f x dx + cderiv K g x dx
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0a1.cderiv_rule
Proof state before:
K✝ : Type ?u.36190
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.36196
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.36209
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.36220
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.36231
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.36242
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.36269
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.36315
inst✝⁵ : Vec K Z
W : Type ?u.36326
inst✝⁴ : Vec K W
ι : Type ?u.36337
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.36364
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (cderiv K fun x => f x + g x) = fun x dx => cderiv K f x dx + cderiv K g x dx
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.36190
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.36196
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.36209
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.36220
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.36231
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.36242
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.36269
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.36315
inst✝⁵ : Vec K Z
W : Type ?u.36326
inst✝⁴ : Vec K W
ι : Type ?u.36337
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.36364
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
x : X
⊢ cderiv K (fun x => f x + g x) x = fun dx => cderiv K f x dx + cderiv K g x dx
Theorem: SciLean.HAdd.hAdd.arg_a0a1.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.36190
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.36196
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.36209
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.36220
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.36231
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.36242
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.36269
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.36315
inst✝⁵ : Vec K Z
W : Type ?u.36326
inst✝⁴ : Vec K W
ι : Type ?u.36337
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.36364
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
x : X
⊢ cderiv K (fun x => f x + g x) x = fun dx => cderiv K f x dx + cderiv K g x dx
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0.cderiv_rule
Proof state before:
K✝ : Type ?u.39307
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.39313
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.39326
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.39337
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.39348
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.39359
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.39386
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.39432
inst✝⁵ : Vec K Z
W : Type ?u.39443
inst✝⁴ : Vec K W
ι : Type ?u.39454
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.39481
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
⊢ (cderiv K fun x => f x + y) = fun x dx => cderiv K f x dx
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.39307
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.39313
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.39326
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.39337
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.39348
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.39359
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.39386
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.39432
inst✝⁵ : Vec K Z
W : Type ?u.39443
inst✝⁴ : Vec K W
ι : Type ?u.39454
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.39481
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => f x + y) x = fun dx => cderiv K f x dx
Theorem: SciLean.HAdd.hAdd.arg_a0.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.39307
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.39313
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.39326
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.39337
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.39348
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.39359
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.39386
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.39432
inst✝⁵ : Vec K Z
W : Type ?u.39443
inst✝⁴ : Vec K W
ι : Type ?u.39454
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.39481
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => f x + y) x = fun dx => cderiv K f x dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a1.cderiv_rule
Proof state before:
K✝ : Type ?u.40756
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.40762
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.40775
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.40786
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.40797
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.40808
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.40835
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.40881
inst✝⁵ : Vec K Z
W : Type ?u.40892
inst✝⁴ : Vec K W
ι : Type ?u.40903
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.40930
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
⊢ (cderiv K fun x => y + f x) = fun x dx => cderiv K f x dx
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.40756
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.40762
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.40775
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.40786
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.40797
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.40808
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.40835
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.40881
inst✝⁵ : Vec K Z
W : Type ?u.40892
inst✝⁴ : Vec K W
ι : Type ?u.40903
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.40930
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => y + f x) x = fun dx => cderiv K f x dx
Theorem: SciLean.HAdd.hAdd.arg_a1.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.40756
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.40762
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.40775
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.40786
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.40797
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.40808
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.40835
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.40881
inst✝⁵ : Vec K Z
W : Type ?u.40892
inst✝⁴ : Vec K W
ι : Type ?u.40903
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.40930
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => y + f x) x = fun dx => cderiv K f x dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0a1.cderiv_rule_at
Proof state before:
K✝ : Type ?u.42205
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.42211
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.42224
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.42235
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.42246
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.42257
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.42284
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.42330
inst✝⁵ : Vec K Z
W : Type ?u.42341
inst✝⁴ : Vec K W
ι : Type ?u.42352
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.42379
inst✝ : (i : ι) → Vec K (E i)
x : X
f g : X → Y
hf : CDifferentiableAt K f x
hg : CDifferentiableAt K g x
⊢ cderiv K (fun x => f x - g x) x = fun dx => cderiv K f x dx - cderiv K g x dx
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0a1.cderiv_rule
Proof state before:
K✝ : Type ?u.47095
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.47101
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.47114
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.47125
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.47136
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.47147
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.47174
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.47220
inst✝⁵ : Vec K Z
W : Type ?u.47231
inst✝⁴ : Vec K W
ι : Type ?u.47242
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.47269
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (cderiv K fun x => f x - g x) = fun x dx => cderiv K f x dx - cderiv K g x dx
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.47095
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.47101
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.47114
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.47125
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.47136
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.47147
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.47174
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.47220
inst✝⁵ : Vec K Z
W : Type ?u.47231
inst✝⁴ : Vec K W
ι : Type ?u.47242
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.47269
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
x : X
⊢ cderiv K (fun x => f x - g x) x = fun dx => cderiv K f x dx - cderiv K g x dx
Theorem: SciLean.HSub.hSub.arg_a0a1.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.47095
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.47101
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.47114
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.47125
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.47136
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.47147
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.47174
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.47220
inst✝⁵ : Vec K Z
W : Type ?u.47231
inst✝⁴ : Vec K W
ι : Type ?u.47242
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.47269
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
x : X
⊢ cderiv K (fun x => f x - g x) x = fun dx => cderiv K f x dx - cderiv K g x dx
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0.cderiv_rule
Proof state before:
K✝ : Type ?u.50462
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.50468
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.50481
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.50492
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.50503
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.50514
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.50541
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.50587
inst✝⁵ : Vec K Z
W : Type ?u.50598
inst✝⁴ : Vec K W
ι : Type ?u.50609
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.50636
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
⊢ (cderiv K fun x => f x - y) = fun x dx => cderiv K f x dx
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.50462
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.50468
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.50481
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.50492
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.50503
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.50514
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.50541
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.50587
inst✝⁵ : Vec K Z
W : Type ?u.50598
inst✝⁴ : Vec K W
ι : Type ?u.50609
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.50636
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => f x - y) x = fun dx => cderiv K f x dx
Theorem: SciLean.HSub.hSub.arg_a0.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.50462
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.50468
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.50481
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.50492
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.50503
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.50514
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.50541
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.50587
inst✝⁵ : Vec K Z
W : Type ?u.50598
inst✝⁴ : Vec K W
ι : Type ?u.50609
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.50636
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => f x - y) x = fun dx => cderiv K f x dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a1.cderiv_rule
Proof state before:
K✝ : Type ?u.51375
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.51381
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.51394
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.51405
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.51416
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.51427
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.51454
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.51500
inst✝⁵ : Vec K Z
W : Type ?u.51511
inst✝⁴ : Vec K W
ι : Type ?u.51522
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.51549
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
⊢ (cderiv K fun x => y - f x) = fun x dx => -cderiv K f x dx
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.51375
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.51381
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.51394
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.51405
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.51416
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.51427
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.51454
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.51500
inst✝⁵ : Vec K Z
W : Type ?u.51511
inst✝⁴ : Vec K W
ι : Type ?u.51522
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.51549
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => y - f x) x = fun dx => -cderiv K f x dx
Theorem: SciLean.HSub.hSub.arg_a1.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.51375
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.51381
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.51394
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.51405
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.51416
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.51427
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.51454
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.51500
inst✝⁵ : Vec K Z
W : Type ?u.51511
inst✝⁴ : Vec K W
ι : Type ?u.51522
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.51549
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
y : Y
x : X
⊢ cderiv K (fun x => y - f x) x = fun dx => -cderiv K f x dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Neg.neg.arg_a0.cderiv_rule'
Proof state before:
K✝ : Type ?u.52488
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.52494
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.52507
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.52518
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.52529
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.52540
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52567
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.52613
inst✝⁵ : Vec K Z
W : Type ?u.52624
inst✝⁴ : Vec K W
ι : Type ?u.52635
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.52662
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y
⊢ cderiv K (fun x => -f x) x = fun dx => -cderiv K f x dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Neg.neg.arg_a0.cderiv_rule
Proof state before:
K✝ : Type ?u.53040
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.53046
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.53059
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.53070
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.53081
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.53092
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.53119
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.53165
inst✝⁵ : Vec K Z
W : Type ?u.53176
inst✝⁴ : Vec K W
ι : Type ?u.53187
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.53214
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
⊢ (cderiv K fun x => -f x) = fun x dx => -cderiv K f x dx
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.53040
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.53046
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.53059
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.53070
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.53081
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.53092
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.53119
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.53165
inst✝⁵ : Vec K Z
W : Type ?u.53176
inst✝⁴ : Vec K W
ι : Type ?u.53187
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.53214
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
x : X
⊢ cderiv K (fun x => -f x) x = fun dx => -cderiv K f x dx
Theorem: SciLean.Neg.neg.arg_a0.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.53040
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.53046
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.53059
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.53070
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.53081
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.53092
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.53119
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.53165
inst✝⁵ : Vec K Z
W : Type ?u.53176
inst✝⁴ : Vec K W
ι : Type ?u.53187
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.53214
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
x : X
⊢ cderiv K (fun x => -f x) x = fun dx => -cderiv K f x dx
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.HMul.hMul.arg_a0a1.cderiv_rule_at
Proof state before:
K✝ : Type ?u.54834
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.54840
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.54853
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.54864
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.54875
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.54886
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.54913
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type ?u.54948
inst✝⁶ : Vec K Y
Z : Type ?u.54959
inst✝⁵ : Vec K Z
W : Type ?u.54970
inst✝⁴ : Vec K W
ι : Type ?u.54981
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.55008
inst✝ : (i : ι) → Vec K (E i)
x : X
f g : X → K
hf : CDifferentiableAt K f x
hg : CDifferentiableAt K g x
⊢ cderiv K (fun x => f x * g x) x =
    let fx := f x;
    let gx := g x;
    fun dx => cderiv K g x dx * fx + cderiv K f x dx * gx
Tactic:
sorry_proof
Proof state after:
no goals