case a.h
l : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.36307
q : Type ?u.36310
m' : o → Type ?u.36315
n' : o → Type ?u.36320
p' : o → Type ?u.36325
R : Type ?u.36328
S : Type ?u.36331
α : Type u_1
β : Type ?u.36337
inst✝ : Zero α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks 0 0 0 0 i j = OfNat.ofNat 0 i j
l : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.36307
q : Type ?u.36310
m' : o → Type ?u.36315
n' : o → Type ?u.36320
p' : o → Type ?u.36325
R : Type ?u.36328
S : Type ?u.36331
α : Type u_1
β : Type ?u.36337
inst✝ : Zero α
⊢ fromBlocks 0 0 0 0 = 0
ext (i j)
no goals
case a.h
l : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
p : Type ?u.36307
q : Type ?u.36310
m' : o → Type ?u.36315
n' : o → Type ?u.36320
p' : o → Type ?u.36325
R : Type ?u.36328
S : Type ?u.36331
α : Type u_1
β : Type ?u.36337
inst✝ : Zero α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks 0 0 0 0 i j = OfNat.ofNat 0 i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl