R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
⊢ IsIntegral { x // x ∈ adjoin R S } x
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S
g : S →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
⊢ IsIntegral { x // x ∈ adjoin R ↑(frange (Polynomial.map (algebraMap A B) p)) } x
generalize hS : (↑(p.map <| algebraMap A B).frange : Set B) = S
case intro
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ IsIntegral { x // x ∈ adjoin R S } x
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
⊢ IsIntegral { x // x ∈ adjoin R S } x
obtain ⟨q, hq⟩ :
  ∃ q : (adjoin R S)[X], q.map (algebraMap (adjoin R S) B) = (p.map <| algebraMap A B) := by
  rw [← Set.mem_range]
  exact (Polynomial.mem_map_range _).2 fun i => ⟨⟨_, coeffs_mem i⟩, rfl⟩
case intro
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic q ∧ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = 0
case intro
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ IsIntegral { x // x ∈ adjoin R S } x
use q
case intro.left
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic q

case intro.right
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = 0
case intro
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic q ∧ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = 0
constructor
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
⊢ ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
intro i
case pos
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S

case neg
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : ¬coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
by_cases hi : (p.map <| algebraMap A B).coeff i = 0
case neg
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : ¬coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R ↑(frange (Polynomial.map (algebraMap A B) p))
case neg
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : ¬coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
rw [← hS]
no goals
case neg
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : ¬coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R ↑(frange (Polynomial.map (algebraMap A B) p))
exact subset_adjoin (coeff_mem_frange _ _ hi)
case pos
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ 0 ∈ adjoin R S
case pos
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
rw [hi]
no goals
case pos
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
i : ℕ
hi : coeff (Polynomial.map (algebraMap A B) p) i = 0
⊢ 0 ∈ adjoin R S
exact Subalgebra.zero_mem _
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
⊢ Polynomial.map (algebraMap A B) p ∈ Set.range fun q => Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
⊢ ∃ q, Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
rw [← Set.mem_range]
no goals
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
⊢ Polynomial.map (algebraMap A B) p ∈ Set.range fun q => Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q
exact (Polynomial.mem_map_range _).2 fun i => ⟨⟨_, coeffs_mem i⟩, rfl⟩
case intro.left
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
h : Monic (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q)
⊢ Monic q

case h
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q)
case intro.left
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic q
suffices h : (q.map (algebraMap (adjoin R S) B)).Monic
case intro.left
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
h : Monic (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q)
⊢ Function.Injective ↑(algebraMap { x // x ∈ adjoin R S } B)
case intro.left
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
h : Monic (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q)
⊢ Monic q
refine' monic_of_injective _ h
no goals
case intro.left
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
h : Monic (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q)
⊢ Function.Injective ↑(algebraMap { x // x ∈ adjoin R S } B)
exact Subtype.val_injective
case h
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic (Polynomial.map (algebraMap A B) p)
case h
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q)
rw [hq]
no goals
case h
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ Monic (Polynomial.map (algebraMap A B) p)
exact pmonic.map _
case h.e'_2
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = ↑(aeval x) p
case intro.right
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = 0
convert hp using 1
case h.e'_2
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : eval x (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q) = eval x (Polynomial.map (algebraMap A B) p)
⊢ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = ↑(aeval x) p
case h.e'_2
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q = Polynomial.map (algebraMap A B) p
⊢ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = ↑(aeval x) p
replace hq := congr_arg (eval x) hq
no goals
case h.e'_2
R : Type u_3
A : Type u_1
B : Type u_2
S✝ : Type ?u.1370556
T : Type ?u.1370559
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra A B
inst✝ : Algebra R B
f : R →+* S✝
g : S✝ →+* T
x : B
p : A[X]
pmonic : Monic p
hp : ↑(aeval x) p = 0
S : Set B
hS : ↑(frange (Polynomial.map (algebraMap A B) p)) = S
coeffs_mem : ∀ (i : ℕ), coeff (Polynomial.map (algebraMap A B) p) i ∈ adjoin R S
q : { x // x ∈ adjoin R S }[X]
hq : eval x (Polynomial.map (algebraMap { x // x ∈ adjoin R S } B) q) = eval x (Polynomial.map (algebraMap A B) p)
⊢ eval₂ (algebraMap { x // x ∈ adjoin R S } B) x q = ↑(aeval x) p
convert hq using 1 <;> symm <;> apply eval_map