no goals
l : Type ?u.398160
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
⊢ IsUnit (submatrix A ↑e₁ ↑e₂) ↔ IsUnit A
simp only [← nonempty_invertible_iff_isUnit,
  (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]