case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i

case neg
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : ¬i ∈ support f
⊢ p ∣ coeff f i * z ^ i
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
⊢ p ∣ coeff f i * z ^ i
by_cases hi : i ∈ f.support
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n in support f, ↑(RingHom.id S) (coeff f n) * z ^ n
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
rw [eval, eval₂_eq_sum, sum_def] at dvd_eval
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n in support f, ↑(RingHom.id S) (coeff f n) * z ^ n
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.not_mem_erase _ _)] at dvd_eval
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ coeff f i * z ^ i
refine' (dvd_add_left _).mp dvd_eval
case pos.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ ∀ (x : ℕ), x ∈ Finset.erase (support f) i → p ∣ ↑(RingHom.id S) (coeff f x) * z ^ x
case pos
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ p ∣ ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
apply Finset.dvd_sum
case pos.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
j : ℕ
hj : j ∈ Finset.erase (support f) i
⊢ p ∣ ↑(RingHom.id S) (coeff f j) * z ^ j
case pos.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
⊢ ∀ (x : ℕ), x ∈ Finset.erase (support f) i → p ∣ ↑(RingHom.id S) (coeff f x) * z ^ x
intro j hj
no goals
case pos.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣ ↑(RingHom.id S) (coeff f i) * z ^ i + ∑ x in Finset.erase (support f) i, ↑(RingHom.id S) (coeff f x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : i ∈ support f
j : ℕ
hj : j ∈ Finset.erase (support f) i
⊢ p ∣ ↑(RingHom.id S) (coeff f j) * z ^ j
exact dvd_terms j (Finset.ne_of_mem_erase hj)
case h.e'_4
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : ¬i ∈ support f
⊢ coeff f i * z ^ i = 0
case neg
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : ¬i ∈ support f
⊢ p ∣ coeff f i * z ^ i
convert dvd_zero p
case h.e'_4
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : coeff f i = 0
⊢ coeff f i * z ^ i = 0
case h.e'_4
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : ¬i ∈ support f
⊢ coeff f i * z ^ i = 0
rw [not_mem_support_iff] at hi
no goals
case h.e'_4
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1578454
B' : Type ?u.1578457
a b : R
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R
p✝ q : R[X]
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type ?u.1578670
inst✝² : Semiring B
inst✝¹ : Algebra R B
x : A
inst✝ : CommRing S
f✝ : R →+* S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ coeff f j * z ^ j
hi : coeff f i = 0
⊢ coeff f i * z ^ i = 0
simp [hi]