awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
this : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate
rw : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate
rw₁ rw₂ : (Aᵀ.map star).adjugate = (Aᵀ.map star).adjugate
⊢ A.adjugateᵀ.map star = (Aᵀ.map star).adjugate

Tactic:
rw [A.adjugate_transpose, this]

Premises used: Matrix.adjugate_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
left : IsLeftRegular A
right : IsRightRegular A
⊢ IsRegular A

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A * x) B) ((fun (x : Matrix n n α) ↦ A * x) C)
⊢ B = C

Tactic:
hA.matrix ?_

Premises used: IsLeftRegular.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A * x) B) ((fun (x : Matrix n n α) ↦ A * x) C)
left : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A.det • x) B) ((fun (x : Matrix n n α) ↦ A.det • x) C)
⊢ B = C

Tactic:
refine hA.matrix ?_

Premises used: IsLeftRegular.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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)
left₇ left₈ : A.adjugate * (A * C) = A.adjugate * (A * C)
⊢ A.det • B = A.det • 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]

Premises used: Matrix.mul_assoc, Matrix.smul_mul, Matrix.adjugate_mul, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 α
right : ∀ (h : B * A = C * A), B = C
⊢ Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ x * A) B) ((fun (x : Matrix n n α) ↦ x * A) C) → B = C

Tactic:
(h : B * A = C * A)
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

Tactic:
hA.matrix ?_

Premises used: IsLeftRegular.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A.det • x) B) ((fun (x : Matrix n n α) ↦ A.det • x) C)
⊢ B = C

Tactic:
refine hA.matrix ?_

Premises used: IsLeftRegular.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
right₇ right₈ : C * A * A.adjugate = C * A * A.adjugate
⊢ A.det • B = 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]

Premises used: Matrix.mul_smul, Matrix.mul_assoc, Matrix.mul_one, Matrix.mul_adjugate
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw : IsLeftRegular (A.det * B.det)
⊢ IsLeftRegular (A * B).det

Tactic:
rw [det_mul]

Premises used: Matrix.det_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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.det * B.det)

Tactic:
hA.mul hB

Premises used: IsLeftRegular.mul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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.det * B.det)

Tactic:
exact hA.mul hB

Premises used: IsLeftRegular.mul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

Tactic:
have hAB : IsLeftRegular (A * B).det := by
    rw [det_mul]
    exact hA.mul hB
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

Tactic:
(isRegular_of_isLeftRegular_det hAB).left ?_

Premises used: Matrix.isRegular_of_isLeftRegular_det, IsRegular.left
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
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))
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
refine (isRegular_of_isLeftRegular_det hAB).left ?_

Premises used: Matrix.isRegular_of_isLeftRegular_det, IsRegular.left
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw₁₀ rw₁₁ : HSMul.hSMul (β := Matrix n n α) (A * B).det 1 = HSMul.hSMul (β := Matrix n n α) (A * B).det 1
⊢ A * B * (A * B).adjugate = 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]

Premises used: Matrix.mul_smul, Matrix.mul_assoc, smul_smul, Matrix.det_mul, Matrix.smul_mul, mul_comm, Matrix.one_mul, Matrix.mul_adjugate
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 α
a : ∀ (i j : n), (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) i j = M i j
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) = M

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 α
i j : n
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M) i j = M i j

Tactic:
simp [f', g]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

Tactic:
have f'_inv : ∀ M, f' (g M) = M := by
    intro
    ext
    simp [f', g]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw₁ rw₂ : M.adjugate = M.adjugate
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M).adjugate = M.adjugate

Tactic:
rw [RingHom.map_adjugate, f'_inv]

Premises used: RingHom.map_adjugate
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

Tactic:
have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M := by
    intro
    rw [RingHom.map_adjugate, f'_inv]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw₂ rw₃ : M * N = M * N
⊢ (f' : (a : Matrix n n α[X]) → Matrix n n α) (g M * g N) = M * N

Tactic:
rw [map_mul, f'_inv, f'_inv]

Premises used: map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

Tactic:
Polynomial.Monic.isRegular ?_

Premises used: Polynomial.Monic.isRegular
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 α
refine : (g M).det.Monic
⊢ IsRegular (g M).det

Tactic:
refine Polynomial.Monic.isRegular ?_

Premises used: Polynomial.Monic.isRegular
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 α
⊢ (g M).det.Monic

Tactic:
simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]

Premises used: Polynomial.leadingCoeff_det_X_one_add_C, add_comm, Polynomial.Monic.def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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))
rw₈ rw₉ : (A * B).adjugate = (A * B).adjugate
⊢ (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]

Premises used: Matrix.adjugate_mul_distrib_aux, RingHom.map_adjugate, RingHom.map_mul, IsRegular.left
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
⊢ (HPow.hPow (β := ℕ) A 0).adjugate = HPow.hPow (β := ℕ) A.adjugate 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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)
succ₃ succ₄ : A.adjugate ^ k * A.adjugate = A.adjugate ^ k * A.adjugate
⊢ (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)

Tactic:
rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

Premises used: pow_succ, Matrix.adjugate_mul_distrib, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
succ : ∀ (k : ℕ) (IH : (A ^ k).adjugate = A.adjugate ^ k), (A ^ (k + 1)).adjugate = A.adjugate ^ (k + 1)
⊢ (A ^ k).adjugate = A.adjugate ^ k

Tactic:
induction k with
  | zero => simp
  | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

Premises used: pow_succ, Matrix.adjugate_mul_distrib, Matrix.zero, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw₃ 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
⊢ A * (A.adjugate * A.adjugate.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]

Premises used: Matrix.adjugate_smul, Matrix.adjugate_mul_distrib, Matrix.adjugate_one, Matrix.adjugate_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rwa₅ rwa₆ rwa₇ 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
⊢ 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

Premises used: Matrix.mul_smul, Matrix.mul_assoc, Matrix.smul_mul, Matrix.mul_one, Matrix.one_mul, Matrix.mul_adjugate