awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩

Premises used: Or.inl
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
Or.inr (nonsing_inv_apply_not_isUnit _ h)

Premises used: Matrix.nonsing_inv_apply_not_isUnit, Or.inr
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
exact Or.inr (nonsing_inv_apply_not_isUnit _ h)

Premises used: Matrix.nonsing_inv_apply_not_isUnit, Or.inr
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
rw : (A⁻¹ * A).det = 1
rw₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
rw₂ rw₃ : Eq.{v + 1} (α := α) 1 1
⊢ A⁻¹.det * A.det = 1

Tactic:
rw [← det_mul, A.nonsing_inv_mul h, det_one]

Premises used: Matrix.nonsing_inv_mul, Matrix.det_mul, Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
pos : ∀ (h : IsUnit A.det), A⁻¹.det = A.det⁻¹ʳ
neg : ∀ (h : ¬IsUnit A.det), A⁻¹.det = A.det⁻¹ʳ
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
by_cases h : IsUnit A.det

Premises used: IsUnit, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
pos : ∀ (val : Invertible A.det), A⁻¹.det = A.det⁻¹ʳ
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
cases h.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
val : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
pos : A⁻¹.det = @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
pos₁ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).det =
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
pos₂ pos₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ =
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]

Premises used: Ring.inverse_invertible, Matrix.invOf_eq_nonsing_inv, Matrix.det_invOf
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
neg : IsEmpty n → A⁻¹.det = A.det⁻¹ʳ
neg₁ : Nonempty n → A⁻¹.det = A.det⁻¹ʳ
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h_1 : IsEmpty n
neg : 1 = A.det⁻¹ʳ
neg₁ : Eq.{v + 1} (α := α) 1 1⁻¹ʳ
neg₂ neg₃ : Eq.{v + 1} (α := α) 1 1
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
rw [det_isEmpty, det_isEmpty, Ring.inverse_one]

Premises used: Ring.inverse_one, Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h_1 : Nonempty n
neg : A⁻¹.det = 0
neg₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 0) 0
neg₂ neg₃ : Eq.{v + 1} (α := α) 0 0
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]

Premises used: Matrix.det_zero, Ring.inverse_non_unit, Matrix.nonsing_inv_apply_not_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ IsUnit A⁻¹.det

Tactic:
.of_mul_eq_one _ (A.det_nonsing_inv_mul_det h)

Premises used: IsUnit.of_mul_eq_one, Matrix.det_nonsing_inv_mul_det
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
rw rw₁ : A⁻¹⁻¹ = A⁻¹⁻¹
⊢ A⁻¹⁻¹ = 1 * A⁻¹⁻¹

Tactic:
rw [Matrix.one_mul]

Premises used: Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
rw rw₁ : 1 * A⁻¹⁻¹ = 1 * A⁻¹⁻¹
⊢ 1 * A⁻¹⁻¹ = A * A⁻¹ * A⁻¹⁻¹

Tactic:
rw [A.mul_nonsing_inv h]

Premises used: Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
rw : A * (A⁻¹ * A⁻¹⁻¹) = A
rw₁ : A * 1 = A
rw₂ rw₃ : A = A
⊢ A * A⁻¹ * A⁻¹⁻¹ = A

Tactic:
rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]

Premises used: Matrix.mul_assoc, Inv.inv, Matrix.mul_one, Matrix.mul_nonsing_inv, Matrix.isUnit_nonsing_inv_det
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
rw : IsUnit A.det⁻¹ʳ ↔ IsUnit A.det
rw₁ rw₂ : IsUnit A.det ↔ IsUnit A.det
⊢ IsUnit A⁻¹.det ↔ IsUnit A.det

Tactic:
rw [Matrix.det_nonsing_inv, isUnit_ringInverse]

Premises used: isUnit_ringInverse, Matrix.det_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
simp_rw : IsUnit A⁻¹.det ↔ IsUnit A.det
⊢ IsUnit A⁻¹ ↔ IsUnit A

Tactic:
simp_rw [isUnit_iff_isUnit_det, isUnit_nonsing_inv_det_iff]

Premises used: Matrix.isUnit_nonsing_inv_det_iff, Matrix.isUnit_iff_isUnit_det
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A.det
huv : ∀ (i j : n), (↑A.unitOfDetInvertible : Matrix n n α) i j = (↑(A.nonsingInvUnit ⋯) : Matrix n n α) i j
⊢ A.unitOfDetInvertible = A.nonsingInvUnit ⋯

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A.det
i j : n
⊢ (↑A.unitOfDetInvertible : Matrix n n α) i j = (↑(A.nonsingInvUnit ⋯) : Matrix n n α) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ A⁻¹ = B

Tactic:
letI := invertibleOfLeftInverse _ _ h
  invOf_eq_nonsing_inv A ▸ invOf_eq_left_inv h

Premises used: Matrix.invOf_eq_nonsing_inv, Eq.rec, invOf_eq_left_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ A⁻¹ = B

Tactic:
inv_eq_left_inv (mul_eq_one_comm.2 h)

Premises used: Iff.mpr, Matrix.inv_eq_left_inv, mul_eq_one_comm
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B C : Matrix n n α
h : B * A = 1
g : C * A = 1
rw : A⁻¹ = C
rw₁ rw₂ : A⁻¹ = A⁻¹
⊢ B = C

Tactic:
rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]

Premises used: Matrix.inv_eq_left_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
rw : A⁻¹ = C
rw₁ rw₂ : A⁻¹ = A⁻¹
⊢ B = C

Tactic:
rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]

Premises used: Matrix.inv_eq_right_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : C * A = 1
rw : A⁻¹ = C
rw₁ rw₂ : A⁻¹ = A⁻¹
⊢ B = C

Tactic:
rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]

Premises used: Matrix.inv_eq_right_inv, Matrix.inv_eq_left_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ A = B

Tactic:
left_inv_eq_left_inv (mul_nonsing_inv _ h') ?_

Premises used: Matrix.left_inv_eq_left_inv, Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
refine : B * A⁻¹ = 1
⊢ A = B

Tactic:
refine left_inv_eq_left_inv (mul_nonsing_inv _ h') ?_

Premises used: Matrix.left_inv_eq_left_inv, Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
rw : B * B⁻¹ = 1
⊢ B * A⁻¹ = 1

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * B⁻¹ = 1

Tactic:
mul_nonsing_inv _ ?_

Premises used: Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
refine : IsUnit B.det
⊢ B * B⁻¹ = 1

Tactic:
refine mul_nonsing_inv _ ?_

Premises used: Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
rwa : IsUnit B⁻¹.det
rwa₁ : IsUnit A⁻¹.det
rwa₂ rwa₃ rwa₄ rwa₅ : IsUnit A.det
⊢ IsUnit B.det

Tactic:
rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]

Premises used: Matrix.isUnit_nonsing_inv_det_iff
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inl : ∀ (ht : Subsingleton α), Eq (α := Matrix n n α) 0⁻¹ 0
inr : ∀ (ht : Nontrivial α), Eq (α := Matrix n n α) 0⁻¹ 0
⊢ Eq (α := Matrix n n α) 0⁻¹ 0

Tactic:
rcases subsingleton_or_nontrivial α with ht | ht

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Subsingleton α
⊢ Eq (α := Matrix n n α) 0⁻¹ 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Nontrivial α
inr : ∀ (hc : 0 = Fintype.card n), Eq (α := Matrix n n α) 0⁻¹ 0
inr₁ : ∀ (hc : 0 < Fintype.card n), Eq (α := Matrix n n α) 0⁻¹ 0
⊢ Eq (α := Matrix n n α) 0⁻¹ 0

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

Premises used: Nat.zero_le, LE.le.eq_or_lt, Fintype.card
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Nontrivial α
hc : 0 = Fintype.card n
⊢ IsEmpty n

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

Premises used: eq_comm, Fintype.card_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Nontrivial α
hc : IsEmpty n
⊢ Eq (α := Matrix n n α) 0⁻¹ 0

Tactic:
subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
⊢ Nonempty n

Tactic:
have hn : Nonempty n := Fintype.card_pos_iff.mp hc
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ Eq (α := Matrix n n α) 0⁻¹ 0

Tactic:
nonsing_inv_apply_not_isUnit _ ?_

Premises used: Matrix.nonsing_inv_apply_not_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
inr : ¬IsUnit.{v} (M := α) (det.{v, u'} (n := n) 0)
⊢ Eq (α := Matrix n n α) 0⁻¹ 0

Tactic:
refine nonsing_inv_apply_not_isUnit _ ?_

Premises used: Matrix.nonsing_inv_apply_not_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ ¬IsUnit.{v} (M := α) (det.{v, u'} (n := n) 0)

Tactic:
simp [det]

Premises used: Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
⊢ HMul.hMul (α := Matrix n n α) 1 1 = 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
k : α
inst_3 : Invertible k
h : IsUnit A.det
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne k _ • A⁻¹ * k • A = 1

Tactic:
simp [h, smul_smul]

Premises used: smul_smul
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
k : αˣ
h : IsUnit A.det
⊢ k⁻¹ • A⁻¹ * k • A = 1

Tactic:
simp [h, smul_smul]

Premises used: smul_smul
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A.adjugate⁻¹ = h.unit⁻¹ • A

Tactic:
inv_eq_left_inv ?_

Premises used: Matrix.inv_eq_left_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
refine : h.unit⁻¹ • A * A.adjugate = 1
⊢ A.adjugate⁻¹ = h.unit⁻¹ • A

Tactic:
refine inv_eq_left_inv ?_

Premises used: Matrix.inv_eq_left_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
rw : h.unit⁻¹ • (A * A.adjugate) = 1
rw₁ : h.unit⁻¹ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
rw₂ : (↑h.unit⁻¹ : α) • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
rw₃ : HSMul.hSMul (β := Matrix n n α) ((↑h.unit⁻¹ : α) * A.det) 1 = 1
rw₄ : HSMul.hSMul (α := α) (β := Matrix n n α) 1 1 = 1
rw₅ rw₆ : Eq (α := Matrix n n α) 1 1
⊢ h.unit⁻¹ • A * A.adjugate = 1

Tactic:
rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]

Premises used: smul_smul, one_smul, Units.smul_def, Matrix.smul_mul, IsUnit.val_inv_mul, Matrix.mul_adjugate
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
inst : Fintype n
inst_1 : DecidableEq n
α : Type u_2
inst_2 : Semiring α
v : n → α
inst_3 : Invertible v
inst_4 : Invertible (diagonal v)
rw :
  @Invertible.invOf _ MulOne.toMul MulOne.toOne (diagonal v) _ =
    diagonal (@Invertible.invOf _ (Pi.instMul (M := fun (a : n) ↦ α)) (Pi.instOne (M := fun (a : n) ↦ α)) v _)
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (diagonal v) _ =
    diagonal (@Invertible.invOf _ (Pi.instMul (M := fun (a : n) ↦ α)) (Pi.instOne (M := fun (a : n) ↦ α)) v _)

Tactic:
rw [@Invertible.congr _ _ _ _ _ (diagonalInvertible v) rfl]

Premises used: Invertible.congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
inst : Fintype n
inst_1 : DecidableEq n
α : Type u_2
inst_2 : Semiring α
v : n → α
inst_3 : Invertible v
inst_4 : Invertible (diagonal v)
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne (diagonal v) _ =
    diagonal (@Invertible.invOf _ (Pi.instMul (M := fun (a : n) ↦ α)) (Pi.instOne (M := fun (a : n) ↦ α)) v _)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
rw :
  ((HSMul.hSMul (β := (i : n) → α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _)
          fun (i : n) ↦ ∏ j ∈ erase univ i, v j) *
        v)
      i =
    1 i
⊢ ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (diagonal v) _).diag * v) i = 1 i

Tactic:
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]

Premises used: Matrix.diag_smul, Matrix.diag_diagonal, Matrix.adjugate_diagonal, Matrix.invOf_eq
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
dsimp :
  (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * ∏ j ∈ erase univ i, v j) * v i = 1
⊢ ((HSMul.hSMul (β := (i : n) → α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _)
          fun (i : n) ↦ ∏ j ∈ erase univ i, v j) *
        v)
      i =
    1 i

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * (diagonal v).det = 1
⊢ (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * ∏ j ∈ erase univ i, v j) * v i = 1

Tactic:
rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal]

Premises used: Finset.mem_univ, Finset.prod_erase_mul, mul_assoc, Matrix.det_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * (diagonal v).det = 1

Tactic:
mul_invOf_self _

Premises used: mul_invOf_self
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * (diagonal v).det = 1

Tactic:
exact mul_invOf_self _

Premises used: mul_invOf_self
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
rw :
  (v *
        HSMul.hSMul (β := (i : n) → α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _)
          fun (i : n) ↦ ∏ j ∈ erase univ i, v j)
      i =
    1 i
⊢ (v * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (diagonal v) _).diag) i = 1 i

Tactic:
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]

Premises used: Matrix.diag_smul, Matrix.diag_diagonal, Matrix.adjugate_diagonal, Matrix.invOf_eq
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
dsimp :
  v i * (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * ∏ j ∈ erase univ i, v j) = 1
⊢ (v *
        HSMul.hSMul (β := (i : n) → α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _)
          fun (i : n) ↦ ∏ j ∈ erase univ i, v j)
      i =
    1 i

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * (diagonal v).det = 1
⊢ v i * (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * ∏ j ∈ erase univ i, v j) = 1

Tactic:
rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]

Premises used: Finset.mem_univ, Finset.mul_prod_erase, mul_left_comm, Matrix.det_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
⊢ IsUnit (diagonal v) ↔ IsUnit v

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (diagonalInvertibleEquivInvertible v).nonempty_congr]

Premises used: Matrix.diagonalInvertibleEquivInvertible, nonempty_invertible_iff_isUnit, Equiv.nonempty_congr
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
rw : (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
⊢ (diagonal v)⁻¹ = diagonal v⁻¹ʳ

Tactic:
rw [nonsing_inv_eq_ringInverse]

Premises used: Matrix.nonsing_inv_eq_ringInverse
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
pos : ∀ (h : IsUnit v), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
neg : ∀ (h : ¬IsUnit v), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
by_cases h : IsUnit v

Premises used: IsUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
h : IsUnit v
⊢ IsUnit (diagonal v)

Tactic:
have := isUnit_diagonal.mpr h
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
pos : ∀ (val : Invertible (diagonal v)), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
cases this.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val : Invertible (diagonal v)
pos : ∀ (val : Invertible v), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
cases h.nonempty_invertible

Premises used: IsUnit.nonempty_invertible