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 α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
⊢ (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)
have succ : (A * A ^ k).adjugate = A.adjugate ^ (k + 1)
Tactic: rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]
-- 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 α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
succ : (A * A ^ k).adjugate = A.adjugate ^ (k + 1)
⊢ (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)
have succ₁ : (A ^ k).adjugate * A.adjugate = A.adjugate ^ (k + 1)
Tactic: rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]
-- 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 α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
succ : (A * A ^ k).adjugate = A.adjugate ^ (k + 1)
succ₁ : (A ^ k).adjugate * A.adjugate = A.adjugate ^ (k + 1)
⊢ (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)
have succ₂ : A.adjugate ^ k * A.adjugate = A.adjugate ^ (k + 1)
Tactic: rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]
-- 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 α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
succ : (A * A ^ k).adjugate = A.adjugate ^ (k + 1)
succ₁ : (A ^ k).adjugate * A.adjugate = A.adjugate ^ (k + 1)
succ₂ : A.adjugate ^ k * A.adjugate = A.adjugate ^ (k + 1)
⊢ (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)
have succ₃ : A.adjugate ^ k * A.adjugate = A.adjugate ^ k * A.adjugate
Tactic: rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]
-- 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 α
k : ℕ
⊢ (A ^ k).adjugate = A.adjugate ^ k
have zero : (HPow.hPow (β := ℕ) A 0).adjugate = HPow.hPow (β := ℕ) A.adjugate 0
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]
Cleared hypotheses: k
-- 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 α
k : ℕ
zero : (HPow.hPow (β := ℕ) A 0).adjugate = HPow.hPow (β := ℕ) A.adjugate 0
⊢ (A ^ k).adjugate = A.adjugate ^ k
have succ : ∀ (k : ℕ) (IH : (A ^ k).adjugate = A.adjugate ^ k), (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]
Cleared hypotheses: k
-- 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 α
⊢ A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
have rw : A * (A.adjugate * A).adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
Tactic: rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
-- 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 α
rw : A * (A.adjugate * A).adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
⊢ A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
have rw₁ : A * (HSMul.hSMul (β := Matrix n n α) A.det 1).adjugate =
  A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
Tactic: rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
-- 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 α
rw : A * (A.adjugate * A).adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rw₁ :
  A * (HSMul.hSMul (β := Matrix n n α) A.det 1).adjugate =
    A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
⊢ A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
have rw₂ : A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) (adjugate 1) =
  A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
Tactic: rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
-- 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 α
rw : A * (A.adjugate * A).adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rw₁ :
  A * (HSMul.hSMul (β := Matrix n n α) A.det 1).adjugate =
    A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rw₂ :
  A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) (adjugate 1) =
    A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
⊢ A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
have rw₃ : A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1 =
  A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
Tactic: rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
-- 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 : Matrix n n α
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
have this : A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
Tactic: have : A * (A.adjugate * A.adjugate.adjugate) =
      A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
    rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
-- 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 α
this : A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
have rwa : ∀ (this : A * A.adjugate * A.adjugate.adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
  A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Tactic: rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this
Cleared hypotheses: this
-- 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 α
this : A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rwa :
  ∀
    (this :
      A * A.adjugate * A.adjugate.adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
have rwa₁ : ∀
  (this :
    HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate =
      A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
  A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Tactic: rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this
Cleared hypotheses: this
-- 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 α
this : A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rwa :
  ∀
    (this :
      A * A.adjugate * A.adjugate.adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate =
        A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
have rwa₂ : ∀ (this : HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • (A * 1)),
  A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Tactic: rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this
Cleared hypotheses: this
-- 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 α
this : A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rwa :
  ∀
    (this :
      A * A.adjugate * A.adjugate.adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate =
        A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₂ :
  ∀ (this : HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • (A * 1)),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
have rwa₃ : ∀ (this : HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A),
  A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Tactic: rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this
Cleared hypotheses: this
-- 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 α
this : A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rwa :
  ∀
    (this :
      A * A.adjugate * A.adjugate.adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate =
        A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₂ :
  ∀ (this : HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • (A * 1)),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₃ :
  ∀ (this : HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
have rwa₄ : ∀ (this : A.det • (1 * A.adjugate.adjugate) = A.det ^ (Fintype.card n - 1) • A),
  A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Tactic: rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this
Cleared hypotheses: this
-- 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 α
this : A * (A.adjugate * A.adjugate.adjugate) = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1
rwa :
  ∀
    (this :
      A * A.adjugate * A.adjugate.adjugate = A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate =
        A * HSMul.hSMul (β := Matrix n n α) (A.det ^ (Fintype.card n - 1)) 1),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₂ :
  ∀ (this : HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • (A * 1)),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₃ :
  ∀ (this : HSMul.hSMul (β := Matrix n n α) A.det 1 * A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
rwa₄ :
  ∀ (this : A.det • (1 * A.adjugate.adjugate) = A.det ^ (Fintype.card n - 1) • A),
    A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
have rwa₅ : ∀ (this : A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A),
  A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Tactic: rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this
Cleared hypotheses: this
-- 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 α
h : Fintype.card n ≠ 1
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
have zero : ∀ (h_card : Fintype.card n = 0), A.adjugate.adjugate = A.det ^ HSub.hSub (α := ℕ) 0 2 • A
Tactic: rcases h_card : Fintype.card n with _ | n'
-- 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 α
h : Fintype.card n ≠ 1
zero : ∀ (h_card : Fintype.card n = 0), A.adjugate.adjugate = A.det ^ HSub.hSub (α := ℕ) 0 2 • A
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
have succ : ∀ (n' : ℕ) (h_card : Fintype.card n = n' + 1), A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A
Tactic: rcases h_card : Fintype.card n with _ | n'
-- 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 α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = n' + 1
⊢ A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A
have succ : ∀ (h_card : Fintype.card n = HAdd.hAdd (α := ℕ) 0 1), A.adjugate.adjugate = A.det ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) • A
Tactic: cases n'
Cleared hypotheses: n', h_card
-- 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 α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = n' + 1
succ :
  ∀ (h_card : Fintype.card n = HAdd.hAdd (α := ℕ) 0 1), A.adjugate.adjugate = A.det ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) • A
⊢ A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A
have succ₁ : ∀ (n_1 : ℕ) (h_card : Fintype.card n = n_1 + 1 + 1), A.adjugate.adjugate = A.det ^ (n_1 + 1 + 1 - 2) • A
Tactic: cases n'
Cleared hypotheses: n', h_card
-- 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 α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
⊢ A.adjugate.adjugate = A.det ^ (n_1 + 1 + 1 - 2) • A
have succ : A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
Tactic: rw [← h_card]
-- 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 α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
have rw : adjugate
    (adjugate
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ))) =
  HSMul.hSMul (β := Matrix n n α)
    (HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 2))
    ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ) :
      Matrix n n α)
Tactic: rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_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 : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
rw :
  adjugate
      (adjugate
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ))) =
    HSMul.hSMul (β := Matrix n n α)
      (HPow.hPow (α := α)
        (det.{w, v} (n := n)
          ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
              (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
            (mvPolynomialX n n ℤ)))
        (Fintype.card n - 2))
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ) :
        Matrix n n α)
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
have rw₁ : adjugate
    ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
        (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
      (adjugate (mvPolynomialX n n ℤ))) =
  HSMul.hSMul (β := Matrix n n α)
    (HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 2))
    ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ) :
      Matrix n n α)
Tactic: rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_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 : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
rw :
  adjugate
      (adjugate
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ))) =
    HSMul.hSMul (β := Matrix n n α)
      (HPow.hPow (α := α)
        (det.{w, v} (n := n)
          ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
              (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
            (mvPolynomialX n n ℤ)))
        (Fintype.card n - 2))
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ) :
        Matrix n n α)
rw₁ :
  adjugate
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (adjugate (mvPolynomialX n n ℤ))) =
    HSMul.hSMul (β := Matrix n n α)
      (HPow.hPow (α := α)
        (det.{w, v} (n := n)
          ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
              (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
            (mvPolynomialX n n ℤ)))
        (Fintype.card n - 2))
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ) :
        Matrix n n α)
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
have rw₂ : (AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
      (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
    (adjugate (adjugate (mvPolynomialX n n ℤ))) =
  HSMul.hSMul (β := Matrix n n α)
    (HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 2))
    ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ) :
      Matrix n n α)
Tactic: rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_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 : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
have succ : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
Tactic: suffices adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A' by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_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 : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
Tactic: have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1 := by simp [h_card]