case intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ FG (↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
hx : IsIntegral R x
⊢ FG (↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
rcases hx with ⟨f, hfm, hfx⟩
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))) ≤
    ↑Subalgebra.toSubmodule (Algebra.adjoin R {x})

case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ ↑Subalgebra.toSubmodule (Algebra.adjoin R {x}) ≤
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))) =
    ↑Subalgebra.toSubmodule (Algebra.adjoin R {x})
apply le_antisymm
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (Algebra.adjoin R {x})
⊢ r ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ ↑Subalgebra.toSubmodule (Algebra.adjoin R {x}) ≤
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
intro r hr
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
r : A
hr : r ∈ Algebra.adjoin R {x}
⊢ r ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (Algebra.adjoin R {x})
⊢ r ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
change r ∈ Algebra.adjoin R ({x} : Set A) at hr
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
r : A
hr : r ∈ AlgHom.range (aeval x)
⊢ r ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
r : A
hr : r ∈ Algebra.adjoin R {x}
⊢ r ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rw [Algebra.adjoin_singleton_eq_range_aeval] at hr
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) p ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
r : A
hr : r ∈ AlgHom.range (aeval x)
⊢ r ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rcases(aeval x).mem_range.mp hr with ⟨p, rfl⟩
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) (p %ₘ f + f * (p /ₘ f)) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) p ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rw [← modByMonic_add_div p hfm]
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) (p %ₘ f + f * (p /ₘ f)) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) (p %ₘ f + f * (p /ₘ f)) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rw [← aeval_def] at hfx
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) (p %ₘ f) ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) (p %ₘ f + f * (p /ₘ f)) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rw [AlgHom.map_add, AlgHom.map_mul, hfx, MulZeroClass.zero_mul, add_zero]
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
this : degree (p %ₘ f) ≤ degree f
⊢ ↑(aeval x) (p %ₘ f) ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
⊢ ↑(aeval x) (p %ₘ f) ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
have : degree (p %ₘ f) ≤ degree f := degree_modByMonic_le p hfm
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
⊢ ↑(aeval x) q ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
this : degree (p %ₘ f) ≤ degree f
⊢ ↑(aeval x) (p %ₘ f) ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
generalize p %ₘ f = q at this⊢
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
⊢ ∑ n in support q, eval₂ (algebraMap R A) x (↑C (coeff q n) * X ^ n) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
⊢ ↑(aeval x) q ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rw [← sum_C_mul_X_pow_eq q, aeval_def, eval₂_sum, sum_def]
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ eval₂ (algebraMap R A) x (↑C (coeff q k) * X ^ k) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
⊢ ∑ n in support q, eval₂ (algebraMap R A) x (↑C (coeff q n) * X ^ n) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
refine' sum_mem fun k hkq => _
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ coeff q k • x ^ k ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ eval₂ (algebraMap R A) x (↑C (coeff q k) * X ^ k) ∈
    span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rw [eval₂_mul, eval₂_C, eval₂_pow, eval₂_X, ← Algebra.smul_def]
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ x ^ k ∈ ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ coeff q k • x ^ k ∈ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
refine' smul_mem _ _ (subset_span _)
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ x ^ k ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ x ^ k ∈ ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
rw [Finset.mem_coe]
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ k ∈ Finset.range (natDegree f + 1)
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ x ^ k ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
refine' Finset.mem_image.2 ⟨_, _, rfl⟩
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ k ≤ natDegree f
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ k ∈ Finset.range (natDegree f + 1)
rw [Finset.mem_range, Nat.lt_succ_iff]
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
hk : natDegree f < k
⊢ False
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
⊢ k ≤ natDegree f
refine' le_of_not_lt fun hk => _
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : k ∈ support q
hk : natDegree f < k
⊢ False
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : degree q ≤ degree f
k : ℕ
hkq : k ∈ support q
hk : natDegree f < k
⊢ False
rw [degree_le_iff_coeff_zero] at this
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : coeff q k ≠ 0
hk : natDegree f < k
⊢ False
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : k ∈ support q
hk : natDegree f < k
⊢ False
rw [mem_support_iff] at hkq
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : coeff q k ≠ 0
hk : natDegree f < k
⊢ coeff q k = 0
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : coeff q k ≠ 0
hk : natDegree f < k
⊢ False
apply hkq
case intro.intro.a.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : coeff q k ≠ 0
hk : natDegree f < k
⊢ degree f < ↑k
case intro.intro.a.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : coeff q k ≠ 0
hk : natDegree f < k
⊢ coeff q k = 0
apply this
no goals
case intro.intro.a.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : ↑(aeval x) f = 0
p : R[X]
hr : ↑(aeval x) p ∈ AlgHom.range (aeval x)
q : R[X]
this : ∀ (m : ℕ), degree f < ↑m → coeff q m = 0
k : ℕ
hkq : coeff q k ≠ 0
hk : natDegree f < k
⊢ degree f < ↑k
exact lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 hk)
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))) ⊆
    ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ span R ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))) ≤
    ↑Subalgebra.toSubmodule (Algebra.adjoin R {x})
rw [span_le]
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
s : A
hs : s ∈ ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
⊢ s ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
⊢ ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))) ⊆
    ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
intro s hs
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
s : A
hs : s ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
⊢ s ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
s : A
hs : s ∈ ↑(Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1)))
⊢ s ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
rw [Finset.mem_coe] at hs
case intro.intro.a.intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
k : ℕ
hk : k ∈ Finset.range (natDegree f + 1)
hs : (fun x x_1 => x ^ x_1) x k ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
⊢ (fun x x_1 => x ^ x_1) x k ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
case intro.intro.a
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
s : A
hs : s ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
⊢ s ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
rcases Finset.mem_image.1 hs with ⟨k, hk, rfl⟩
case intro.intro.a.intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
k : ℕ
hs : (fun x x_1 => x ^ x_1) x k ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
⊢ (fun x x_1 => x ^ x_1) x k ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
case intro.intro.a.intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
k : ℕ
hk : k ∈ Finset.range (natDegree f + 1)
hs : (fun x x_1 => x ^ x_1) x k ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
⊢ (fun x x_1 => x ^ x_1) x k ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
clear hk
no goals
case intro.intro.a.intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.290022
S : Type ?u.290025
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
x : A
f : R[X]
hfm : Monic f
hfx : eval₂ (algebraMap R A) x f = 0
k : ℕ
hs : (fun x x_1 => x ^ x_1) x k ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (natDegree f + 1))
⊢ (fun x x_1 => x ^ x_1) x k ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R {x}))
exact (Algebra.adjoin R {x}).pow_mem (Algebra.subset_adjoin (Set.mem_singleton _)) k