-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
rw :
  det.{w, v} (n := n)
      (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 ℤ))) =
    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 - 1)
rw₁ :
  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 α)
        (adjugate (mvPolynomialX 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 - 1)
rw₂ :
  ((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
          AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
        (a : MvPolynomial (n × n) ℤ) → α)
      (det (adjugate (mvPolynomialX 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 - 1)
rw₃ :
  ((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
          AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
        (a : MvPolynomial (n × n) ℤ) → α)
      (det (adjugate (mvPolynomialX n n ℤ))) =
    HPow.hPow (α := α)
      (((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
              AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
            (a : MvPolynomial (n × n) ℤ) → α)
          (det (mvPolynomialX n n ℤ)) :
        α)
      (Fintype.card n - 1)
rw₄ :
  Eq.{w + 1} (α := α)
    (((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
            AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
          (a : MvPolynomial (n × n) ℤ) → α)
        (det (adjugate (mvPolynomialX n n ℤ))) :
      α)
    (((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
            AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
          (a : MvPolynomial (n × n) ℤ) → α)
        (HPow.hPow (α := MvPolynomial (n × n) ℤ) (det (mvPolynomialX n n ℤ)) (Fintype.card n - 1)) :
      α)
rw₅ rw₆ :
  Eq.{w + 1} (α := α)
    (((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
            AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
          (a : MvPolynomial (n × n) ℤ) → α)
        (A'.det ^ (Fintype.card n - 1)) :
      α)
    (((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
            AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
          (a : MvPolynomial (n × n) ℤ) → α)
        (HPow.hPow (α := MvPolynomial (n × n) ℤ) (det (mvPolynomialX n n ℤ)) (Fintype.card n - 1)) :
      α)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, this]

Premises used: AlgHom.map_adjugate, AlgHom.map_det, Int, map_pow, Matrix.mvPolynomialX_mapMatrix_aeval