no goals
l : Type ?u.172
m : Type u_1
n : Type u_2
o : Type ?u.181
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : Fintype o
α : m → n → Type v
M N : DMatrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j
simp [h]