case mp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ ↑C r ∣ φ → ∀ (i : ℕ), r ∣ coeff φ i

case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ coeff φ i) → ↑C r ∣ φ
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ ↑C r ∣ φ ↔ ∀ (i : ℕ), r ∣ coeff φ i
constructor
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ coeff (↑C r * φ) c
case mp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ ↑C r ∣ φ → ∀ (i : ℕ), r ∣ coeff φ i
rintro ⟨φ, rfl⟩ c
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * coeff φ c
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ coeff (↑C r * φ) c
rw [coeff_C_mul]
no goals
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * coeff φ c
apply dvd_mul_right
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ coeff φ i
⊢ ↑C r ∣ φ
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ coeff φ i) → ↑C r ∣ φ
intro h
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
⊢ ↑C r ∣ φ
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ coeff φ i
⊢ ↑C r ∣ φ
choose c hc using h
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
⊢ ↑C r ∣ φ
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
⊢ ↑C r ∣ φ
let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ ↑C r ∣ φ
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
⊢ ↑C r ∣ φ
let ψ : R[X] := ∑ i in φ.support, monomial i (c' i)
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ φ = ↑C r * ψ
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ ↑C r ∣ φ
use ψ
case mpr.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = coeff (↑C r * ψ) i
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ φ = ↑C r * ψ
ext i
case mpr.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = r * if coeff φ i ≠ 0 then if coeff φ i ≠ 0 then c i else 0 else 0
case mpr.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = coeff (↑C r * ψ) i
simp only [coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff,
  Finset.sum_ite_eq']
case mpr.a.inl
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i ≠ 0
⊢ coeff φ i = r * c i

case mpr.a.inr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : ¬coeff φ i ≠ 0
⊢ coeff φ i = r * 0
case mpr.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = r * if coeff φ i ≠ 0 then if coeff φ i ≠ 0 then c i else 0 else 0
split_ifs with hi
no goals
case mpr.a.inl
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i ≠ 0
⊢ coeff φ i = r * c i
rw [hc]
case mpr.a.inr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i = 0
⊢ coeff φ i = r * 0
case mpr.a.inr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : ¬coeff φ i ≠ 0
⊢ coeff φ i = r * 0
rw [Classical.not_not] at hi
no goals
case mpr.a.inr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i = 0
⊢ coeff φ i = r * 0
rwa [mul_zero]