-- 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:
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})
⊢ y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I ↔ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

Tactic:
constructor

Result:
case mp
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})
⊢ y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I → ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

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

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})
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x) p = ↑y
⊢ y = ∑ i ∈ p.support, ⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩

Tactic:
ext1

Result:
case a
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 = ↑(∑ i ∈ p.support, ⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩)

Proof state:
case mp.add
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)
ha' : ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑a
hb' : ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑b
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a + b)

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

Result:
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)

Proof state:
case mp
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})
⊢ y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I → ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

Tactic:
intro H

Result:
case mp
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})
H : y ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

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 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✝
⊢ (aeval x) (a + b) = ↑(a✝ + b✝)

Tactic:
simp [ha', hb']

Result:
no goals

Proof state:
case a
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 = ↑(∑ i ∈ p.support, ⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩)

Tactic:
simp only [AddSubmonoidClass.coe_finset_sum, ← map_sum, ← hp', ← as_sum_support_C_mul_X_pow]

Result:
no goals

Proof state:
case mp.smul.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})
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
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a • b)

Tactic:
obtain ⟨a, ha⟩ := a

Result:
case mp.smul.intro.intro.mk
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, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(⟨a, ha⟩ • b)