case intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.664590
S : Type ?u.664593
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
n : ℕ
hn : 0 < n
p : R[X]
hmonic : Monic p
heval : eval₂ (algebraMap R A) (x ^ n) p = 0
⊢ IsIntegral R x
R : Type u_1
A : Type u_2
B : Type ?u.664590
S : Type ?u.664593
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
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
⊢ IsIntegral R x
rcases hx with ⟨p, ⟨hmonic, heval⟩⟩
no goals
case intro.intro
R : Type u_1
A : Type u_2
B : Type ?u.664590
S : Type ?u.664593
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
n : ℕ
hn : 0 < n
p : R[X]
hmonic : Monic p
heval : eval₂ (algebraMap R A) (x ^ n) p = 0
⊢ IsIntegral R x
exact
  ⟨expand R n p, Monic.expand hn hmonic, by
    rwa [eval₂_eq_eval_map, map_expand, expand_eval, ← eval₂_eq_eval_map]⟩
no goals
R : Type u_1
A : Type u_2
B : Type ?u.664590
S : Type ?u.664593
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
n : ℕ
hn : 0 < n
p : R[X]
hmonic : Monic p
heval : eval₂ (algebraMap R A) (x ^ n) p = 0
⊢ eval₂ (algebraMap R A) x (↑(expand R n) p) = 0
rwa [eval₂_eq_eval_map, map_expand, expand_eval, ← eval₂_eq_eval_map]