case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit (det A)
h : n ≤ m
⊢ IsUnit (det (A ^ n))
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit (det A)
h : n ≤ m
⊢ A ^ (m - n) = A ^ m ⬝ (A ^ n)⁻¹
rw [← tsub_add_cancel_of_le h, pow_add, mul_eq_mul, Matrix.mul_assoc, mul_nonsing_inv,
  tsub_add_cancel_of_le h, Matrix.mul_one]
no goals
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit (det A)
h : n ≤ m
⊢ IsUnit (det (A ^ n))
simpa using ha.pow n