-- Mathlib/RingTheory/Polynomial/Ideal.lean
lemma _root_.Algebra.mem_ideal_map_adjoin {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    (x : S) (I : Ideal R) {y : adjoin R ({x} : Set S)} :
    y ∈ I.map (algebraMap R (adjoin R ({x} : Set S))) ↔
      ∃ p : R[X], (∀ i, p.coeff i ∈ I) ∧ Polynomial.aeval x p = y

Proof state:
case mp.smul.intro.intro.mk.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y b : ↥(adjoin R {x})
hb✝ : b ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
a : S
ha : a ∈ adjoin R {x}
p : R[X]
hp : (aeval x) p = a
i : ℕ
⊢ (p * b').coeff i ∈ I

Tactic:
rw [coeff_mul]

Result:
case mp.smul.intro.intro.mk.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y b : ↥(adjoin R {x})
hb✝ : b ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
a : S
ha : a ∈ adjoin R {x}
p : R[X]
hp : (aeval x) p = a
i : ℕ
⊢ ∑ x ∈ antidiagonal i, p.coeff x.1 * b'.coeff x.2 ∈ I

Proof state:
case mp.add.intro.intro.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y a✝ b✝ : ↥(adjoin R {x})
ha✝ : a✝ ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
hb✝ : b✝ ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x) a = ↑a✝
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x) b = ↑b✝
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a✝ + b✝)

Tactic:
exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y b : ↥(adjoin R {x})
hb✝ : b ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
a : S
ha : a ∈ adjoin R {x}
p : R[X]
hp : (aeval x) p = a
⊢ (aeval x) (p * b') = ↑(⟨a, ha⟩ • b)

Tactic:
simp [hp, hb']

Result:
no goals

Proof state:
case mpr
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
⊢ (∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y) → y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

Tactic:
rintro ⟨p, hp, hp'⟩

Result:
case mpr.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x) p = ↑y
⊢ y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
⊢ ∀ (i : ℕ), coeff 0 i ∈ I

Tactic:
simp

Result:
no goals

Proof state:
case mp.mem
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y a : ↥(adjoin R {x})
ha : a ∈ ⇑(algebraMap R ↥(adjoin R {x})) '' ↑I
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑a

Tactic:
obtain ⟨a, ha, rfl⟩ := ha

Result:
case mp.mem.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
a : R
ha : a ∈ ↑I
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑((algebraMap R ↥(adjoin R {x})) a)

Proof state:
case mp.smul.intro.intro.mk.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y b : ↥(adjoin R {x})
hb✝ : b ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
a : S
ha : a ∈ adjoin R {x}
p : R[X]
hp : (aeval x) p = a
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(⟨a, ha⟩ • b)

Tactic:
refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩

Result:
case mp.smul.intro.intro.mk.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y b : ↥(adjoin R {x})
hb✝ : b ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
a : S
ha : a ∈ adjoin R {x}
p : R[X]
hp : (aeval x) p = a
i : ℕ
⊢ (p * b').coeff i ∈ I

Proof state:
case mp.add.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y a✝ b : ↥(adjoin R {x})
ha✝ : a✝ ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
hb : b ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
hb' : ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑b
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x) a = ↑a✝
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a✝ + b)

Tactic:
obtain ⟨b, hb, hb'⟩ := hb'

Result:
case mp.add.intro.intro.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y a✝ b✝ : ↥(adjoin R {x})
ha✝ : a✝ ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
hb✝ : b✝ ∈ Submodule.span (↥(adjoin R {x})) (⇑(algebraMap R ↥(adjoin R {x})) '' ↑I)
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x) a = ↑a✝
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x) b = ↑b✝
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a✝ + b✝)

Proof state:
case mp.zero
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑0

Tactic:
exact ⟨0, by simp, aeval_zero _⟩

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
a : R
ha : a ∈ ↑I
i : ℕ
⊢ (if i = 0 then a else 0) ∈ I

Tactic:
aesop

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x) p = ↑y
this : y = ∑ i ∈ p.support, p.coeff i • ⟨(aeval x) (X ^ i), ⋯⟩
⊢ y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

Tactic:
simp_rw [this, Algebra.smul_def]

Result:
case mpr.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x) p = ↑y
this : y = ∑ i ∈ p.support, p.coeff i • ⟨(aeval x) (X ^ i), ⋯⟩
⊢ ∑ x_1 ∈ p.support, (algebraMap R ↥(adjoin R {x})) (p.coeff x_1) * ⟨(aeval x) (X ^ x_1), ⋯⟩ ∈
    Ideal.map (algebraMap R ↥(adjoin R {x})) I

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
a : R
ha : a ∈ ↑I
i : ℕ
⊢ (C a).coeff i ∈ I

Tactic:
rw [coeff_C]

Result:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
a : R
ha : a ∈ ↑I
i : ℕ
⊢ (if i = 0 then a else 0) ∈ I

Proof state:
case mp.mem.intro.intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥(adjoin R {x})
a : R
ha : a ∈ ↑I
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑((algebraMap R ↥(adjoin R {x})) a)

Tactic:
exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩

Result:
no goals