∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyEtale R A ↔
    ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp