-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
x : MvPolynomial σ S₁
hx : (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
refine_2 :
  ∀ (a : S₁)
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) a)) : Set S₁) ⊆
        range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
refine_2₁ :
  ∀ (p : MvPolynomial σ S₁) (n : σ)
    (ih :
      ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
        Membership.mem (γ := Set (MvPolynomial σ S₁))
          (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p)
    (hx : (↑(p * X n).coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) (p * X n)
refine_2₂ :
  ∀ (a : σ →₀ ℕ) (s : S₁) (p : MvPolynomial σ S₁) (ha : a ∉ p.support) (hs : s ≠ 0)
    (hp :
      ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
        Membership.mem (γ := Set (MvPolynomial σ S₁))
          (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p)
    (ih :
      ∀
        (hx :
          (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
            range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
        Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
          (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
          ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁))
    (hx :
      (↑(HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
                p).coeffs :
          Set S₁) ⊆
        range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x

Tactic:
induction x using induction_on'' with
    | C a =>
      by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩

Premises used: Set.singleton_subset_iff, Finset.coe_singleton, MvPolynomial.coeffs_mul_X, Set.union_subset_iff, MvPolynomial.coeffs_C, MvPolynomial.induction_on'', reduceIte, MvPolynomial.C, rfl, Finset.coe_union