Theorem: SciLean.oneHot_inl (SciLean/Data/StructType/Algebra.lean)

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]
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

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
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

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
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

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]
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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)
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

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]
State after:
no goals