-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
pos :
  ∀
    (hpi :
      Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
    totalDegree.{u, v} (R := R) (σ := S₁)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
        i ≤
      p.totalDegree
neg neg₁ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i)
          0),
    totalDegree.{u, v} (R := R) (σ := S₁)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
        i ≤
      p.totalDegree
neg₂ neg₃ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
    (σ : S₁ →₀ ℕ)
    (hσ :
      Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        σ),
    (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree
neg₄ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
    (σ : S₁ →₀ ℕ)
    (hσ :
      Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        σ),
    (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤
      (embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e
neg₅ neg₆ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
    (σ : S₁ →₀ ℕ)
    (hσ :
      Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        σ),
    embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree

Tactic:
classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ

Premises used: MvPolynomial.mem_support_iff, Finsupp.sum_embDomain, add_comm, Polynomial.coeff, Finset.add_sup, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, MvPolynomial.totalDegree, Finset.sup_le_iff, MvPolynomial.optionEquivLeft, Finsupp.sum_add_index, DFunLike.coe