∀ (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.SmoothOfRelativeDimension n f ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
          ∃ V,
            ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              RingHom.IsStandardSmoothOfRelativeDimension n
                (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e))