-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0

Proof state:
case inr.inl.a
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc this : IsEmpty n
i j✝ : n
⊢ 0⁻¹ i j✝ = 0 i j✝

Tactic:
exact (IsEmpty.false i).elim

Result:
no goals

Proof state:
case inr.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : IsEmpty n
⊢ 0⁻¹ = 0

Tactic:
haveI := hc

Result:
case inr.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc this : IsEmpty n
⊢ 0⁻¹ = 0

Proof state:
case inr.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 = Fintype.card n
⊢ 0⁻¹ = 0

Tactic:
rw [eq_comm, Fintype.card_eq_zero_iff] at hc

Result:
case inr.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : IsEmpty n
⊢ 0⁻¹ = 0

Proof state:
case inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Subsingleton α
⊢ 0⁻¹ = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case inr.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ 0⁻¹ = 0

Tactic:
refine nonsing_inv_apply_not_isUnit _ ?_

Result:
case inr.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ ¬IsUnit (det 0)

Proof state:
case inr.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
⊢ 0⁻¹ = 0

Tactic:
have hn : Nonempty n := Fintype.card_pos_iff.mp hc

Result:
case inr.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ 0⁻¹ = 0

Proof state:
case inr.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc this : IsEmpty n
⊢ 0⁻¹ = 0

Tactic:
ext i

Result:
case inr.inl.a
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc this : IsEmpty n
i j✝ : n
⊢ 0⁻¹ i j✝ = 0 i j✝

Proof state:
case inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
⊢ 0⁻¹ = 0

Tactic:
rcases (Fintype.card n).zero_le.eq_or_lt with hc | hc

Result:
case inr.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 = Fintype.card n
⊢ 0⁻¹ = 0

case inr.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
⊢ 0⁻¹ = 0

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
⊢ 0⁻¹ = 0

Tactic:
rcases subsingleton_or_nontrivial α with ht | ht

Result:
case inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Subsingleton α
⊢ 0⁻¹ = 0

case inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
⊢ 0⁻¹ = 0

Proof state:
case inr.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ ¬IsUnit (det 0)

Tactic:
simp [hn]

Result:
no goals