-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem C_dvd_iff_dvd_coeff (r : R) (φ : R[X]) : C r ∣ φ ↔ ∀ i, r ∣ φ.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i

case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ φ.coeff i
⊢ C r ∣ φ

Tactic:
choose c hc using h

Result:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
⊢ C r ∣ φ

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
⊢ C r ∣ φ

Tactic:
let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0

Result:
case mpr
R : Type u
inst✝ : Semiring R
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 ∣ φ

Proof state:
case mp.intro
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ (C r * φ).coeff c

Tactic:
rw [coeff_C_mul]

Result:
case mp.intro
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * φ.coeff c

Proof state:
case h
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
⊢ φ = C r * ψ

Tactic:
ext i

Result:
case h.a
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
⊢ φ.coeff i = (C r * ψ).coeff i

Proof state:
case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i

Tactic:
rintro ⟨φ, rfl⟩ c

Result:
case mp.intro
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ (C r * φ).coeff c

Proof state:
case h.a
R : Type u
inst✝ : Semiring R
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 ∈ φ.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

Tactic:
split_ifs with hi

Result:
case pos
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i ≠ 0
⊢ φ.coeff i = r * c i

case neg
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = r * 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ

Tactic:
intro h

Result:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ φ.coeff i
⊢ C r ∣ φ

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
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 ∣ φ

Tactic:
let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)

Result:
case mpr
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
⊢ C r ∣ φ

Proof state:
case neg
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i = 0
⊢ φ.coeff i = r * 0

Tactic:
rwa [mul_zero]

Result:
no goals

Proof state:
case h.a
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
⊢ φ.coeff i = (C r * ψ).coeff i

Tactic:
simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff,
  Finset.sum_ite_eq']

Result:
case h.a
R : Type u
inst✝ : Semiring R
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 ∈ φ.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

Proof state:
case mp.intro
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * φ.coeff c

Tactic:
apply dvd_mul_right

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = r * 0

Tactic:
rw [Classical.not_not] at hi

Result:
case neg
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i = 0
⊢ φ.coeff i = r * 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
⊢ C r ∣ φ

Tactic:
use ψ

Result:
case h
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
⊢ φ = C r * ψ

Proof state:
case pos
R : Type u
inst✝ : Semiring R
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 ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i ≠ 0
⊢ φ.coeff i = r * c i

Tactic:
rw [hc]

Result:
no goals