internlm/Lean-Github huggingface dataset:
Theorem: SciLean.SciLean.cderiv.arg_dx.cderiv_rule
Proof state before:
K✝ : Type ?u.120637
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.120643
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.120656
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.120667
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.120678
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.120689
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.120716
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.120773
inst✝⁴ : Vec K W
ι : Type ?u.120784
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.120811
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (cderiv K fun dx => cderiv K f y (g dx)) = fun dx ddx =>
    let ddy := cderiv K g dx ddx;
    cderiv K f y ddy
Tactic:
funext dx
Proof state after:
case h
K✝ : Type ?u.120637
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.120643
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.120656
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.120667
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.120678
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.120689
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.120716
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.120773
inst✝⁴ : Vec K W
ι : Type ?u.120784
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.120811
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ cderiv K (fun dx => cderiv K f y (g dx)) dx = fun ddx =>
    let ddy := cderiv K g dx ddx;
    cderiv K f y ddy
Theorem: SciLean.SciLean.cderiv.arg_dx.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.120637
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.120643
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.120656
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.120667
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.120678
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.120689
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.120716
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
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.120773
inst✝⁴ : Vec K W
ι : Type ?u.120784
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.120811
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
y : Y
hf : CDifferentiable K f
hg : CDifferentiable K g
dx : X
⊢ cderiv K (fun dx => cderiv K f y (g dx)) dx = fun ddx =>
    let ddy := cderiv K g dx ddx;
    cderiv K f y ddy
Tactic:
apply cderiv.arg_dx.cderiv_rule_at _ _ _ _ (hf y) (hg dx)
Proof state after:
no goals
Theorem: SciLean.StructType.structMake_zero
Proof state before:
K : Type u_4
inst✝¹⁴ : RCLike K
ι : Type ?u.168462
κ : Type ?u.168465
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.168512
I : Type u_2
EI : I → Type ?u.168520
inst✝⁷ : StructType E I EI
F : Type ?u.168531
J : Type ?u.168534
FJ : J → Type ?u.168539
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.168663
inst✝ : Vec K W
⊢ (structMake fun x => 0) = 0
Tactic:
apply structExt (I:=I)
Proof state after:
case a
K : Type u_4
inst✝¹⁴ : RCLike K
ι : Type ?u.168462
κ : Type ?u.168465
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.168512
I : Type u_2
EI : I → Type ?u.168520
inst✝⁷ : StructType E I EI
F : Type ?u.168531
J : Type ?u.168534
FJ : J → Type ?u.168539
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.168663
inst✝ : Vec K W
⊢ ∀ (i : I), structProj (structMake fun x => 0) i = structProj 0 i
Theorem: SciLean.StructType.structMake_zero
Proof state before:
case a
K : Type u_4
inst✝¹⁴ : RCLike K
ι : Type ?u.168462
κ : Type ?u.168465
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.168512
I : Type u_2
EI : I → Type ?u.168520
inst✝⁷ : StructType E I EI
F : Type ?u.168531
J : Type ?u.168534
FJ : J → Type ?u.168539
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.168663
inst✝ : Vec K W
⊢ ∀ (i : I), structProj (structMake fun x => 0) i = structProj 0 i
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.oneHot.arg_xi.IsLinearMap_rule
Proof state before:
K : Type u_1
inst✝¹⁴ : RCLike K
ι : Type ?u.178721
κ : Type ?u.178724
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.178771
I : Type u_5
EI : I → Type ?u.178779
inst✝⁷ : StructType E I EI
F : Type ?u.178790
J : Type ?u.178793
FJ : J → Type ?u.178798
inst✝⁶ : StructType F J FJ
X : Type u_4
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type u_2
inst✝ : Vec K W
i : I
xi : W → XI i
hxi : IsLinearMap K xi
⊢ IsLinearMap K fun w => oneHot i (xi w)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.add_oneHot_eq_structModify
Proof state before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ x + oneHot i xi = structModify i (fun xi' => xi' + xi) x
Tactic:
apply structExt (I:=I)
Proof state after:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj (x + oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1
Theorem: SciLean.add_oneHot_eq_structModify
Proof state before:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj (x + oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1
Tactic:
simp
Proof state after:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj x i_1 + structProj (oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1
Theorem: SciLean.add_oneHot_eq_structModify
Proof state before:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj x i_1 + structProj (oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1
Tactic:
intro j
Proof state after:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j
Theorem: SciLean.add_oneHot_eq_structModify
Proof state before:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j
Tactic:
if h:i=j then
  subst h; simp
else
  simp[h]
Proof state after:
no goals
Theorem: SciLean.add_oneHot_eq_structModify
Proof state before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
h : i = j
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j
Tactic:
subst h
Proof state after:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ structProj x i + structProj (oneHot i xi) i = structProj (structModify i (fun xi' => xi' + xi) x) i
Theorem: SciLean.add_oneHot_eq_structModify
Proof state before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ structProj x i + structProj (oneHot i xi) i = structProj (structModify i (fun xi' => xi' + xi) x) i
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.add_oneHot_eq_structModify
Proof state before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
h : ¬i = j
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.add_oneHot_eq_structModify'
Proof state before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.196743
κ : Type ?u.196746
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.196793
I : Type u_3
EI : I → Type ?u.196801
inst✝⁷ : StructType E I EI
F : Type ?u.196812
J : Type ?u.196815
FJ : J → Type ?u.196820
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.196944
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ oneHot i xi + x = structModify i (fun xi' => xi + xi') x
Tactic:
simp[add_comm]
Proof state after:
no goals
Theorem: SciLean.oneHot_inl
Proof state before:
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ oneHot (Sum.inl i) xi = (oneHot i xi, 0)
Tactic:
simp[oneHot, structMake]
Proof state after:
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ ((structMake fun a => if h : i = a then ⋯ ▸ xi else 0) = structMake fun i' => if h : i = i' then h ▸ xi else 0) ∧
    (structMake fun b => 0) = 0
Theorem: SciLean.oneHot_inl
Proof state before:
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ ((structMake fun a => if h : i = a then ⋯ ▸ xi else 0) = structMake fun i' => if h : i = i' then h ▸ xi else 0) ∧
    (structMake fun b => 0) = 0
Tactic:
constructor
Proof state after:
case left
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (structMake fun a => if h : i = a then ⋯ ▸ xi else 0) = structMake fun i' => if h : i = i' then h ▸ xi else 0

case right
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (structMake fun b => 0) = 0
Theorem: SciLean.oneHot_inl
Proof state before:
case left
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (structMake fun a => if h : i = a then ⋯ ▸ xi else 0) = structMake fun i' => if h : i = i' then h ▸ xi else 0

case right
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (structMake fun b => 0) = 0
Tactic:
. congr; funext; congr; funext h; subst h; rfl
Proof state after:
case right
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (structMake fun b => 0) = 0
Theorem: SciLean.oneHot_inl
Proof state before:
case right
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (structMake fun b => 0) = 0
Tactic:
. apply structExt (I:=J); simp [ZeroStruct.structProj_zero]
Proof state after:
no goals
Theorem: SciLean.oneHot_inl
Proof state before:
case left
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (structMake fun a => if h : i = a then ⋯ ▸ xi else 0) = structMake fun i' => if h : i = i' then h ▸ xi else 0
Tactic:
congr
Proof state after:
case left.e_f
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (fun a => if h : i = a then ⋯ ▸ xi else 0) = fun i' => if h : i = i' then h ▸ xi else 0
Theorem: SciLean.oneHot_inl
Proof state before:
case left.e_f
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
⊢ (fun a => if h : i = a then ⋯ ▸ xi else 0) = fun i' => if h : i = i' then h ▸ xi else 0
Tactic:
funext
Proof state after:
case left.e_f.h
K : Type ?u.211192
inst✝¹⁶ : RCLike K
ι : Type ?u.211198
κ : Type ?u.211201
inst✝¹⁵ : IndexType ι
inst✝¹⁴ : LawfulIndexType ι
inst✝¹³ : DecidableEq ι
inst✝¹² : IndexType κ
inst✝¹¹ : LawfulIndexType κ
inst✝¹⁰ : DecidableEq κ
E : Type u_1
I : Type u_4
EI : I → Type u_5
inst✝⁹ : StructType E I EI
F : Type u_2
J : Type u_3
FJ : J → Type u_5
inst✝⁸ : StructType F J FJ
inst✝⁷ : Zero E
inst✝⁶ : (i : I) → Zero (EI i)
inst✝⁵ : ZeroStruct E I EI
inst✝⁴ : Zero F
inst✝³ : (j : J) → Zero (FJ j)
inst✝² : ZeroStruct F J FJ
inst✝¹ : DecidableEq I
inst✝ : DecidableEq J
i : I
xi : EI i
x✝ : I
⊢ (if h : i = x✝ then ⋯ ▸ xi else 0) = if h : i = x✝ then h ▸ xi else 0