internlm/Lean-Github huggingface dataset:
Theorem: SciLean.fwdDeriv.IndexType.sum.arg_f.fwdDeriv_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.119193
inst✝⁵ : Vec K Z
W : Type ?u.119204
inst✝⁴ : Vec K W
ι : Type u_4
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.119242
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
hf : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ (fun x dx => ( ∑ i, f x i, ∑ i, cderiv K (fun x => f x i) x dx)) = fun x dx =>
     ∑ i, (f x i, cderiv K (fun x => f x i) x dx)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
dec : Decidable c
t e : X → Y
⊢ (fwdDeriv K fun x => if c then t x else e x) = fun y => if c then fwdDeriv K t y else fwdDeriv K e y
Tactic:
induction dec
Proof state after:
case isFalse
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h✝ : ¬c
⊢ (fwdDeriv K fun x => if c then t x else e x) = fun y => if c then fwdDeriv K t y else fwdDeriv K e y

case isTrue
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h✝ : c
⊢ (fwdDeriv K fun x => if c then t x else e x) = fun y => if c then fwdDeriv K t y else fwdDeriv K e y
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
⊢ (fwdDeriv K fun x => if c then t x else e x) = fun y => if c then fwdDeriv K t y else fwdDeriv K e y
Tactic:
case isTrue h  => ext y; simp[h]; simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
⊢ (fwdDeriv K fun x => if c then t x else e x) = fun y => if c then fwdDeriv K t y else fwdDeriv K e y
Tactic:
case isFalse h => ext y; simp[h]; simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
⊢ (fwdDeriv K fun x => if c then t x else e x) = fun y => if c then fwdDeriv K t y else fwdDeriv K e y
Tactic:
ext y
Proof state after:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).1 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).1

case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).1 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).1

case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Tactic:
simp[h]
Proof state after:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
⊢ (fwdDeriv K fun x => if c then t x else e x) = fun y => if c then fwdDeriv K t y else fwdDeriv K e y
Tactic:
ext y
Proof state after:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).1 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).1

case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).1 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).1

case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Tactic:
simp[h]
Proof state after:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Theorem: SciLean.fwdDeriv.ite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.126534
inst✝⁵ : Vec K Z
W : Type ?u.126545
inst✝⁴ : Vec K W
ι : Type ?u.126556
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.126583
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if c then t x else e x) y x✝).2 = ((if c then fwdDeriv K t y else fwdDeriv K e y) x✝).2
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
dec : Decidable c
t : c → X → Y
e : ¬c → X → Y
⊢ (fwdDeriv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y
Tactic:
induction dec
Proof state after:
case isFalse
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h✝ : ¬c
⊢ (fwdDeriv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y

case isTrue
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h✝ : c
⊢ (fwdDeriv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
⊢ (fwdDeriv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y
Tactic:
case isTrue h  => ext y; simp[h]; simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
⊢ (fwdDeriv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y
Tactic:
case isFalse h => ext y; simp[h]; simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
⊢ (fwdDeriv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y
Tactic:
ext y
Proof state after:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).1 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).1

case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).1 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).1

case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Tactic:
simp[h]
Proof state after:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
⊢ (fwdDeriv K fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y
Tactic:
ext y
Proof state after:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).1 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).1

case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).1 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).1

case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Tactic:
simp[h]
Proof state after:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Theorem: SciLean.fwdDeriv.dite.arg_te.fwdDeriv_rule
Proof state before:
case h.h.a
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.127715
inst✝⁵ : Vec K Z
W : Type ?u.127726
inst✝⁴ : Vec K W
ι : Type ?u.127737
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.127764
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
h : ¬c
y x✝ : X
⊢ (fwdDeriv K (fun x => if x_1 : c then t x_1 x else e x_1 x) y x✝).2 =
    ((if p : c then fwdDeriv K (t p) y else fwdDeriv K (e p) y) x✝).2
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.fwdDeriv.Inner.inner.arg_a0a1.fwdDeriv_rule_at
Proof state before:
K : Type ?u.129107
inst✝¹¹ : RCLike K
X✝ : Type ?u.129113
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.129126
inst✝⁹ : Vec K Y✝
Z : Type ?u.129137
inst✝⁸ : Vec K Z
W : Type ?u.129148
inst✝⁷ : Vec K W
ι : Type ?u.129159
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.129186
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 g : X → Y
hf : CDifferentiableAt R f x
hg : CDifferentiableAt R g x
⊢ fwdDeriv R (fun x => ⟪f x, g x⟫_R) x = fun 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.129107
inst✝¹¹ : RCLike K
X✝ : Type ?u.129113
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.129126
inst✝⁹ : Vec K Y✝
Z : Type ?u.129137
inst✝⁸ : Vec K Z
W : Type ?u.129148
inst✝⁷ : Vec K W
ι : Type ?u.129159
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.129186
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 g : X → Y
hf : CDifferentiableAt R f x
hg : CDifferentiableAt R g x
⊢ (fun dx => ((fun x => ⟪f x, g x⟫_R) x, cderiv R (fun x => ⟪f x, g x⟫_R) x dx)) = fun 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_at
Proof state before:
K : Type ?u.129107
inst✝¹¹ : RCLike K
X✝ : Type ?u.129113
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.129126
inst✝⁹ : Vec K Y✝
Z : Type ?u.129137
inst✝⁸ : Vec K Z
W : Type ?u.129148
inst✝⁷ : Vec K W
ι : Type ?u.129159
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.129186
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 g : X → Y
hf : CDifferentiableAt R f x
hg : CDifferentiableAt R g x
⊢ (fun dx => ((fun x => ⟪f x, g x⟫_R) x, cderiv R (fun x => ⟪f x, g x⟫_R) x dx)) = fun 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