case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R ((fun x => B) x)) (↑(algebraMap A B) x) p = 0
⊢ IsIntegral R x
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
h : IsIntegral R (↑(algebraMap A B) x)
⊢ IsIntegral R x
rcases h with ⟨p, ⟨hp, hp'⟩⟩
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R ((fun x => B) x)) (↑(algebraMap A B) x) p = 0
⊢ eval₂ (algebraMap R A) x p = 0
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R ((fun x => B) x)) (↑(algebraMap A B) x) p = 0
⊢ IsIntegral R x
refine' ⟨p, ⟨hp, _⟩⟩
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : ↑(algebraMap A B) (eval x (Polynomial.map (algebraMap R A) p)) = ↑(algebraMap A B) 0
⊢ eval₂ (algebraMap R A) x p = 0
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R ((fun x => B) x)) (↑(algebraMap A B) x) p = 0
⊢ eval₂ (algebraMap R A) x p = 0
rw [IsScalarTower.algebraMap_eq R A B, ← eval₂_map, eval₂_hom, ←
  RingHom.map_zero (algebraMap A B)] at hp'
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : ↑(algebraMap A B) (eval x (Polynomial.map (algebraMap R A) p)) = ↑(algebraMap A B) 0
⊢ eval x (Polynomial.map (algebraMap R A) p) = 0
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : ↑(algebraMap A B) (eval x (Polynomial.map (algebraMap R A) p)) = ↑(algebraMap A B) 0
⊢ eval₂ (algebraMap R A) x p = 0
rw [eval₂_eq_eval_map]
no goals
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.1449203
T : Type ?u.1449206
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
H : Function.Injective ↑(algebraMap A B)
x : A
p : R[X]
hp : Monic p
hp' : ↑(algebraMap A B) (eval x (Polynomial.map (algebraMap R A) p)) = ↑(algebraMap A B) 0
⊢ eval x (Polynomial.map (algebraMap R A) p) = 0
exact H hp'