case mp
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
⊢ f ∈ map C I → ∀ (n : ℕ), coeff f n ∈ I

case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
⊢ (∀ (n : ℕ), coeff f n ∈ I) → f ∈ map C I
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
⊢ f ∈ map C I ↔ ∀ (n : ℕ), coeff f n ∈ I
constructor
case mp
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff f n ∈ I
case mp
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
⊢ f ∈ map C I → ∀ (n : ℕ), coeff f n ∈ I
intro hf
case mp.Hs
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x : R[X]), x ∈ ↑C '' ↑I → ∀ (n : ℕ), coeff x n ∈ I

case mp.H0
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff 0 n ∈ I

case mp.H1
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x y : R[X]), (∀ (n : ℕ), coeff x n ∈ I) → (∀ (n : ℕ), coeff y n ∈ I) → ∀ (n : ℕ), coeff (x + y) n ∈ I

case mp.H2
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), (∀ (n : ℕ), coeff x n ∈ I) → ∀ (n : ℕ), coeff (a • x) n ∈ I
case mp
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff f n ∈ I
apply @Submodule.span_induction _ _ _ _ _ f _ _ hf
case mp.Hs
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
⊢ coeff f n ∈ I
case mp.Hs
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x : R[X]), x ∈ ↑C '' ↑I → ∀ (n : ℕ), coeff x n ∈ I
intro f hf n
case mp.Hs.intro
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
⊢ coeff f n ∈ I
case mp.Hs
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
⊢ coeff f n ∈ I
cases' (Set.mem_image _ _ _).mp hf with x hx
case mp.Hs.intro
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
⊢ (if n = 0 then x else 0) ∈ I
case mp.Hs.intro
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
⊢ coeff f n ∈ I
rw [← hx.right, coeff_C]
case pos
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I

case neg
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I
case mp.Hs.intro
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
⊢ (if n = 0 then x else 0) ∈ I
by_cases h : n = 0
no goals
case pos
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I
simpa [h] using hx.left
no goals
case neg
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ↑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ ↑C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I
simp [h]
no goals
case mp.H0
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff 0 n ∈ I
simp
no goals
case mp.H1
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x y : R[X]), (∀ (n : ℕ), coeff x n ∈ I) → (∀ (n : ℕ), coeff y n ∈ I) → ∀ (n : ℕ), coeff (x + y) n ∈ I
exact fun f g hf hg n => by simp [I.add_mem (hf n) (hg n)]
no goals
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f g : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
hg : ∀ (n : ℕ), coeff g n ∈ I
n : ℕ
⊢ coeff (f + g) n ∈ I
simp [I.add_mem (hf n) (hg n)]
case mp.H2
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hg : ∀ (n : ℕ), coeff g n ∈ I
n : ℕ
⊢ coeff (f • g) n ∈ I
case mp.H2
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), (∀ (n : ℕ), coeff x n ∈ I) → ∀ (n : ℕ), coeff (a • x) n ∈ I
refine' fun f g hg n => _
case mp.H2
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hg : ∀ (n : ℕ), coeff g n ∈ I
n : ℕ
⊢ ∑ x in Nat.antidiagonal n, coeff f x.fst * coeff g x.snd ∈ I
case mp.H2
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hg : ∀ (n : ℕ), coeff g n ∈ I
n : ℕ
⊢ coeff (f • g) n ∈ I
rw [smul_eq_mul, coeff_mul]
no goals
case mp.H2
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hg : ∀ (n : ℕ), coeff g n ∈ I
n : ℕ
⊢ ∑ x in Nat.antidiagonal n, coeff f x.fst * coeff g x.snd ∈ I
exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
⊢ f ∈ map C I
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
⊢ (∀ (n : ℕ), coeff f n ∈ I) → f ∈ map C I
intro hf
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
⊢ (sum f fun n a => ↑(monomial n) a) ∈ map C I
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
⊢ f ∈ map C I
rw [← sum_monomial_eq f]
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
n : ℕ
x✝ : n ∈ support f
⊢ (fun n a => ↑(monomial n) a) n (coeff f n) ∈ map C I
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
⊢ (sum f fun n a => ↑(monomial n) a) ∈ map C I
refine' (I.map C : Ideal R[X]).sum_mem fun n _ => _
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
n : ℕ
x✝ : n ∈ support f
⊢ ↑C (coeff f n) * X ^ n ∈ map C I
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
n : ℕ
x✝ : n ∈ support f
⊢ (fun n a => ↑(monomial n) a) n (coeff f n) ∈ map C I
simp [← C_mul_X_pow_eq_monomial]
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
n : ℕ
x✝ : n ∈ support f
⊢ X ^ n * ↑C (coeff f n) ∈ map C I
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
n : ℕ
x✝ : n ∈ support f
⊢ ↑C (coeff f n) * X ^ n ∈ map C I
rw [mul_comm]
no goals
case mpr
R : Type u
S : Type ?u.120906
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), coeff f n ∈ I
n : ℕ
x✝ : n ∈ support f
⊢ X ^ n * ↑C (coeff f n) ∈ map C I
exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))