-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Polynomial (goal)
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : Eq (α := ℤˣ) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
inr :
  (HSMul.hSMul (α := ℤˣ) (β := α[X]) (-1)
        (∏ i : n,
          HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)).natDegree ≤
    natDegree.{u_2} (R := α)
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
inr₁ :
  (-HSMul.hSMul (α := ℤˣ) (β := α[X]) 1
          (∏ i : n,
            HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
              (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
              (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)).natDegree ≤
    natDegree.{u_2} (R := α)
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
inr₂ :
  natDegree.{u_2} (R := α)
      (-∏ i : n,
          HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i) ≤
    natDegree.{u_2} (R := α)
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
⊢ (HSMul.hSMul (α := ℤˣ) (β := α[X]) (((sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) g : ℤˣ)
        (∏ i : n,
          HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
            (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
            (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)).natDegree ≤
    natDegree.{u_2} (R := α)
      (∏ i : n,
        HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
          (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
          (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
have inr₃ : natDegree.{u_2} (R := α)
    (∏ i : n,
      HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
        (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
        (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i) ≤
  natDegree.{u_2} (R := α)
    (∏ i : n,
      HAdd.hAdd (β := Matrix.{u_1, u_1, u_2} n n α[X])
        (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (A.map (⇑C : (a : α) → α[X])))
        (B.map (⇑C : (a : α) → α[X])) ((g : (a : n) → n) i) i)
Tactic: rw [sg, Units.neg_smul, one_smul, natDegree_neg]