no goals
l : Type ?u.1186135
m : Type u_1
n : Type u_2
o : Type ?u.1186144
m' : o → Type ?u.1186149
n' : o → Type ?u.1186154
R : Type ?u.1186157
S : Type ?u.1186160
α : Type v
β : Type w
γ : Type ?u.1186167
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
e : m ≃ n
M : Matrix m n α
⊢ submatrix M id ↑e ⬝ submatrix Mᵀ (↑e) id = M ⬝ Mᵀ
rw [submatrix_mul_equiv, submatrix_id_id]