α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
⊢ p ∈ s
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
⊢ p ∈ s
haveI := Classical.decPred s
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (of p) = ↑n
⊢ p ∈ s
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∀ (x : FreeCommRing α), IsSupported x s → ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n
⊢ p ∈ s
specialize this (of p) hps
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∃ n, (if p ∈ s then 0 else X) = ↑n
⊢ p ∈ s
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (of p) = ↑n
⊢ p ∈ s
rw [lift_of] at this
case inl
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : p ∈ s
this : ∃ n, 0 = ↑n
⊢ p ∈ s

case inr
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ p ∈ s
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∃ n, (if p ∈ s then 0 else X) = ↑n
⊢ p ∈ s
split_ifs  at this with h
case inr.h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ False
case inr
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ p ∈ s
exfalso
case inr.h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ 1 = 0
case inr.h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ False
apply Ne.symm Int.zero_ne_one
case inr.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑w
⊢ 1 = 0
case inr.h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ 1 = 0
rcases this with ⟨w, H⟩
case inr.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ 1 = 0
case inr.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑w
⊢ 1 = 0
rw [← Polynomial.C_eq_int_cast] at H
case inr.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
this : coeff X 1 = coeff (↑C w) 1
⊢ 1 = 0
case inr.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ 1 = 0
have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
no goals
case inr.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
this : coeff X 1 = coeff (↑C w) 1
⊢ 1 = 0
rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
⊢ ∀ (x : FreeCommRing α), IsSupported x s → ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n
intro x hx
case refine'_1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) 1 = ↑n

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

case refine'_3
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∀ (z : FreeCommRing α),
    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
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x 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
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n
refine' Subring.InClosure.recOn hx _ _ _ _
case refine'_1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) 1 = ↑1
case refine'_1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) 1 = ↑n
use 1
case refine'_1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ 1 = ↑1
case refine'_1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) 1 = ↑1
rw [RingHom.map_one]
no goals
case refine'_1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ 1 = ↑1
norm_cast
case refine'_2
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) (-1) = ↑(-1)
case refine'_2
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (-1) = ↑n
use -1
no goals
case refine'_2
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) (-1) = ↑(-1)
rw [RingHom.map_neg, RingHom.map_one, Int.cast_neg, Int.cast_one]
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x 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
case refine'_3
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∀ (z : FreeCommRing α),
    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
rintro _ ⟨z, hzs, rfl⟩ _ _
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x 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
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x 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
use 0
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ 0 = ↑0
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x 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
rw [RingHom.map_mul, lift_of, if_pos hzs, MulZeroClass.zero_mul]
no goals
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ 0 = ↑0
norm_cast
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ 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
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (x + y) = ↑n
case refine'_4
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x 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
rintro x y ⟨q, hq⟩ ⟨r, hr⟩
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ 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
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) (x + y) = ↑(q + r)
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ 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
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (x + y) = ↑n
refine' ⟨q + r, _⟩
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ 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)
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ 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
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) (x + y) = ↑(q + r)
rw [RingHom.map_add, hq, hr]
no goals
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ 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)
norm_cast
no goals
case inl
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : p ∈ s
this : ∃ n, 0 = ↑n
⊢ p ∈ s
exact h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ coeff (↑C ↑w) 1 = coeff (↑C w) 1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ coeff X 1 = coeff (↑C w) 1
rw [H]
no goals
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ coeff (↑C ↑w) 1 = coeff (↑C w) 1
rfl