-- 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 α)
⊢ 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 α)
    (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 α)
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 _)]