case refine'_1
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ 0 ≠ 0 → eval₂ f r 0 = 0 → ∃ i, coeff 0 i ≠ 0 ∧ coeff 0 i ∈ comap f I

case refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]) (a : R),
    coeff p 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I) →
          p + ↑C a ≠ 0 → eval₂ f r (p + ↑C a) = 0 → ∃ i, coeff (p + ↑C a) i ≠ 0 ∧ coeff (p + ↑C a) i ∈ comap f I

case refine'_3
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]),
    p ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I) →
        p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
refine' p.recOnHorner _ _ _
case refine'_1
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
h : 0 ≠ 0
⊢ eval₂ f r 0 = 0 → ∃ i, coeff 0 i ≠ 0 ∧ coeff 0 i ∈ comap f I
case refine'_1
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ 0 ≠ 0 → eval₂ f r 0 = 0 → ∃ i, coeff 0 i ≠ 0 ∧ coeff 0 i ∈ comap f I
intro h
no goals
case refine'_1
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
h : 0 ≠ 0
⊢ eval₂ f r 0 = 0 → ∃ i, coeff 0 i ≠ 0 ∧ coeff 0 i ∈ comap f I
contradiction
case refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : coeff p 0 = 0
a_ne_zero : a ≠ 0
a✝ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p + ↑C a ≠ 0
hp : eval₂ f r (p + ↑C a) = 0
⊢ ∃ i, coeff (p + ↑C a) i ≠ 0 ∧ coeff (p + ↑C a) i ∈ comap f I
case refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]) (a : R),
    coeff p 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I) →
          p + ↑C a ≠ 0 → eval₂ f r (p + ↑C a) = 0 → ∃ i, coeff (p + ↑C a) i ≠ 0 ∧ coeff (p + ↑C a) i ∈ comap f I
intro p a coeff_eq_zero a_ne_zero _ _ hp
case refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : coeff p 0 = 0
a_ne_zero : a ≠ 0
a✝ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p + ↑C a ≠ 0
hp : eval₂ f r (p + ↑C a) = 0
⊢ coeff (p + ↑C a) 0 ≠ 0
case refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : coeff p 0 = 0
a_ne_zero : a ≠ 0
a✝ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p + ↑C a ≠ 0
hp : eval₂ f r (p + ↑C a) = 0
⊢ ∃ i, coeff (p + ↑C a) i ≠ 0 ∧ coeff (p + ↑C a) i ∈ comap f I
refine' ⟨0, _, coeff_zero_mem_comap_of_root_mem hr hp⟩
no goals
case refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : coeff p 0 = 0
a_ne_zero : a ≠ 0
a✝ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p + ↑C a ≠ 0
hp : eval₂ f r (p + ↑C a) = 0
⊢ coeff (p + ↑C a) 0 ≠ 0
simp [coeff_eq_zero, a_ne_zero]
case refine'_3
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r (p * X) = 0
⊢ ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
case refine'_3
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]),
    p ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I) →
        p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
intro p p_nonzero ih _ hp
case refine'_3
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
⊢ ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
case refine'_3
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r (p * X) = 0
⊢ ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
rw [eval₂_mul, eval₂_X] at hp
case refine'_3.intro.intro
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
case refine'_3
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
⊢ ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
obtain ⟨i, hi, mem⟩ := ih p_nonzero (r_non_zero_divisor hp)
case refine'_3.intro.intro.refine'_1
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ≠ 0

case refine'_3.intro.intro.refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ∈ comap f I
case refine'_3.intro.intro
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ ∃ i, coeff (p * X) i ≠ 0 ∧ coeff (p * X) i ∈ comap f I
refine' ⟨i + 1, _, _⟩
case refine'_3.intro.intro.refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ∈ comap f I
case refine'_3.intro.intro.refine'_1
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ≠ 0

case refine'_3.intro.intro.refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ∈ comap f I
. simp [hi, mem]
no goals
case refine'_3.intro.intro.refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ∈ comap f I
. simpa [hi] using mem
no goals
case refine'_3.intro.intro.refine'_1
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ≠ 0
simp [hi, mem]
no goals
case refine'_3.intro.intro.refine'_2
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, coeff p i ≠ 0 ∧ coeff p i ∈ comap f I
x✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : coeff p i ≠ 0
mem : coeff p i ∈ comap f I
⊢ coeff (p * X) (i + 1) ∈ comap f I
simpa [hi] using mem