no goals
R : Type u_3
A✝ : Type ?u.168448
B✝ : Type ?u.168451
S : Type ?u.168454
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
x : A
h : IsIntegral R (↑f x)
⊢ IsIntegral R x
simpa using map_isIntegral f.symm.toAlgHom h