-- 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))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ 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))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))
neg₁ :
  (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))
            ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
                (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))
            ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
                (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))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p
have neg₂ : (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))
Tactic: classical
  simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul']
  · simp
  · have hp' : (optionEquivLeft R _ ((rename (optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0 := by
      intro h
      exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))
    simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C,
      Polynomial.leadingCoeff_C]
    contrapose hp'
    ext m
    apply hc.1
    simpa using congr_arg (coeff m) hp'