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

Tactic:
trans ∑ i ∈ p.support, ⟨_, (C (p.coeff i) * X ^ i).aeval_mem_adjoin_singleton _ x⟩

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})
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), ⋯⟩

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

Proof state:
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)

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval] at ha

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}
ha : a ∈ (aeval x).range
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(⟨a, ha✝⟩ • b)

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

Tactic:
congr with i

Result:
case e_f.h.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
i : ℕ
⊢ ↑⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩ = ↑(p.coeff i • ⟨(aeval x) (X ^ i), ⋯⟩)

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

Tactic:
obtain ⟨p, hp : aeval x p = a⟩ := ha

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

Tactic:
induction' H using Submodule.span_induction with a ha a b ha hb ha' hb' a b hb hb'

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

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

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)

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

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

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

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

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), ⋯⟩
⊢ ∑ 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

Tactic:
exact sum_mem fun i _ ↦ Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ (hp i))

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 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✝
i : ℕ
⊢ (a + b).coeff i ∈ I

Tactic:
simpa using add_mem (ha i) (hb i)

Result:
no goals

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 : ℕ
⊢ ∑ x ∈ antidiagonal i, p.coeff x.1 * b'.coeff x.2 ∈ I

Tactic:
exact sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)

Result:
no goals

Proof state:
case e_f.h.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
i : ℕ
⊢ ↑⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩ = ↑(p.coeff i • ⟨(aeval x) (X ^ i), ⋯⟩)

Tactic:
simp [Algebra.smul_def]

Result:
no goals