R : Type u_3
A✝ : Type ?u.158436
B✝ : Type ?u.158439
S : Type ?u.158442
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A✝
inst✝⁷ : CommRing B✝
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B✝
f✝ : R →+* S
A : Type u_1
B : Type u_2
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ↑f
x : A
⊢ IsIntegral R (↑f x) → IsIntegral R x
R : Type u_3
A✝ : Type ?u.158436
B✝ : Type ?u.158439
S : Type ?u.158442
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A✝
inst✝⁷ : CommRing B✝
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B✝
f✝ : R →+* S
A : Type u_1
B : Type u_2
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ↑f
x : A
⊢ IsIntegral R (↑f x) ↔ IsIntegral R x
refine' ⟨_, map_isIntegral f⟩
case intro.intro
R : Type u_3
A✝ : Type ?u.158436
B✝ : Type ?u.158439
S : Type ?u.158442
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A✝
inst✝⁷ : CommRing B✝
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B✝
f✝ : R →+* S
A : Type u_1
B : Type u_2
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ↑f
x : A
p : R[X]
hp : Monic p
hx : eval₂ (algebraMap R ((fun x => B) x)) (↑f x) p = 0
⊢ IsIntegral R x
R : Type u_3
A✝ : Type ?u.158436
B✝ : Type ?u.158439
S : Type ?u.158442
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A✝
inst✝⁷ : CommRing B✝
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B✝
f✝ : R →+* S
A : Type u_1
B : Type u_2
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ↑f
x : A
⊢ IsIntegral R (↑f x) → IsIntegral R x
rintro ⟨p, hp, hx⟩
case intro.intro
R : Type u_3
A✝ : Type ?u.158436
B✝ : Type ?u.158439
S : Type ?u.158442
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A✝
inst✝⁷ : CommRing B✝
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B✝
f✝ : R →+* S
A : Type u_1
B : Type u_2
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ↑f
x : A
p : R[X]
hp : Monic p
hx : eval₂ (algebraMap R ((fun x => B) x)) (↑f x) p = 0
⊢ eval₂ (algebraMap R A) x p = 0
case intro.intro
R : Type u_3
A✝ : Type ?u.158436
B✝ : Type ?u.158439
S : Type ?u.158442
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A✝
inst✝⁷ : CommRing B✝
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B✝
f✝ : R →+* S
A : Type u_1
B : Type u_2
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ↑f
x : A
p : R[X]
hp : Monic p
hx : eval₂ (algebraMap R ((fun x => B) x)) (↑f x) p = 0
⊢ IsIntegral R x
use p, hp
no goals
case intro.intro
R : Type u_3
A✝ : Type ?u.158436
B✝ : Type ?u.158439
S : Type ?u.158442
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A✝
inst✝⁷ : CommRing B✝
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B✝
f✝ : R →+* S
A : Type u_1
B : Type u_2
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ↑f
x : A
p : R[X]
hp : Monic p
hx : eval₂ (algebraMap R ((fun x => B) x)) (↑f x) p = 0
⊢ eval₂ (algebraMap R A) x p = 0
rwa [← f.comp_algebraMap, ← AlgHom.coe_toRingHom, ← Polynomial.hom_eval₂, AlgHom.coe_toRingHom,
  map_eq_zero_iff f hf] at hx