-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v)

Proof state:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Tactic:
cases this.nonempty_invertible

Result:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝ : Invertible (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Proof state:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Tactic:
have := isUnit_diagonal.mpr h

Result:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ (diagonal v)⁻¹ = diagonal (Ring.inverse v)

Tactic:
rw [nonsing_inv_eq_ring_inverse]

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Proof state:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Tactic:
rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]

Result:
no goals

Proof state:
case pos.intro.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝¹ : Invertible (diagonal v)
val✝ : Invertible v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Tactic:
rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Tactic:
by_cases h : IsUnit v

Result:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Proof state:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝ : Invertible (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Tactic:
cases h.nonempty_invertible

Result:
case pos.intro.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝¹ : Invertible (diagonal v)
val✝ : Invertible v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Proof state:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)

Tactic:
have := isUnit_diagonal.not.mpr h

Result:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)