case intro.intro
R : Type u_2
A : Type ?u.738556
B : Type ?u.738559
S : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x y : S
r : R
hr : ↑f r * y = 1
p : R[X]
p_monic : Monic p
hp : eval₂ f (x * y) p = 0
⊢ IsIntegralElem f x
R : Type u_2
A : Type ?u.738556
B : Type ?u.738559
S : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x y : S
r : R
hr : ↑f r * y = 1
hx : IsIntegralElem f (x * y)
⊢ IsIntegralElem f x
obtain ⟨p, ⟨p_monic, hp⟩⟩ := hx
case intro.intro
R : Type u_2
A : Type ?u.738556
B : Type ?u.738559
S : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x y : S
r : R
hr : ↑f r * y = 1
p : R[X]
p_monic : Monic p
hp : eval₂ f (x * y) p = 0
⊢ eval₂ f x (scaleRoots p r) = 0
case intro.intro
R : Type u_2
A : Type ?u.738556
B : Type ?u.738559
S : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x y : S
r : R
hr : ↑f r * y = 1
p : R[X]
p_monic : Monic p
hp : eval₂ f (x * y) p = 0
⊢ IsIntegralElem f x
refine' ⟨scaleRoots p r, ⟨(monic_scaleRoots_iff r).2 p_monic, _⟩⟩
case h.e'_2.h.e'_6
R : Type u_2
A : Type ?u.738556
B : Type ?u.738559
S : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x y : S
r : R
hr : ↑f r * y = 1
p : R[X]
p_monic : Monic p
hp : eval₂ f (x * y) p = 0
⊢ x = ↑f r * (x * y)
case intro.intro
R : Type u_2
A : Type ?u.738556
B : Type ?u.738559
S : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x y : S
r : R
hr : ↑f r * y = 1
p : R[X]
p_monic : Monic p
hp : eval₂ f (x * y) p = 0
⊢ eval₂ f x (scaleRoots p r) = 0
convert scaleRoots_eval₂_eq_zero f hp
no goals
case h.e'_2.h.e'_6
R : Type u_2
A : Type ?u.738556
B : Type ?u.738559
S : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x y : S
r : R
hr : ↑f r * y = 1
p : R[X]
p_monic : Monic p
hp : eval₂ f (x * y) p = 0
⊢ x = ↑f r * (x * y)
rw [mul_comm x y, ← mul_assoc, hr, one_mul]