awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
Tactic: have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M := by
    intro
    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
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
M N : Matrix n n α
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
have rw : HMul.hMul (α := Matrix n n α) (β := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g N) : Matrix n n α) =
  M * N
Tactic: rw [map_mul, f'_inv, 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
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
M N : Matrix n n α
rw :
  HMul.hMul (α := Matrix n n α) (β := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g N) : Matrix n n α) =
    M * N
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
have rw₁ : HMul.hMul (β := Matrix n n α) M ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g N) : Matrix n n α) = M * N
Tactic: rw [map_mul, f'_inv, 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
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
M N : Matrix n n α
rw :
  HMul.hMul (α := Matrix n n α) (β := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g N) : Matrix n n α) =
    M * N
rw₁ : HMul.hMul (β := Matrix n n α) M ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g N) : Matrix n n α) = M * N
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
have rw₂ : M * N = M * N
Tactic: rw [map_mul, f'_inv, f'_inv]
-- 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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
Tactic: have f'_g_mul : ∀ M N : Matrix n n α, f' (g M * g N) = M * N := by
    intro M N
    rw [map_mul, f'_inv, 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
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
M : Matrix n n α
⊢ IsRegular (g M).det
have refine : (g M).det.Monic
Tactic: refine Polynomial.Monic.isRegular ?_
-- 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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have hu : ∀ (M : Matrix n n α), IsRegular (g M).det
Tactic: have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by
    intro M
    refine Polynomial.Monic.isRegular ?_
    simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]
-- 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
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₁ : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
  HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
rw₁ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₂ : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
  HMul.hMul (α := Matrix n n α) (β := Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A).adjugate : Matrix n n α)
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
rw₁ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
rw₂ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) (β := Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A).adjugate : Matrix n n α)
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₃ : Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
  ((f' : (a : Matrix n n α[X]) → Matrix n n α) ((g B).adjugate * (g A).adjugate) : Matrix n n α)
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
rw₁ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
rw₂ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) (β := Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A).adjugate : Matrix n n α)
rw₃ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) ((g B).adjugate * (g A).adjugate) : Matrix n n α)
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₄ : Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
  ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate : Matrix n n α)
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
rw₁ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
rw₂ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) (β := Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A).adjugate : Matrix n n α)
rw₃ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) ((g B).adjugate * (g A).adjugate) : Matrix n n α)
rw₄ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate : Matrix n n α)
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₅ : Eq (α := Matrix n n α)
  (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B))))
  ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate)
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
rw₁ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
rw₂ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) (β := Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A).adjugate : Matrix n n α)
rw₃ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) ((g B).adjugate * (g A).adjugate) : Matrix n n α)
rw₄ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate : Matrix n n α)
rw₅ :
  Eq (α := Matrix n n α)
    (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B))))
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate)
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₆ : Eq (α := Matrix n n α)
  (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B))))
  (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B)))
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
rw₁ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
rw₂ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) (β := Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A).adjugate : Matrix n n α)
rw₃ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) ((g B).adjugate * (g A).adjugate) : Matrix n n α)
rw₄ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate : Matrix n n α)
rw₅ :
  Eq (α := Matrix n n α)
    (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B))))
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate)
rw₆ :
  Eq (α := Matrix n n α)
    (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B))))
    (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B)))
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₇ : (A * B).adjugate = adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B))
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_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)
f'_inv : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M
f'_adj : ∀ (M : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
rw : (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate = B.adjugate * A.adjugate
rw₁ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α) A.adjugate
rw₂ :
  (f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate =
    HMul.hMul (α := Matrix n n α) (β := Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g B).adjugate : Matrix n n α)
      ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A).adjugate : Matrix n n α)
rw₃ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) ((g B).adjugate * (g A).adjugate) : Matrix n n α)
rw₄ :
  Eq (α := Matrix n n α) ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B)).adjugate : Matrix n n α)
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate : Matrix n n α)
rw₅ :
  Eq (α := Matrix n n α)
    (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B))))
    ((f' : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B).adjugate)
rw₆ :
  Eq (α := Matrix n n α)
    (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g (A * B))))
    (adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B)))
rw₇ :
  (A * B).adjugate = adjugate ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n α[X]) → Matrix n n α) (g A * g B))
⊢ (A * B).adjugate = B.adjugate * A.adjugate
have rw₈ : (A * B).adjugate = (A * B).adjugate
Tactic: rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_mul]