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

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

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

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

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

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

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

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

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

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

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

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

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