no goals
R : Type u_1
A : Type u_2
B : Type ?u.722967
S✝ : Type ?u.722970
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S✝
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S✝
S T : Subalgebra R A
⊢ Algebra.IsIntegral R { x // x ∈ S ⊔ T } ↔ Algebra.IsIntegral R { x // x ∈ S } ∧ Algebra.IsIntegral R { x // x ∈ T }
simp only [← le_integralClosure_iff_isIntegral, sup_le_iff]