-- Mathlib/RingTheory/FreeCommRing.lean
theorem isSupported_of {p} {s : Set α} : IsSupported (of p) s ↔ p ∈ s :=
  suffices IsSupported (of p) s → p ∈ s from ⟨this, fun hps => Subring.subset_closure ⟨p, hps, rfl⟩⟩
  fun hps : IsSupported (of p) s => by
  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

Proof state:
case neg.intro
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
h : p ∉ s
w : ℤ
H : X = ↑w
⊢ 1 = 0

Tactic:
rw [← Polynomial.C_eq_intCast] at H

Result:
case neg.intro
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
h : p ∉ s
w : ℤ
H : X = C ↑w
⊢ 1 = 0

Proof state:
case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred s
h : p ∉ s
this : ∃ n, X = ↑n
⊢ 1 = 0

Tactic:
rcases this with ⟨w, H⟩

Result:
case neg.intro
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
h : p ∉ s
w : ℤ
H : X = ↑w
⊢ 1 = 0

Proof state:
case neg.intro
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
h : p ∉ s
w : ℤ
H : X = C ↑w
⊢ 1 = 0

Tactic:
have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl

Result:
case neg.intro
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred s
h : p ∉ s
w : ℤ
H : X = C ↑w
this : X.coeff 1 = (C w).coeff 1
⊢ 1 = 0

Proof state:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ (lift fun a => if a ∈ s then 0 else X) 1 = ↑1

Tactic:
rw [RingHom.map_one]

Result:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ 1 = ↑1

Proof state:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
h : p ∉ s
w : ℤ
H : X = C ↑w
⊢ (C ↑w).coeff 1 = (C w).coeff 1

Tactic:
rfl

Result:
no goals

Proof state:
case refine_4.intro.intro
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x✝ : FreeCommRing α
hx : x✝.IsSupported s
x y : FreeCommRing α
q : ℤ
hq : (lift fun a => if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : (lift fun a => if a ∈ s then 0 else X) y = ↑r
⊢ ↑q + ↑r = ↑(q + r)

Tactic:
norm_cast

Result:
no goals

Proof state:
case refine_3
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (∃ n_1, (lift fun a => if a ∈ s then 0 else X) n = ↑n_1) →
        ∃ n_1, (lift fun a => if a ∈ s then 0 else X) (z * n) = ↑n_1

Tactic:
rintro _ ⟨z, hzs, rfl⟩ _ _

Result:
case refine_3.intro.intro
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ ∃ n, (lift fun a => if a ∈ s then 0 else X) (of z * n✝) = ↑n

Proof state:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a => if a ∈ s then 0 else X) x = ↑n

Tactic:
refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a => if a ∈ s then 0 else X) 1 = ↑n

case refine_2
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a => if a ∈ s then 0 else X) (-1) = ↑n

case refine_3
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (∃ n_1, (lift fun a => if a ∈ s then 0 else X) n = ↑n_1) →
        ∃ n_1, (lift fun a => if a ∈ s then 0 else X) (z * n) = ↑n_1

case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, (lift fun a => if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, (lift fun a => if a ∈ s then 0 else X) y = ↑n) → ∃ n, (lift fun a => if a ∈ s then 0 else X) (x + y) = ↑n

Proof state:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ (lift fun a => if a ∈ s then 0 else X) (of z * n✝) = ↑0

Tactic:
rw [RingHom.map_mul, lift_of, if_pos hzs, zero_mul]

Result:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ 0 = ↑0