-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
intro₁ :
  ∀ ⦃i : τ⦄,
    (∃ (d : τ →₀ ℕ),
        Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
      ∃ a ∈ φ.degrees, f a = i
intro₂ :
  ∀ ⦃i : τ⦄ (d : τ →₀ ℕ)
    (hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ d.support), ∃ a ∈ φ.degrees, f a = i
intro₃ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
intro₄ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)),
    ∃ a ∈ φ.degrees, f a = i
intro₅ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0),
    ∃ a ∈ φ.degrees, f a = i
intro₆ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i),
    Eq (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
intro₇ intro₈ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i) (j : σ) (hj : j ∈ x.support),
    Eq (α := ℕ) (((Finsupp.single (f j) ((x : (a : σ) → ℕ) j) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₉ : ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
  (hd :
    Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (j : σ) (hj : j ∈ x.support) (hi : ∀ (a : σ) (_ : ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ a ∈ d.support), f a ≠ i),
  Eq (α := ℕ) (((Finsupp.single (f j) ((x : (a : σ) → ℕ) j) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]