internlm/Lean-Github huggingface dataset:
Theorem: SciLean.ite.arg_te.cderiv_rule
Proof state before:
case h.h
K✝ : Type ?u.104136
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104142
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104155
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104166
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104177
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104188
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.104215
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.104261
inst✝⁵ : Vec K Z
W : Type ?u.104272
inst✝⁴ : Vec K W
ι : Type ?u.104283
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.104310
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
y x✝ : X
⊢ cderiv K (fun x => if c then t x else e x) y x✝ = (if c then cderiv K t y else cderiv K e y) x✝
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.ite.arg_te.cderiv_rule
Proof state before:
K✝ : Type ?u.104136
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104142
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104155
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104166
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104177
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104188
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.104215
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.104261
inst✝⁵ : Vec K Z
W : Type ?u.104272
inst✝⁴ : Vec K W
ι : Type ?u.104283
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.104310
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
⊢ (cderiv K fun x => if c then t x else e x) = fun y => if c then cderiv K t y else cderiv K e y
Tactic:
ext y
Proof state after:
case h.h
K✝ : Type ?u.104136
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104142
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104155
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104166
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104177
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104188
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.104215
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.104261
inst✝⁵ : Vec K Z
W : Type ?u.104272
inst✝⁴ : Vec K W
ι : Type ?u.104283
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.104310
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ cderiv K (fun x => if c then t x else e x) y x✝ = (if c then cderiv K t y else cderiv K e y) x✝
Theorem: SciLean.ite.arg_te.cderiv_rule
Proof state before:
case h.h
K✝ : Type ?u.104136
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104142
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104155
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104166
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104177
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104188
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.104215
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.104261
inst✝⁵ : Vec K Z
W : Type ?u.104272
inst✝⁴ : Vec K W
ι : Type ?u.104283
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.104310
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ cderiv K (fun x => if c then t x else e x) y x✝ = (if c then cderiv K t y else cderiv K e y) x✝
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.cderiv_rule
Proof state before:
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
dec : Decidable c
t : c → X → Y
e : ¬c → X → Y
⊢ (cderiv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then cderiv K (t p) y else cderiv K (e p) y
Tactic:
induction dec
Proof state after:
case isFalse
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h✝ : ¬c
⊢ (cderiv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then cderiv K (t p) y else cderiv K (e p) y

case isTrue
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h✝ : c
⊢ (cderiv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then cderiv K (t p) y else cderiv K (e p) y
Theorem: SciLean.dite.arg_te.cderiv_rule
Proof state before:
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
⊢ (cderiv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then cderiv K (t p) y else cderiv K (e p) y
Tactic:
case isTrue h  => ext y; simp[h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.cderiv_rule
Proof state before:
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
⊢ (cderiv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then cderiv K (t p) y else cderiv K (e p) y
Tactic:
case isFalse h => ext y; simp[h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.cderiv_rule
Proof state before:
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
⊢ (cderiv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then cderiv K (t p) y else cderiv K (e p) y
Tactic:
ext y
Proof state after:
case h.h
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ cderiv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝ =
    (if p : c then cderiv K (t p) y else cderiv K (e p) y) x✝
Theorem: SciLean.dite.arg_te.cderiv_rule
Proof state before:
case h.h
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ cderiv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝ =
    (if p : c then cderiv K (t p) y else cderiv K (e p) y) x✝
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.cderiv_rule
Proof state before:
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
⊢ (cderiv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then cderiv K (t p) y else cderiv K (e p) y
Tactic:
ext y
Proof state after:
case h.h
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ cderiv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝ =
    (if p : c then cderiv K (t p) y else cderiv K (e p) y) x✝
Theorem: SciLean.dite.arg_te.cderiv_rule
Proof state before:
case h.h
K✝ : Type ?u.104921
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.104927
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.104940
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.104951
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.104962
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.104973
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105000
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.105046
inst✝⁵ : Vec K Z
W : Type ?u.105057
inst✝⁴ : Vec K W
ι : Type ?u.105068
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105095
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ cderiv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝ =
    (if p : c then cderiv K (t p) y else cderiv K (e p) y) x✝
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.ite.arg_chte.cderiv_rule
Proof state before:
K✝ : Type ?u.105773
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.105779
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.105792
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.105803
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.105814
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.105825
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.105852
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_2
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.105898
inst✝⁵ : Vec K Z
W : Type ?u.105909
inst✝⁴ : Vec K W
ι : Type ?u.105920
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.105947
inst✝ : (i : ι) → Vec K (E i)
c : X → Prop
dec : (x : X) → Decidable (c x)
t e : X → Y
ht : ∀ x ∈ closure c, CDifferentiableAt K t x
he : ∀ x ∈ (interior c)ᶜ, CDifferentiableAt K e x
hc : ∀ x ∈ frontier c, cderiv K t x = cderiv K e x
⊢ (cderiv K fun x => if c x then t x else e x) = fun y => if c y then cderiv K t y else cderiv K e y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.cderiv_rule_at
Proof state before:
K✝ : Type ?u.106961
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.106967
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.106980
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.106991
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.107002
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.107013
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.107040
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.107056
inst✝¹¹ : RCLike K
X✝ : Type ?u.107062
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.107075
inst✝⁹ : Vec K Y✝
Z : Type ?u.107086
inst✝⁸ : Vec K Z
W : Type ?u.107097
inst✝⁷ : Vec K W
ι : Type ?u.107108
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.107135
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
x : X
hf : CDifferentiableAt R f x
hg : CDifferentiableAt R g x
⊢ cderiv R (fun x => ⟪f x, g x⟫_R) x = fun dx =>
    let y₁ := f x;
    let dy₁ := cderiv R f x dx;
    let y₂ := g x;
    let dy₂ := cderiv R g x dx;
    ⟪dy₁, y₂⟫_R + ⟪y₁, dy₂⟫_R
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.cderiv_rule
Proof state before:
K✝ : Type ?u.107796
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.107802
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.107815
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.107826
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.107837
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.107848
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.107875
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.107891
inst✝¹¹ : RCLike K
X✝ : Type ?u.107897
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.107910
inst✝⁹ : Vec K Y✝
Z : Type ?u.107921
inst✝⁸ : Vec K Z
W : Type ?u.107932
inst✝⁷ : Vec K W
ι : Type ?u.107943
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.107970
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
⊢ (cderiv R fun x => ⟪f x, g x⟫_R) = fun x dx =>
    let y₁ := f x;
    let dy₁ := cderiv R f x dx;
    let y₂ := g x;
    let dy₂ := cderiv R g x dx;
    ⟪dy₁, y₂⟫_R + ⟪y₁, dy₂⟫_R
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.107796
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.107802
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.107815
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.107826
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.107837
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.107848
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.107875
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.107891
inst✝¹¹ : RCLike K
X✝ : Type ?u.107897
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.107910
inst✝⁹ : Vec K Y✝
Z : Type ?u.107921
inst✝⁸ : Vec K Z
W : Type ?u.107932
inst✝⁷ : Vec K W
ι : Type ?u.107943
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.107970
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
x : X
⊢ cderiv R (fun x => ⟪f x, g x⟫_R) x = fun dx =>
    let y₁ := f x;
    let dy₁ := cderiv R f x dx;
    let y₂ := g x;
    let dy₂ := cderiv R g x dx;
    ⟪dy₁, y₂⟫_R + ⟪y₁, dy₂⟫_R
Theorem: SciLean.Inner.inner.arg_a0a1.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.107796
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.107802
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.107815
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.107826
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.107837
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.107848
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.107875
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.107891
inst✝¹¹ : RCLike K
X✝ : Type ?u.107897
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.107910
inst✝⁹ : Vec K Y✝
Z : Type ?u.107921
inst✝⁸ : Vec K Z
W : Type ?u.107932
inst✝⁷ : Vec K W
ι : Type ?u.107943
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.107970
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
x : X
⊢ cderiv R (fun x => ⟪f x, g x⟫_R) x = fun dx =>
    let y₁ := f x;
    let dy₁ := cderiv R f x dx;
    let y₂ := g x;
    let dy₂ := cderiv R g x dx;
    ⟪dy₁, y₂⟫_R + ⟪y₁, dy₂⟫_R
Tactic:
apply Inner.inner.arg_a0a1.cderiv_rule_at f g x (hf x) (hg x)
Proof state after:
no goals
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule_at
Proof state before:
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
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
x : X
hf : CDifferentiableAt R f x
⊢ cderiv R (fun x => ‖f x‖₂²) x = fun dx =>
    let y := f x;
    let dy := cderiv R f x dx;
    2 * ⟪dy, y⟫_R
Tactic:
simp_rw [← SemiInnerProductSpace.inner_norm2]
Proof state after:
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
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
x : X
hf : CDifferentiableAt R f x
⊢ cderiv R (fun x => ⟪f x, f x⟫_R) x = fun dx => 2 * ⟪cderiv R f x dx, f x⟫_R
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.cderiv_rule_at
Proof state before:
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
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
x : X
hf : CDifferentiableAt R f x
⊢ cderiv R (fun x => ⟪f x, f x⟫_R) x = fun dx => 2 * ⟪cderiv R f x dx, f x⟫_R
Tactic:
fun_trans
Proof state after:
K✝ : Type ?u.108719
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.108725
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.108738
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.108749
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.108760
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.108771
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.108798
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.108814
inst✝¹¹ : RCLike K
X✝ : Type ?u.108820
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.108833
inst✝⁹ : Vec K Y✝
Z : Type ?u.108844
inst✝⁸ : Vec K Z
W : Type ?u.108855
inst✝⁷ : Vec K W
ι : Type ?u.108866
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.108893
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
x : X
hf : CDifferentiableAt R f x
⊢ (fun dx => ⟪cderiv R (fun x => f x) x dx, f x⟫_R + ⟪f x, cderiv R (fun x => f x) x dx⟫_R) = fun dx =>
    2 * ⟪cderiv R f x dx, f x⟫_R