awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
left : A.det • (1 * B) = A.det • C
left₁ : A.det • (1 * B) = A.det • (1 * C)
left₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = A.det • (1 * C)
left₃ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = HSMul.hSMul (β := Matrix n n α) A.det 1 * C
left₄ : A.adjugate * A * B = A.adjugate * A * C
⊢ A.det • B = A.det • C
have left₅ : A.adjugate * (A * B) = A.adjugate * A * C
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
left : A.det • (1 * B) = A.det • C
left₁ : A.det • (1 * B) = A.det • (1 * C)
left₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = A.det • (1 * C)
left₃ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = HSMul.hSMul (β := Matrix n n α) A.det 1 * C
left₄ : A.adjugate * A * B = A.adjugate * A * C
left₅ : A.adjugate * (A * B) = A.adjugate * A * C
⊢ A.det • B = A.det • C
have left₆ : A.adjugate * (A * B) = A.adjugate * (A * C)
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
left : A.det • (1 * B) = A.det • C
left₁ : A.det • (1 * B) = A.det • (1 * C)
left₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = A.det • (1 * C)
left₃ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = HSMul.hSMul (β := Matrix n n α) A.det 1 * C
left₄ : A.adjugate * A * B = A.adjugate * A * C
left₅ : A.adjugate * (A * B) = A.adjugate * A * C
left₆ : A.adjugate * (A * B) = A.adjugate * (A * C)
⊢ A.det • B = A.det • C
have left₇ : A.adjugate * (A * C) = A.adjugate * (A * C)
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ B = C
have right : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A.det • x) B) ((fun (x : Matrix n n α) ↦ A.det • x) C)
Tactic: refine hA.matrix ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ A.det • B = A.det • C
have right : A.det • (B * 1) = A.det • C
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
right : A.det • (B * 1) = A.det • C
⊢ A.det • B = A.det • C
have right₁ : A.det • (B * 1) = A.det • (C * 1)
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
right : A.det • (B * 1) = A.det • C
right₁ : A.det • (B * 1) = A.det • (C * 1)
⊢ A.det • B = A.det • C
have right₂ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = A.det • (C * 1)
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
right : A.det • (B * 1) = A.det • C
right₁ : A.det • (B * 1) = A.det • (C * 1)
right₂ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = A.det • (C * 1)
⊢ A.det • B = A.det • C
have right₃ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = C * HSMul.hSMul (β := Matrix n n α) A.det 1
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
right : A.det • (B * 1) = A.det • C
right₁ : A.det • (B * 1) = A.det • (C * 1)
right₂ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = A.det • (C * 1)
right₃ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = C * HSMul.hSMul (β := Matrix n n α) A.det 1
⊢ A.det • B = A.det • C
have right₄ : B * (A * A.adjugate) = C * (A * A.adjugate)
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
right : A.det • (B * 1) = A.det • C
right₁ : A.det • (B * 1) = A.det • (C * 1)
right₂ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = A.det • (C * 1)
right₃ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = C * HSMul.hSMul (β := Matrix n n α) A.det 1
right₄ : B * (A * A.adjugate) = C * (A * A.adjugate)
⊢ A.det • B = A.det • C
have right₅ : B * A * A.adjugate = C * (A * A.adjugate)
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
right : A.det • (B * 1) = A.det • C
right₁ : A.det • (B * 1) = A.det • (C * 1)
right₂ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = A.det • (C * 1)
right₃ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = C * HSMul.hSMul (β := Matrix n n α) A.det 1
right₄ : B * (A * A.adjugate) = C * (A * A.adjugate)
right₅ : B * A * A.adjugate = C * (A * A.adjugate)
⊢ A.det • B = A.det • C
have right₆ : B * A * A.adjugate = C * A * A.adjugate
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
right : A.det • (B * 1) = A.det • C
right₁ : A.det • (B * 1) = A.det • (C * 1)
right₂ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = A.det • (C * 1)
right₃ : B * HSMul.hSMul (β := Matrix n n α) A.det 1 = C * HSMul.hSMul (β := Matrix n n α) A.det 1
right₄ : B * (A * A.adjugate) = C * (A * A.adjugate)
right₅ : B * A * A.adjugate = C * (A * A.adjugate)
right₆ : B * A * A.adjugate = C * A * A.adjugate
⊢ A.det • B = A.det • C
have right₇ : C * A * A.adjugate = C * A * A.adjugate
Tactic: rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
⊢ IsLeftRegular (A * B).det
have rw : IsLeftRegular (A.det * B.det)
Tactic: rw [det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have hAB : IsLeftRegular (A * B).det
Tactic: have hAB : IsLeftRegular (A * B).det := by
    rw [det_mul]
    exact hA.mul hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have refine : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A * B * x) (A * B).adjugate)
  ((fun (x : Matrix n n α) ↦ A * B * x) (B.adjugate * A.adjugate))
Tactic: refine (isRegular_of_isLeftRegular_det hAB).left ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₄ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • (1 * A.adjugate)
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
rw₄ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • (1 * A.adjugate)
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₅ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • A.adjugate
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
rw₄ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • (1 * A.adjugate)
rw₅ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • A.adjugate
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₆ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • (A * A.adjugate)
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
rw₄ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • (1 * A.adjugate)
rw₅ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • A.adjugate
rw₆ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • (A * A.adjugate)
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₇ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • HSMul.hSMul (β := Matrix n n α) A.det 1
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
rw₄ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • (1 * A.adjugate)
rw₅ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • A.adjugate
rw₆ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • (A * A.adjugate)
rw₇ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • HSMul.hSMul (β := Matrix n n α) A.det 1
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₈ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = HSMul.hSMul (β := Matrix n n α) (B.det * A.det) 1
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
rw₄ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • (1 * A.adjugate)
rw₅ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • A.adjugate
rw₆ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • (A * A.adjugate)
rw₇ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • HSMul.hSMul (β := Matrix n n α) A.det 1
rw₈ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = HSMul.hSMul (β := Matrix n n α) (B.det * A.det) 1
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₉ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = HSMul.hSMul (β := Matrix n n α) (A.det * B.det) 1
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
rw : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B * (B.adjugate * A.adjugate)
rw₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * (B.adjugate * A.adjugate))
rw₂ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (B * B.adjugate * A.adjugate)
rw₃ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * (HSMul.hSMul (β := Matrix n n α) B.det 1 * A.adjugate)
rw₄ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • (1 * A.adjugate)
rw₅ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = A * B.det • A.adjugate
rw₆ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • (A * A.adjugate)
rw₇ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = B.det • HSMul.hSMul (β := Matrix n n α) A.det 1
rw₈ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = HSMul.hSMul (β := Matrix n n α) (B.det * A.det) 1
rw₉ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = HSMul.hSMul (β := Matrix n n α) (A.det * B.det) 1
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
have rw₁₀ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = HSMul.hSMul (β := Matrix n n α) (A * B).det 1
Tactic: rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix.{v, v, w} n n α[X] :=
  fun (M : Matrix n n α) ↦ M.map (⇑C : (a : α) → α[X]) + HSMul.hSMul (α := α[X]) (β := Matrix.{v, v, w} n n α[X]) X 1
f' : Matrix.{v, v, w} n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
M : Matrix n n α
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
have a : ∀ (i j : n), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) i j = M i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix.{v, v, w} n n α[X] :=
  fun (M : Matrix n n α) ↦ M.map (⇑C : (a : α) → α[X]) + HSMul.hSMul (α := α[X]) (β := Matrix.{v, v, w} n n α[X]) X 1
f' : Matrix.{v, v, w} n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
Tactic: have f'_inv : ∀ M, f' (g M) = M := by
    intro
    ext
    simp [f', g]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix.{v, v, w} n n α[X] :=
  fun (M : Matrix n n α) ↦ M.map (⇑C : (a : α) → α[X]) + HSMul.hSMul (α := α[X]) (β := Matrix.{v, v, w} n n α[X]) X 1
f' : Matrix.{v, v, w} n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
M : Matrix n n α
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
have rw : adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g M)) = M.adjugate
Tactic: rw [RingHom.map_adjugate, f'_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix.{v, v, w} n n α[X] :=
  fun (M : Matrix n n α) ↦ M.map (⇑C : (a : α) → α[X]) + HSMul.hSMul (α := α[X]) (β := Matrix.{v, v, w} n n α[X]) X 1
f' : Matrix.{v, v, w} n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
M : Matrix n n α
rw : adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g M)) = M.adjugate
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
have rw₁ : M.adjugate = M.adjugate
Tactic: rw [RingHom.map_adjugate, f'_inv]