case a.h
l : Type u_1
m : Type u_2
n : Type ?u.116901
o : Type ?u.116904
p : Type ?u.116907
q : Type ?u.116910
m' : o → Type ?u.116915
n' : o → Type ?u.116920
p' : o → Type ?u.116925
R : Type ?u.116928
S : Type ?u.116931
α : Type u_3
β : Type ?u.116937
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
l : Type u_1
m : Type u_2
n : Type ?u.116901
o : Type ?u.116904
p : Type ?u.116907
q : Type ?u.116910
m' : o → Type ?u.116915
n' : o → Type ?u.116920
p' : o → Type ?u.116925
R : Type ?u.116928
S : Type ?u.116931
α : Type u_3
β : Type ?u.116937
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)
ext i j
no goals
case a.h
l : Type u_1
m : Type u_2
n : Type ?u.116901
o : Type ?u.116904
p : Type ?u.116907
q : Type ?u.116910
m' : o → Type ?u.116915
n' : o → Type ?u.116920
p' : o → Type ?u.116925
R : Type ?u.116928
S : Type ?u.116931
α : Type u_3
β : Type ?u.116937
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [diagonal]