-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s)
    (this :
      ∀ (x : FreeCommRing α),
        x.IsSupported s →
          ∃ (n : ℤ),
            Eq (α := ℤ[X])
              ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                      FreeCommRing α →+* ℤ[X]) :
                    (a : FreeCommRing α) → ℤ[X])
                  x :
                ℤ[X])
              ((↑n : ℤ[X]) : ℤ[X])),
    p ∈ s
haveI₄ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s)
    (this :
      ∃ (n : ℤ),
        Eq (α := ℤ[X])
          ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                  FreeCommRing α →+* ℤ[X]) :
                (a : FreeCommRing α) → ℤ[X])
              (of p) :
            ℤ[X])
          ((↑n : ℤ[X]) : ℤ[X])),
    p ∈ s
haveI₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])),
    p ∈ s
pos : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
neg neg₁ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), p ∈ s
neg₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), False
neg₃ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])),
    Eq (α := ℤ) 1 0
neg₄ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ) (H : Eq (α := ℤ[X]) X (↑w : ℤ[X])), Eq (α := ℤ) 1 0
neg₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ)
    (H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))), Eq (α := ℤ) 1 0
neg₆ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ)
    (H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ)))
    (this : Eq (α := ℤ) (coeff X 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)), Eq (α := ℤ) 1 0
⊢ p ∈ s

Tactic:
classical
  haveI := Classical.decPred (· ∈ s)
  have : ∀ x, IsSupported x s →
        ∃ n : ℤ, lift (fun a => if a ∈ s then (0 : ℤ[X]) else Polynomial.X) x = n := by
    intro x hx
    refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
    · use 1
      rw [map_one]
      norm_cast
    · use -1
      rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
    · rintro _ ⟨z, hzs, rfl⟩ _ _
      use 0
      rw [map_mul, lift_of, if_pos hzs, zero_mul]
      norm_cast
    · rintro x y ⟨q, hq⟩ ⟨r, hr⟩
      refine ⟨q + r, ?_⟩
      rw [map_add, hq, hr]
      norm_cast
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this

Premises used: Polynomial.C_eq_intCast, FreeCommRing.lift_of, Int.zero_ne_one, Ne.symm, if_pos, Polynomial.coeff_C, one_ne_zero, Polynomial.coeff_X, if_neg, rfl