-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
simp_rw :
  Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
      ((optionEquivLeft R { b : σ // b ≠ n } :
          (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
        ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          (p * q))) =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            p)) +
      Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            q))
simp_rw₁ :
  (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)) (β :=
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
        ((optionEquivLeft R { b : σ // b ≠ n } :
              (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
            ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
              p) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
        ((optionEquivLeft R { b : σ // b ≠ n } :
              (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
            ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
              q) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))).natDegree =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            p)) +
      Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            q))
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q
have simp_rw₂ : (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)) (β :=
      Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
      ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((renameEquiv R (optionSubtypeNe n).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            p) :
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
      ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((renameEquiv R (optionSubtypeNe n).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            q) :
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))).natDegree =
  Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
      ((optionEquivLeft R { b : σ // b ≠ n } :
          (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
        ((renameEquiv R (optionSubtypeNe n).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          p)) +
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
      ((optionEquivLeft R { b : σ // b ≠ n } :
          (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
        ((renameEquiv R (optionSubtypeNe n).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          q))
Tactic: classical
  simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul] <;> simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]