no goals
R : Type ?u.2748126
R₁ : Type u_2
R₂ : Type ?u.2748132
M✝ : Type ?u.2748135
M₁ : Type u_3
M₂ : Type ?u.2748141
M₁' : Type ?u.2748144
M₂' : Type ?u.2748147
n : Type ?u.2748150
m : Type ?u.2748153
n' : Type ?u.2748156
m' : Type ?u.2748159
ι : Type u_1
inst✝⁴ : CommRing R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁
M : Matrix ι ι R₁
b : Basis ι R₁ M₁
⊢ SeparatingLeft (↑(toLinearMap₂ b b) M) ↔ Matrix.Nondegenerate M
rw [← Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂,
  Matrix.separatingLeft_toLinearMap₂'_iff]