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