-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_map_C_iff {I : Ideal R} {f : R[X]} :
    f ∈ (Ideal.map (C : R →+* R[X]) I : Ideal R[X]) ↔ ∀ n : ℕ, f.coeff n ∈ I

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
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

Tactic:
simp [h]

Result:
no goals

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

Tactic:
intro hf

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), f.coeff n ∈ I

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ (f.sum fun n a => (monomial n) a) ∈ map C I

Tactic:
refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ (fun n a => (monomial n) a) n (f.coeff n) ∈ map C I

Proof state:
case mp.refine_1.intro
R : Type u
inst✝ : CommSemiring R
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
⊢ f.coeff n ∈ I

Tactic:
rw [← hx.right, coeff_C]

Result:
case mp.refine_1.intro
R : Type u
inst✝ : CommSemiring R
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

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ X ^ n * C (f.coeff n) ∈ map C I

Tactic:
exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

Result:
no goals

Proof state:
case mp.refine_3
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x y : R[X]),
    x ∈ Submodule.span R[X] (⇑C '' ↑I) →
      y ∈ Submodule.span R[X] (⇑C '' ↑I) →
        (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I

Tactic:
exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]

Result:
no goals

Proof state:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), x ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I

Tactic:
refine fun f g _ hg n => ?_

Result:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
x✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f • g).coeff n ∈ I

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ f ∈ map C I

Tactic:
rw [← sum_monomial_eq f]

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ (f.sum fun n a => (monomial n) a) ∈ map C I

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ (fun n a => (monomial n) a) n (f.coeff n) ∈ map C I

Tactic:
simp only [← C_mul_X_pow_eq_monomial, ne_eq]

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ C (f.coeff n) * X ^ n ∈ map C I

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ f ∈ map C I ↔ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
constructor

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

case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ (∀ (n : ℕ), f.coeff n ∈ I) → f ∈ map C I

Proof state:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
x✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f • g).coeff n ∈ I

Tactic:
rw [smul_eq_mul, coeff_mul]

Result:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
x✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff x.1 * g.coeff x.2 ∈ I

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ C (f.coeff n) * X ^ n ∈ map C I

Tactic:
rw [mul_comm]

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ X ^ n * C (f.coeff n) ∈ map C I

Proof state:
case mp.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff 0 n ∈ I

Tactic:
simp

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ (∀ (n : ℕ), f.coeff n ∈ I) → f ∈ map C I

Tactic:
intro hf

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ f ∈ map C I

Proof state:
case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (n : ℕ), x.coeff n ∈ I

Tactic:
intro f hf n

Result:
case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
⊢ f.coeff n ∈ I

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hf

Result:
case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (n : ℕ), x.coeff n ∈ I

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

case mp.refine_3
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x y : R[X]),
    x ∈ Submodule.span R[X] (⇑C '' ↑I) →
      y ∈ Submodule.span R[X] (⇑C '' ↑I) →
        (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I

case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), x ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
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

Tactic:
simpa [h] using hx.left

Result:
no goals

Proof state:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
x✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff x.1 * g.coeff x.2 ∈ I

Tactic:
exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f g : R[X]
x✝¹ : f ∈ Submodule.span R[X] (⇑C '' ↑I)
x✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hf : ∀ (n : ℕ), f.coeff n ∈ I
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f + g).coeff n ∈ I

Tactic:
simp [I.add_mem (hf n) (hg n)]

Result:
no goals

Proof state:
case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
⊢ f.coeff n ∈ I

Tactic:
obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf

Result:
case mp.refine_1.intro
R : Type u
inst✝ : CommSemiring R
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
⊢ f.coeff n ∈ I