case pos
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A

case neg
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ = Ring.inverse A
by_cases h_det : IsUnit A.det
case pos.intro
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
val✝ : Invertible A
⊢ A⁻¹ = Ring.inverse A
case pos
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A
cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible
no goals
case pos.intro
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
val✝ : Invertible A
⊢ A⁻¹ = Ring.inverse A
rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
case neg
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
h : ¬IsUnit A
⊢ A⁻¹ = Ring.inverse A
case neg
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A
have h := mt A.isUnit_iff_isUnit_det.mp h_det
no goals
case neg
l : Type ?u.181457
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
h : ¬IsUnit A
⊢ A⁻¹ = Ring.inverse A
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]