-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
neg :
  Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            ((C : (a : R) → MvPolynomial σ R) c))) +
      Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p)) =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))
⊢ (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)) (β :=
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
        ((optionEquivLeft R { b : σ // b ≠ j } :
              (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
            ((renameEquiv R (optionSubtypeNe j).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
              ((C : (a : R) → MvPolynomial σ R) c)) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
        ((optionEquivLeft R { b : σ // b ≠ j } :
              (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
            ((renameEquiv R (optionSubtypeNe j).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
              p) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))).natDegree =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))
have neg₁ : HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          ((C : (a : R) → MvPolynomial σ R) c))))
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))) ≠
  0
Tactic: rw [Polynomial.natDegree_mul']