internlm/Lean-Github huggingface dataset:
Theorem: SciLean.oneHot_inl
Proof state before:
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
Tactic:
congr
Proof state after:
case left.e_f.h.e_t
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
⊢ (fun h => ⋯ ▸ xi) = fun h => h ▸ xi
Theorem: SciLean.oneHot_inl
Proof state before:
case left.e_f.h.e_t
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
⊢ (fun h => ⋯ ▸ xi) = fun h => h ▸ xi
Tactic:
funext h
Proof state after:
case left.e_f.h.e_t.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
h : i = x✝
⊢ ⋯ ▸ xi = h ▸ xi
Theorem: SciLean.oneHot_inl
Proof state before:
case left.e_f.h.e_t.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
h : i = x✝
⊢ ⋯ ▸ xi = h ▸ xi
Tactic:
subst h
Proof state after:
case left.e_f.h.e_t.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
⊢ ⋯ ▸ xi = ⋯ ▸ xi
Theorem: SciLean.oneHot_inl
Proof state before:
case left.e_f.h.e_t.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
⊢ ⋯ ▸ xi = ⋯ ▸ xi
Tactic:
rfl
Proof state after:
no goals
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)
Proof state after:
case right.a
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
⊢ ∀ (i : J), structProj (structMake fun b => 0) i = structProj 0 i
Theorem: SciLean.oneHot_inl
Proof state before:
case right.a
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
⊢ ∀ (i : J), structProj (structMake fun b => 0) i = structProj 0 i
Tactic:
simp [ZeroStruct.structProj_zero]
Proof state after:
no goals
Theorem: SciLean.oneHot_inr
Proof state before:
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ oneHot (Sum.inr j) xj = (0, oneHot j xj)
Tactic:
simp[oneHot, structMake]
Proof state after:
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun a => 0) = 0 ∧
    (structMake fun b => if h : j = b then ⋯ ▸ xj else 0) = structMake fun i' => if h : j = i' then h ▸ xj else 0
Theorem: SciLean.oneHot_inr
Proof state before:
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun a => 0) = 0 ∧
    (structMake fun b => if h : j = b then ⋯ ▸ xj else 0) = structMake fun i' => if h : j = i' then h ▸ xj else 0
Tactic:
constructor
Proof state after:
case left
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun a => 0) = 0

case right
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun b => if h : j = b then ⋯ ▸ xj else 0) = structMake fun i' => if h : j = i' then h ▸ xj else 0
Theorem: SciLean.oneHot_inr
Proof state before:
case left
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun a => 0) = 0

case right
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun b => if h : j = b then ⋯ ▸ xj else 0) = structMake fun i' => if h : j = i' then h ▸ xj else 0
Tactic:
. apply structExt (I:=I); simp [ZeroStruct.structProj_zero]
Proof state after:
case right
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun b => if h : j = b then ⋯ ▸ xj else 0) = structMake fun i' => if h : j = i' then h ▸ xj else 0
Theorem: SciLean.oneHot_inr
Proof state before:
case right
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun b => if h : j = b then ⋯ ▸ xj else 0) = structMake fun i' => if h : j = i' then h ▸ xj else 0
Tactic:
. congr; funext; congr; funext h; subst h; rfl
Proof state after:
no goals
Theorem: SciLean.oneHot_inr
Proof state before:
case left
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun a => 0) = 0
Tactic:
apply structExt (I:=I)
Proof state after:
case left.a
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ ∀ (i : I), structProj (structMake fun a => 0) i = structProj 0 i
Theorem: SciLean.oneHot_inr
Proof state before:
case left.a
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ ∀ (i : I), structProj (structMake fun a => 0) i = structProj 0 i
Tactic:
simp [ZeroStruct.structProj_zero]
Proof state after:
no goals
Theorem: SciLean.oneHot_inr
Proof state before:
case right
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (structMake fun b => if h : j = b then ⋯ ▸ xj else 0) = structMake fun i' => if h : j = i' then h ▸ xj else 0
Tactic:
congr
Proof state after:
case right.e_f
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (fun b => if h : j = b then ⋯ ▸ xj else 0) = fun i' => if h : j = i' then h ▸ xj else 0
Theorem: SciLean.oneHot_inr
Proof state before:
case right.e_f
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ (fun b => if h : j = b then ⋯ ▸ xj else 0) = fun i' => if h : j = i' then h ▸ xj else 0
Tactic:
funext
Proof state after:
case right.e_f.h
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
x✝ : J
⊢ (if h : j = x✝ then ⋯ ▸ xj else 0) = if h : j = x✝ then h ▸ xj else 0
Theorem: SciLean.oneHot_inr
Proof state before:
case right.e_f.h
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
x✝ : J
⊢ (if h : j = x✝ then ⋯ ▸ xj else 0) = if h : j = x✝ then h ▸ xj else 0
Tactic:
congr
Proof state after:
case right.e_f.h.e_t
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
x✝ : J
⊢ (fun h => ⋯ ▸ xj) = fun h => h ▸ xj
Theorem: SciLean.oneHot_inr
Proof state before:
case right.e_f.h.e_t
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
x✝ : J
⊢ (fun h => ⋯ ▸ xj) = fun h => h ▸ xj
Tactic:
funext h
Proof state after:
case right.e_f.h.e_t.h
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
x✝ : J
h : j = x✝
⊢ ⋯ ▸ xj = h ▸ xj
Theorem: SciLean.oneHot_inr
Proof state before:
case right.e_f.h.e_t.h
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
x✝ : J
h : j = x✝
⊢ ⋯ ▸ xj = h ▸ xj
Tactic:
subst h
Proof state after:
case right.e_f.h.e_t.h
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ ⋯ ▸ xj = ⋯ ▸ xj
Theorem: SciLean.oneHot_inr
Proof state before:
case right.e_f.h.e_t.h
K : Type ?u.222434
inst✝¹⁶ : RCLike K
ι : Type ?u.222440
κ : Type ?u.222443
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
j : J
xj : FJ j
⊢ ⋯ ▸ xj = ⋯ ▸ xj
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prob.distribution_action_normalize
Proof state before:
W : Type ?u.11935
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.12614
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Distribution X
φ : X → Y
⊢ f.action φ = ⟪f, φ⟫
Tactic:
rfl
Proof state after:
no goals