no goals
l : Type u_4
m : Type u_3
n : Type u_2
o : Type u_1
p : Type ?u.5734
q : Type ?u.5737
m' : o → Type ?u.5742
n' : o → Type ?u.5747
p' : o → Type ?u.5752
R : Type ?u.5755
S : Type ?u.5758
α : Type u_5
β : Type ?u.5764
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  toBlocks₁₁ A = toBlocks₁₁ B ∧ toBlocks₁₂ A = toBlocks₁₂ B ∧ toBlocks₂₁ A = toBlocks₂₁ B ∧ toBlocks₂₂ A = toBlocks₂₂ B
h₁₁ : toBlocks₁₁ A = toBlocks₁₁ B
h₁₂ : toBlocks₁₂ A = toBlocks₁₂ B
h₂₁ : toBlocks₂₁ A = toBlocks₂₁ B
h₂₂ : toBlocks₂₂ A = toBlocks₂₂ B
⊢ A = B
rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]