-- 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 α)
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 α)
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 α)
      (A'.det ^ (Fintype.card n - 2) • A') =
    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₄ :
  (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 α)
      (A'.det ^ (Fintype.card n - 2) • A') =
    HSMul.hSMul (β := Matrix 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 - 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₅ :
  (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 α)
      (A'.det ^ (Fintype.card n - 2) • A') =
    HSMul.hSMul (α := α) (β := Matrix 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 - 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₆ : (A'.det ^ (Fintype.card n - 2) • A').map
    (⇑(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) ℤ) → α) =
  HSMul.hSMul (α := α) (β := Matrix 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 - 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 _)]