awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⁻¹ * A⁻¹⁻¹ = A
have rw : A * (A⁻¹ * A⁻¹⁻¹) = A
Tactic: rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_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
rw : A * (A⁻¹ * A⁻¹⁻¹) = A
⊢ A * A⁻¹ * A⁻¹⁻¹ = A
have rw₁ : A * 1 = A
Tactic: rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_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
rw : A * (A⁻¹ * A⁻¹⁻¹) = A
rw₁ : A * 1 = A
⊢ A * A⁻¹ * A⁻¹⁻¹ = A
have rw₂ : A = A
Tactic: rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_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 α
⊢ IsUnit A⁻¹.det ↔ IsUnit A.det
have rw : IsUnit A.det⁻¹ʳ ↔ IsUnit A.det
Tactic: rw [Matrix.det_nonsing_inv, isUnit_ringInverse]
-- 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 : IsUnit A.det⁻¹ʳ ↔ IsUnit A.det
⊢ IsUnit A⁻¹.det ↔ IsUnit A.det
have rw₁ : IsUnit A.det ↔ IsUnit A.det
Tactic: rw [Matrix.det_nonsing_inv, isUnit_ringInverse]
-- 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 α
⊢ IsUnit A⁻¹ ↔ IsUnit A
have simp_rw : IsUnit A⁻¹.det ↔ IsUnit A.det
Tactic: simp_rw [isUnit_iff_isUnit_det, isUnit_nonsing_inv_det_iff]
-- 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.det
⊢ A.unitOfDetInvertible = A.nonsingInvUnit ⋯
have huv : ∀ (i j : n), (↑A.unitOfDetInvertible : Matrix n n α) i j = (↑(A.nonsingInvUnit sorry) : Matrix n n α) i j
Tactic: ext
-- 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 B C : Matrix n n α
h : B * A = 1
g : C * A = 1
⊢ B = C
have rw : A⁻¹ = C
Tactic: rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]
-- 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 B C : Matrix n n α
h : B * A = 1
g : C * A = 1
rw : A⁻¹ = C
⊢ B = C
have rw₁ : A⁻¹ = A⁻¹
Tactic: rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]
-- 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 B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ B = C
have rw : A⁻¹ = C
Tactic: rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]
-- 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 B C : Matrix n n α
h : A * B = 1
g : A * C = 1
rw : A⁻¹ = C
⊢ B = C
have rw₁ : A⁻¹ = A⁻¹
Tactic: rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]
-- 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 B C : Matrix n n α
h : A * B = 1
g : C * A = 1
⊢ B = C
have rw : A⁻¹ = C
Tactic: rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]
-- 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 B C : Matrix n n α
h : A * B = 1
g : C * A = 1
rw : A⁻¹ = C
⊢ B = C
have rw₁ : A⁻¹ = A⁻¹
Tactic: rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]
-- 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 B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ A = B
have refine : B * A⁻¹ = 1
Tactic: refine left_inv_eq_left_inv (mul_nonsing_inv _ h') ?_
-- 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 B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * A⁻¹ = 1
have rw : B * B⁻¹ = 1
Tactic: rw [h]
-- 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 B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * B⁻¹ = 1
have refine : IsUnit B.det
Tactic: refine mul_nonsing_inv _ ?_
-- 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 B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ IsUnit B.det
have rwa : IsUnit B⁻¹.det
Tactic: rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]
-- 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 B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
rwa : IsUnit B⁻¹.det
⊢ IsUnit B.det
have rwa₁ : IsUnit A⁻¹.det
Tactic: rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]
-- 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 α
⊢ Eq (α := Matrix n n α) 0⁻¹ 0
have inl : ∀ (ht : Subsingleton α), Eq (α := Matrix n n α) 0⁻¹ 0
Tactic: rcases subsingleton_or_nontrivial α with ht | ht
-- 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 α
inl : ∀ (ht : Subsingleton α), Eq (α := Matrix n n α) 0⁻¹ 0
⊢ Eq (α := Matrix n n α) 0⁻¹ 0
have inr : ∀ (ht : Nontrivial α), Eq (α := Matrix n n α) 0⁻¹ 0
Tactic: rcases subsingleton_or_nontrivial α with ht | ht
-- 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 α
ht : Nontrivial α
⊢ Eq (α := Matrix n n α) 0⁻¹ 0
have inr : ∀ (hc : 0 = Fintype.card n), Eq (α := Matrix n n α) 0⁻¹ 0
Tactic: rcases (Fintype.card n).zero_le.eq_or_lt with hc | hc
-- 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 α
ht : Nontrivial α
inr : ∀ (hc : 0 = Fintype.card n), Eq (α := Matrix n n α) 0⁻¹ 0
⊢ Eq (α := Matrix n n α) 0⁻¹ 0
have inr₁ : ∀ (hc : 0 < Fintype.card n), Eq (α := Matrix n n α) 0⁻¹ 0
Tactic: rcases (Fintype.card n).zero_le.eq_or_lt with hc | hc
-- 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 α
ht : Nontrivial α
hc : 0 = Fintype.card n
⊢ Eq (α := Matrix n n α) 0⁻¹ 0
have hc₁ : IsEmpty n
Tactic: rw [eq_comm, Fintype.card_eq_zero_iff] at hc
Cleared hypotheses: hc
-- 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 α
ht : Nontrivial α
hc : 0 < Fintype.card n
⊢ Eq (α := Matrix n n α) 0⁻¹ 0
have hn : Nonempty n
Tactic: have hn : Nonempty n := Fintype.card_pos_iff.mp hc
-- 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 α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ Eq (α := Matrix n n α) 0⁻¹ 0
have inr : ¬IsUnit.{v} (M := α) (det.{v, u'} (n := n) 0)
Tactic: refine nonsing_inv_apply_not_isUnit _ ?_
-- 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.adjugate⁻¹ = h.unit⁻¹ • A
have refine : h.unit⁻¹ • A * A.adjugate = 1
Tactic: refine inv_eq_left_inv ?_
-- 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
⊢ h.unit⁻¹ • A * A.adjugate = 1
have rw : h.unit⁻¹ • (A * A.adjugate) = 1
Tactic: rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_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 : h.unit⁻¹ • (A * A.adjugate) = 1
⊢ h.unit⁻¹ • A * A.adjugate = 1
have rw₁ : h.unit⁻¹ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
Tactic: rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_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 : h.unit⁻¹ • (A * A.adjugate) = 1
rw₁ : h.unit⁻¹ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
⊢ h.unit⁻¹ • A * A.adjugate = 1
have rw₂ : (↑h.unit⁻¹ : α) • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
Tactic: rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_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 : 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
⊢ h.unit⁻¹ • A * A.adjugate = 1
have rw₃ : HSMul.hSMul (β := Matrix n n α) ((↑h.unit⁻¹ : α) * A.det) 1 = 1
Tactic: rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_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 : 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
⊢ h.unit⁻¹ • A * A.adjugate = 1
have rw₄ : HSMul.hSMul (α := α) (β := Matrix n n α) 1 1 = 1
Tactic: rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_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 : 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
⊢ h.unit⁻¹ • A * A.adjugate = 1
have rw₅ : Eq (α := Matrix n n α) 1 1
Tactic: rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 _ instMulOfFintypeOfAddCommMonoid one (diagonal v) _ =
    diagonal (@Invertible.invOf _ (Pi.instMul (M := fun (a : n) ↦ α)) (Pi.instOne (M := fun (a : n) ↦ α)) v _)
have 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 _)
Tactic: rw [@Invertible.congr _ _ _ _ _ (diagonalInvertible v) rfl]
-- 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 α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (diagonal v) _).diag * v) i = 1 i
have 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
Tactic: rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
-- 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 α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ((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
have dsimp : (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * ∏ j ∈ erase univ i, v j) * v i = 1
Tactic: dsimp
-- 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 α
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 _ * ∏ j ∈ erase univ i, v j) * v i = 1
have rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * (diagonal v).det = 1
Tactic: rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal]
-- 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 α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (v * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (diagonal v) _).diag) i = 1 i
have 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
Tactic: rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
-- 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 α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (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
have dsimp : v i * (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * ∏ j ∈ erase univ i, v j) = 1
Tactic: dsimp
-- 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 α
v : n → α
inst_3 : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ v i * (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * ∏ j ∈ erase univ i, v j) = 1
have rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (diagonal v).det _ * (diagonal v).det = 1
Tactic: rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]
-- 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 α
v : n → α
⊢ (diagonal v)⁻¹ = diagonal v⁻¹ʳ
have rw : (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
Tactic: rw [nonsing_inv_eq_ringInverse]
-- 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 α
v : n → α
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have pos : ∀ (h : IsUnit v), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
Tactic: by_cases h : IsUnit v
-- 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 α
v : n → α
pos : ∀ (h : IsUnit v), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have neg : ∀ (h : ¬IsUnit v), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
Tactic: by_cases h : IsUnit v
-- 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 α
v : n → α
h : IsUnit v
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have this : IsUnit (diagonal v)
Tactic: have := isUnit_diagonal.mpr h
-- 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 α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have pos : ∀ (val : Invertible (diagonal v)), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
Tactic: cases this.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 α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val : Invertible (diagonal v)
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have pos : ∀ (val : Invertible v), (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
Tactic: cases 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 α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val : Invertible (diagonal v)
val_1 : Invertible v
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have pos : @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne (diagonal v) _ = diagonal v⁻¹ʳ
Tactic: rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_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 α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val : Invertible (diagonal v)
val_1 : Invertible v
pos : @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne (diagonal v) _ = diagonal v⁻¹ʳ
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have pos₁ : @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne (diagonal v) _ =
  diagonal (@Invertible.invOf _ MulZeroClass.toMul MulOne.toOne v _)
Tactic: rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_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 α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val : Invertible (diagonal v)
val_1 : Invertible v
pos : @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne (diagonal v) _ = diagonal v⁻¹ʳ
pos₁ :
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne (diagonal v) _ =
    diagonal (@Invertible.invOf _ MulZeroClass.toMul MulOne.toOne v _)
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have pos₂ : diagonal (@Invertible.invOf _ (Pi.instMul (M := fun (a : n) ↦ α)) (Pi.instOne (M := fun (a : n) ↦ α)) v _) =
  diagonal (@Invertible.invOf _ MulZeroClass.toMul MulOne.toOne v _)
Tactic: rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]
-- 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 α
v : n → α
h : ¬IsUnit v
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have this : ¬IsUnit (diagonal v)
Tactic: have := isUnit_diagonal.not.mpr h
-- 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 α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have neg : (diagonal v)⁻¹ʳ = diagonal 0
Tactic: rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]
-- 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 α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
neg : (diagonal v)⁻¹ʳ = diagonal 0
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have neg₁ : (diagonal v)⁻¹ʳ = diagonal fun (x : n) ↦ 0
Tactic: rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]
-- 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 α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
neg : (diagonal v)⁻¹ʳ = diagonal 0
neg₁ : (diagonal v)⁻¹ʳ = diagonal fun (x : n) ↦ 0
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have neg₂ : (diagonal v)⁻¹ʳ = 0
Tactic: rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]
-- 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 α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
neg : (diagonal v)⁻¹ʳ = diagonal 0
neg₁ : (diagonal v)⁻¹ʳ = diagonal fun (x : n) ↦ 0
neg₂ : (diagonal v)⁻¹ʳ = 0
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
have neg₃ : Eq (α := Matrix n n α) 0 0
Tactic: rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Subsingleton m
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
⊢ A⁻¹ = diagonal fun (i : m) ↦ (A i i)⁻¹ʳ
have rw : Eq (α := Matrix m m α) (diagonal fun (x : m) ↦ A.det⁻¹ʳ) (diagonal fun (i : m) ↦ (A i i)⁻¹ʳ)
Tactic: rw [inv_def, adjugate_subsingleton, smul_one_eq_diagonal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Subsingleton m
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
⊢ Eq (α := Matrix m m α) (diagonal fun (x : m) ↦ A.det⁻¹ʳ) (diagonal fun (i : m) ↦ (A i i)⁻¹ʳ)
have h : ∀ (i : m), A.det = A i i
Tactic: congr! with i
-- 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 α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
have obtain : ∀ (val : Invertible A), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
Tactic: obtain ⟨_⟩ := hA.nonempty_invertible