case a.h
l : Type u_4
m : Type u_3
n : Type u_2
o : Type u_1
p : Type ?u.4504
q : Type ?u.4507
m' : o → Type ?u.4512
n' : o → Type ?u.4517
p' : o → Type ?u.4522
R : Type ?u.4525
S : Type ?u.4528
α : Type u_5
β : Type ?u.4534
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) i j = M i j
l : Type u_4
m : Type u_3
n : Type u_2
o : Type u_1
p : Type ?u.4504
q : Type ?u.4507
m' : o → Type ?u.4512
n' : o → Type ?u.4517
p' : o → Type ?u.4522
R : Type ?u.4525
S : Type ?u.4528
α : Type u_5
β : Type ?u.4534
M : Matrix (n ⊕ o) (l ⊕ m) α
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) = M
ext i j
no goals
case a.h
l : Type u_4
m : Type u_3
n : Type u_2
o : Type u_1
p : Type ?u.4504
q : Type ?u.4507
m' : o → Type ?u.4512
n' : o → Type ?u.4517
p' : o → Type ?u.4522
R : Type ?u.4525
S : Type ?u.4528
α : Type u_5
β : Type ?u.4534
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) i j = M i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl