awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate = 1
have rw₃ : HSMul.hSMul (α := α) (β := Matrix n n α) 1 1 = 1
Tactic: rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate = 1
have rw₄ : Eq (α := Matrix n n α) 1 1
Tactic: rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ B.det * A.det = 1
have rw : (B * A).det = 1
Tactic: rw [← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ B.det * A.det = 1
have rw₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
Tactic: rw [← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ B.det * A.det = 1
have rw₂ : Eq.{v + 1} (α := α) 1 1
Tactic: rw [← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det * B.det = 1
have rw : B.det * A.det = 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det * B.det = 1
have rw₁ : (B * A).det = 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det * B.det = 1
have rw₂ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det * B.det = 1
have rw₃ : Eq.{v + 1} (α := α) 1 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ B.det * A.det = 1
have rw : A.det * B.det = 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ B.det * A.det = 1
have rw₁ : (A * B).det = 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ B.det * A.det = 1
have rw₂ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ B.det * A.det = 1
have rw₃ : Eq.{v + 1} (α := α) 1 1
Tactic: rw [mul_comm, ← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det * B.det = 1
have rw : (A * B).det = 1
Tactic: rw [← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det * B.det = 1
have rw₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
Tactic: rw [← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det * B.det = 1
have rw₂ : Eq.{v + 1} (α := α) 1 1
Tactic: rw [← det_mul, h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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⁻¹ = 0
have rw : A.det⁻¹ʳ • A.adjugate = 0
Tactic: rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = 0
have rw₁ : HSMul.hSMul (α := α) 0 A.adjugate = 0
Tactic: rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = 0
have rw₂ : Eq (α := Matrix n n α) 0 0
Tactic: rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate
have rw : A.det⁻¹ʳ • A.adjugate = (↑h.unit⁻¹ : α) • A.adjugate
Tactic: rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate
have rw₁ : A.det⁻¹ʳ • A.adjugate = (↑h.unit : α)⁻¹ʳ • A.adjugate
Tactic: rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate
have rw₂ : A.det⁻¹ʳ • A.adjugate = A.det⁻¹ʳ • A.adjugate
Tactic: rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A⁻¹
have rw : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A.det⁻¹ʳ • A.adjugate
Tactic: rw [inv_def, Ring.inverse_invertible, invOf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A⁻¹
have rw₁ : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _ • A.adjugate
Tactic: rw [inv_def, Ring.inverse_invertible, invOf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A⁻¹
have rw₂ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate =
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _ • A.adjugate
Tactic: rw [inv_def, Ring.inverse_invertible, invOf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ (↑A⁻¹ : Matrix n n α) = (↑A : Matrix n n α)⁻¹
have rw : (↑A⁻¹ : Matrix n n α) = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (↑A : Matrix n n α) _
Tactic: rw [← invOf_eq_nonsing_inv, invOf_units]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 α) _
⊢ (↑A⁻¹ : Matrix n n α) = (↑A : Matrix n n α)⁻¹
have rw₁ : (↑A⁻¹ : Matrix n n α) = (↑A⁻¹ : Matrix n n α)
Tactic: rw [← invOf_eq_nonsing_inv, invOf_units]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
⊢ A⁻¹ = A⁻¹ʳ
have pos : ∀ (h_det : IsUnit A.det), A⁻¹ = A⁻¹ʳ
Tactic: by_cases h_det : IsUnit A.det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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⁻¹ʳ
⊢ A⁻¹ = A⁻¹ʳ
have neg : ∀ (h_det : ¬IsUnit A.det), A⁻¹ = A⁻¹ʳ
Tactic: by_cases h_det : IsUnit A.det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = A⁻¹ʳ
have pos : ∀ (val : Invertible A), A⁻¹ = A⁻¹ʳ
Tactic: cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = A⁻¹ʳ
have pos : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = A⁻¹ʳ
Tactic: rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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⁻¹ʳ
⊢ A⁻¹ = A⁻¹ʳ
have pos₁ : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A _
Tactic: rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (hypothesis)
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
⊢ A⁻¹ = A⁻¹ʳ
have h : ¬IsUnit A
Tactic: have h := mt A.isUnit_iff_isUnit_det.mp h_det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = A⁻¹ʳ
have neg : A⁻¹ = 0
Tactic: rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ = A⁻¹ʳ
have neg₁ : Eq (α := Matrix n n α) 0 0
Tactic: rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
⊢ A⁻¹ᵀ = Aᵀ⁻¹
have rw : (A.det⁻¹ʳ • A.adjugate)ᵀ = Aᵀ⁻¹
Tactic: rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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ᵀ⁻¹
⊢ A⁻¹ᵀ = Aᵀ⁻¹
have rw₁ : (A.det⁻¹ʳ • A.adjugate)ᵀ = Aᵀ.det⁻¹ʳ • Aᵀ.adjugate
Tactic: rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ᵀ = Aᵀ⁻¹
have rw₂ : A.det⁻¹ʳ • A.adjugateᵀ = Aᵀ.det⁻¹ʳ • Aᵀ.adjugate
Tactic: rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ᵀ = Aᵀ⁻¹
have rw₃ : A.det⁻¹ʳ • A.adjugateᵀ = A.det⁻¹ʳ • Aᵀ.adjugate
Tactic: rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ᵀ = Aᵀ⁻¹
have rw₄ : A.det⁻¹ʳ • Aᵀ.adjugate = A.det⁻¹ʳ • Aᵀ.adjugate
Tactic: rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : StarRing α
⊢ A⁻¹ᴴ = Aᴴ⁻¹
have rw : (A.det⁻¹ʳ • A.adjugate)ᴴ = Aᴴ⁻¹
Tactic: rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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ᴴ⁻¹
⊢ A⁻¹ᴴ = Aᴴ⁻¹
have rw₁ : (A.det⁻¹ʳ • A.adjugate)ᴴ = Aᴴ.det⁻¹ʳ • Aᴴ.adjugate
Tactic: rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ᴴ = Aᴴ⁻¹
have rw₂ : star A.det⁻¹ʳ • A.adjugateᴴ = Aᴴ.det⁻¹ʳ • Aᴴ.adjugate
Tactic: rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ᴴ = Aᴴ⁻¹
have rw₃ : star A.det⁻¹ʳ • A.adjugateᴴ = (star A.det)⁻¹ʳ • Aᴴ.adjugate
Tactic: rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ᴴ = Aᴴ⁻¹
have rw₄ : star A.det⁻¹ʳ • Aᴴ.adjugate = (star A.det)⁻¹ʳ • Aᴴ.adjugate
Tactic: rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ᴴ = Aᴴ⁻¹
have rw₅ : star A.det⁻¹ʳ • Aᴴ.adjugate = star A.det⁻¹ʳ • Aᴴ.adjugate
Tactic: rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
have intro : ∀ (val : Invertible A), A * A⁻¹ = 1
Tactic: cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A * A⁻¹ = 1
have intro : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ = 1
Tactic: rw [← invOf_eq_nonsing_inv, mul_invOf_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A * A⁻¹ = 1
have intro₁ : Eq (α := Matrix n n α) 1 1
Tactic: rw [← invOf_eq_nonsing_inv, mul_invOf_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
have intro : ∀ (val : Invertible A), A⁻¹ * A = 1
Tactic: cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ * A = 1
have intro : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A = 1
Tactic: rw [← invOf_eq_nonsing_inv, invOf_mul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A⁻¹ * A = 1
have intro₁ : Eq (α := Matrix n n α) 1 1
Tactic: rw [← invOf_eq_nonsing_inv, invOf_mul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 A⁻¹
have rw : Invertible (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
Tactic: rw [← invOf_eq_nonsing_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix n m α
h : A⁻¹ * B = C
⊢ B = A * C
have rw : B = A * (A⁻¹ * B)
Tactic: rw [← h, mul_inv_cancel_left_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix n m α
h : A⁻¹ * B = C
rw : B = A * (A⁻¹ * B)
⊢ B = A * C
have rw₁ : B = B
Tactic: rw [← h, mul_inv_cancel_left_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix n m α
h : B = A * C
⊢ A⁻¹ * B = C
have rw : A⁻¹ * (A * C) = C
Tactic: rw [h, inv_mul_cancel_left_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix n m α
h : B = A * C
rw : A⁻¹ * (A * C) = C
⊢ A⁻¹ * B = C
have rw₁ : C = C
Tactic: rw [h, inv_mul_cancel_left_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix m n α
h : B * A⁻¹ = C
⊢ B = C * A
have rw : B = B * A⁻¹ * A
Tactic: rw [← h, inv_mul_cancel_right_of_invertible]