awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this_1 : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ i : κ, HSMul.hSMul (β := M) (w i) (∑ j : ι, A i j • v j)) 0
this : w = 0
⊢ ∀ (i : κ), w i = 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ i : κ, HSMul.hSMul (β := M) (w i) (∑ j : ι, A i j • v j)) 0
suffices : w = 0
⊢ ∀ (i : κ), w i = 0

Tactic:
suffices w = 0 by aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ i : κ, HSMul.hSMul (β := M) (w i) (∑ j : ι, A i j • v j)) 0
⊢ Eq.{u_4 + 1} (α := M) (∑ x : κ, ∑ x_1 : ι, (w x • A x x_1) • v x_1) 0

Tactic:
simp_rw [Finset.smul_sum, ← smul_assoc] at hw

Premises used: smul_assoc, Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : κ, ∑ x_1 : ι, (w x • A x x_1) • v x_1) 0
⊢ Eq.{u_4 + 1} (α := M) (∑ y : ι, ∑ x : κ, (w x • A x y) • v y) 0

Tactic:
rw [Finset.sum_comm] at hw

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ y : ι, ∑ x : κ, (w x • A x y) • v y) 0
⊢ Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0

Tactic:
simp_rw [← Finset.sum_smul] at hw

Premises used: Finset.sum_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
⊢ w ᵥ* A = 0

Tactic:
replace hv : w ᵥ* A = 0 := funext <| hv _ hw
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
hv : w ᵥ* A = 0
w' : ι → R
⊢ w ⬝ᵥ A *ᵥ w' = 0

Tactic:
simpa [Matrix.dotProduct_mulVec] using congr_arg (fun x ↦ dotProduct x w') hv

Premises used: dotProduct, congr_arg, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
hv : w ᵥ* A = 0
⊢ ∀ (w' : ι → R), w ⬝ᵥ A *ᵥ w' = 0

Tactic:
replace hv (w' : ι → R) : w ⬝ᵥ A *ᵥ w' = 0 := by
    simpa [Matrix.dotProduct_mulVec] using congr_arg (fun x ↦ dotProduct x w') hv
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
hv : ∀ (w' : ι → R), w ⬝ᵥ A *ᵥ w' = 0
⊢ w = 0

Tactic:
hA.eq_zero_of_ortho hv

Premises used: Matrix.Nondegenerate.eq_zero_of_ortho
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
hv : ∀ (w' : ι → R), w ⬝ᵥ A *ᵥ w' = 0
⊢ w = 0

Tactic:
exact hA.eq_zero_of_ortho hv

Premises used: Matrix.Nondegenerate.eq_zero_of_ortho
-- 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 α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A.adjugate * A) = 1
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
rw₂ : HSMul.hSMul (β := Matrix n n α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ * A.det) 1 = 1
rw₃ : HSMul.hSMul (α := α) (β := Matrix n n α) 1 1 = 1
rw₄ rw₅ : Eq (α := Matrix n n α) 1 1
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate * A = 1

Tactic:
rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]

Premises used: smul_smul, invOf_mul_self, smul_mul_assoc, one_smul, Matrix.adjugate_mul
-- 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 α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A * A.adjugate) = 1
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
rw₂ : HSMul.hSMul (β := Matrix n n α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ * A.det) 1 = 1
rw₃ : HSMul.hSMul (α := α) (β := Matrix n n α) 1 1 = 1
rw₄ rw₅ : Eq (α := Matrix n n α) 1 1
⊢ A * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate = 1

Tactic:
rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]

Premises used: smul_smul, invOf_mul_self, one_smul, mul_smul_comm, Matrix.mul_adjugate
-- 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
inst_4 : Invertible A
this : Invertible A := A.invertibleOfDetInvertible
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _

Tactic:
(rfl : ⅟A = _)

Premises used: rfl
-- 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
inst_4 : Invertible A
this : Invertible A := A.invertibleOfDetInvertible
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate

Tactic:
convert! (rfl : ⅟A = _)

Premises used: 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 α
h : B * A = 1
rw : (B * A).det = 1
rw₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
rw₂ rw₃ : Eq.{v + 1} (α := α) 1 1
⊢ B.det * A.det = 1

Tactic:
rw [← det_mul, h, det_one]

Premises used: Matrix.det_mul, Matrix.det_one
-- 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 α
h : B * A = 1
rw : B.det * A.det = 1
rw₁ : (B * A).det = 1
rw₂ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
rw₃ rw₄ : Eq.{v + 1} (α := α) 1 1
⊢ A.det * B.det = 1

Tactic:
rw [mul_comm, ← det_mul, h, det_one]

Premises used: Matrix.det_mul, mul_comm, Matrix.det_one
-- 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 α
h : A * B = 1
rw : A.det * B.det = 1
rw₁ : (A * B).det = 1
rw₂ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
rw₃ rw₄ : Eq.{v + 1} (α := α) 1 1
⊢ B.det * A.det = 1

Tactic:
rw [mul_comm, ← det_mul, h, det_one]

Premises used: Matrix.det_mul, mul_comm, Matrix.det_one
-- 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 α
h : A * B = 1
rw : (A * B).det = 1
rw₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
rw₂ rw₃ : Eq.{v + 1} (α := α) 1 1
⊢ A.det * B.det = 1

Tactic:
rw [← det_mul, h, det_one]

Premises used: 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 α
inst_3 : Invertible A
inst_4 : Invertible A.det
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _

Tactic:
(rfl : _ = ⅟A.det)

Premises used: rfl
-- 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
inst_4 : Invertible A.det
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).det =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _

Tactic:
convert! (rfl : _ = ⅟A.det)

Premises used: rfl
-- 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 α
⊢ IsUnit A ↔ IsUnit A.det

Tactic:
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr]

Premises used: nonempty_invertible_iff_isUnit, Equiv.nonempty_congr, Matrix.invertibleEquivDetInvertible
-- 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 α)ˣ
⊢ IsUnit (↑A : Matrix n n α).det

Tactic:
isUnit_iff_isUnit_det _ |>.mp A.isUnit

Premises used: Matrix.isUnit_iff_isUnit_det, Iff.mp, Units.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 α
inst_3 : Invertible A
⊢ IsUnit A.det

Tactic:
@isUnit_of_invertible _ _ _ (detInvertibleOfInvertible A)

Premises used: isUnit_of_invertible
-- 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
⊢ IsUnit A.det

Tactic:
@isUnit_of_invertible _ _ _ (detInvertibleOfLeftInverse _ _ h)

Premises used: isUnit_of_invertible
-- 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
⊢ IsUnit A.det

Tactic:
@isUnit_of_invertible _ _ _ (detInvertibleOfRightInverse _ _ h)

Premises used: isUnit_of_invertible
-- 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 α
inst_3 : Nontrivial α
h : B * A = 1
⊢ A.det ≠ 0

Tactic:
(isUnit_det_of_left_inverse h).ne_zero

Premises used: Matrix.isUnit_det_of_left_inverse, IsUnit.ne_zero
-- 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 α
inst_3 : Nontrivial α
h : A * B = 1
⊢ A.det ≠ 0

Tactic:
(isUnit_det_of_right_inverse h).ne_zero

Premises used: IsUnit.ne_zero, Matrix.isUnit_det_of_right_inverse
-- 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 rw : IsUnit A.det
⊢ IsUnit Aᵀ.det

Tactic:
rw [det_transpose]

Premises used: Matrix.det_transpose
-- 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:
h
-- 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:
exact h
-- 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 α
⊢ A⁻¹ = A.det⁻¹ʳ • A.adjugate

Tactic:
rfl

Premises used: rfl
-- 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.det⁻¹ʳ • A.adjugate = 0
rw₁ : HSMul.hSMul (α := α) 0 A.adjugate = 0
rw₂ rw₃ : Eq (α := Matrix n n α) 0 0
⊢ A⁻¹ = 0

Tactic:
rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]

Premises used: Matrix.inv_def, Ring.inverse_non_unit, zero_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
rw : A.det⁻¹ʳ • A.adjugate = (↑h.unit⁻¹ : α) • A.adjugate
rw₁ : A.det⁻¹ʳ • A.adjugate = (↑h.unit : α)⁻¹ʳ • A.adjugate
rw₂ rw₃ : A.det⁻¹ʳ • A.adjugate = A.det⁻¹ʳ • A.adjugate
⊢ A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate

Tactic:
rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]

Premises used: Matrix.inv_def, Ring.inverse_unit, IsUnit.unit, IsUnit.unit_spec
-- 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
this : Invertible A.det := A.detInvertibleOfInvertible
rw : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A.det⁻¹ʳ • A.adjugate
rw₁ :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _ • A.adjugate
rw₂ rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate =
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _ • A.adjugate
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A⁻¹

Tactic:
rw [inv_def, Ring.inverse_invertible, invOf_eq]

Premises used: Ring.inverse_invertible, Matrix.inv_def, Matrix.invOf_eq
-- 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 α)ˣ
this : Invertible (↑A : Matrix n n α) := A.invertible
rw : (↑A⁻¹ : Matrix n n α) = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (↑A : Matrix n n α) _
rw₁ rw₂ : (↑A⁻¹ : Matrix n n α) = (↑A⁻¹ : Matrix n n α)
⊢ (↑A⁻¹ : Matrix n n α) = (↑A : Matrix n n α)⁻¹

Tactic:
rw [← invOf_eq_nonsing_inv, invOf_units]

Premises used: Matrix.invOf_eq_nonsing_inv, invOf_units
-- 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_det : IsUnit A.det), A⁻¹ = A⁻¹ʳ
neg : ∀ (h_det : ¬IsUnit A.det), A⁻¹ = A⁻¹ʳ
⊢ A⁻¹ = A⁻¹ʳ

Tactic:
by_cases h_det : 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_det : IsUnit A.det
pos : ∀ (val : Invertible A), A⁻¹ = A⁻¹ʳ
⊢ A⁻¹ = A⁻¹ʳ

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible

Premises used: Iff.mpr, IsUnit.nonempty_invertible, 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 α
h_det : IsUnit A.det
val : Invertible A
pos : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A⁻¹ʳ
pos₁ pos₂ :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A _
⊢ A⁻¹ = A⁻¹ʳ

Tactic:
rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]

Premises used: Ring.inverse_invertible, Matrix.invOf_eq_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_det : ¬IsUnit A.det
⊢ ¬IsUnit A

Tactic:
have h := mt A.isUnit_iff_isUnit_det.mp h_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_det : ¬IsUnit A.det
h : ¬IsUnit A
neg : A⁻¹ = 0
neg₁ neg₂ : Eq (α := Matrix n n α) 0 0
⊢ A⁻¹ = A⁻¹ʳ

Tactic:
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]

Premises used: 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 α
rw : (A.det⁻¹ʳ • A.adjugate)ᵀ = Aᵀ⁻¹
rw₁ : (A.det⁻¹ʳ • A.adjugate)ᵀ = Aᵀ.det⁻¹ʳ • Aᵀ.adjugate
rw₂ : A.det⁻¹ʳ • A.adjugateᵀ = Aᵀ.det⁻¹ʳ • Aᵀ.adjugate
rw₃ : A.det⁻¹ʳ • A.adjugateᵀ = A.det⁻¹ʳ • Aᵀ.adjugate
rw₄ rw₅ : A.det⁻¹ʳ • Aᵀ.adjugate = A.det⁻¹ʳ • Aᵀ.adjugate
⊢ A⁻¹ᵀ = Aᵀ⁻¹

Tactic:
rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]

Premises used: Matrix.det_transpose, Matrix.inv_def, Matrix.transpose_smul, Matrix.adjugate_transpose
-- 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 : StarRing α
rw : (A.det⁻¹ʳ • A.adjugate)ᴴ = Aᴴ⁻¹
rw₁ : (A.det⁻¹ʳ • A.adjugate)ᴴ = Aᴴ.det⁻¹ʳ • Aᴴ.adjugate
rw₂ : star A.det⁻¹ʳ • A.adjugateᴴ = Aᴴ.det⁻¹ʳ • Aᴴ.adjugate
rw₃ : star A.det⁻¹ʳ • A.adjugateᴴ = (star A.det)⁻¹ʳ • Aᴴ.adjugate
rw₄ : star A.det⁻¹ʳ • Aᴴ.adjugate = (star A.det)⁻¹ʳ • Aᴴ.adjugate
rw₅ rw₆ : star A.det⁻¹ʳ • Aᴴ.adjugate = star A.det⁻¹ʳ • Aᴴ.adjugate
⊢ A⁻¹ᴴ = Aᴴ⁻¹

Tactic:
rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]

Premises used: Matrix.det_conjTranspose, Matrix.inv_def, Matrix.adjugate_conjTranspose, Ring.inverse_star, Matrix.conjTranspose_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
intro : ∀ (val : Invertible A), A * A⁻¹ = 1
⊢ A * A⁻¹ = 1

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible

Premises used: Iff.mpr, IsUnit.nonempty_invertible, 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 α
h : IsUnit A.det
val : Invertible A
intro : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = 1
intro₁ intro₂ : Eq (α := Matrix n n α) 1 1
⊢ A * A⁻¹ = 1

Tactic:
rw [← invOf_eq_nonsing_inv, mul_invOf_self]

Premises used: Matrix.invOf_eq_nonsing_inv, mul_invOf_self
-- 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
intro : ∀ (val : Invertible A), A⁻¹ * A = 1
⊢ A⁻¹ * A = 1

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible

Premises used: Iff.mpr, IsUnit.nonempty_invertible, 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 α
h : IsUnit A.det
val : Invertible A
intro : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A = 1
intro₁ intro₂ : Eq (α := Matrix n n α) 1 1
⊢ A⁻¹ * A = 1

Tactic:
rw [← invOf_eq_nonsing_inv, invOf_mul_self]

Premises used: Matrix.invOf_eq_nonsing_inv, invOf_mul_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 α
inst_3 : Invertible A
rw : Invertible (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
⊢ Invertible A⁻¹

Tactic:
rw [← invOf_eq_nonsing_inv]

Premises used: Matrix.invOf_eq_nonsing_inv
-- 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 α
inst_3 : Invertible A
⊢ Invertible (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)

Tactic:
infer_instance
-- 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
⊢ A⁻¹⁻¹ = A

Tactic:
simp only [← invOf_eq_nonsing_inv, invOf_invOf]

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

Tactic:
simp [Matrix.mul_assoc, mul_nonsing_inv A h]

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

Tactic:
simp [← Matrix.mul_assoc, mul_nonsing_inv A h]

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

Tactic:
simp [Matrix.mul_assoc, nonsing_inv_mul A h]

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

Tactic:
simp [← Matrix.mul_assoc, nonsing_inv_mul A h]

Premises used: Matrix.mul_assoc, Matrix.nonsing_inv_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 α
inst_3 : Invertible A
⊢ A * A⁻¹ = 1

Tactic:
mul_nonsing_inv A (isUnit_det_of_invertible A)

Premises used: Matrix.isUnit_det_of_invertible, Matrix.mul_nonsing_inv