∀ {A : Type u_1} {R : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B],
  Function.Injective ⇑(algebraMap A B) →
    (∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap A B) y = x) → IsIntegralClosure A R B