-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
x :
  (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
        TopCat) :
    Type u)
⊢ Mono (X :=
    (LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj Y)).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom.base :
          (a :
              (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                          (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
                    TopCat) :
                Type u)) →
            (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                        (Scheme.forgetToLocallyRingedSpace.obj Y)).toPresheafedSpace :
                  TopCat) :
              Type u))
        x))
    (PresheafedSpace.Hom.stalkMap
      (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x)
have i : Function.Injective (α :=
  (↑((LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj Y)).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom.base :
            (a :
                (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                            (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
                      TopCat) :
                  Type u)) →
              (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                          (Scheme.forgetToLocallyRingedSpace.obj Y)).toPresheafedSpace :
                    TopCat) :
                Type u))
          x)) :
    Type u))
  (β :=
  (↑((LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).presheaf.stalk x) :
    Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (X :=
        (LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj Y)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom.base :
              (a :
                  (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                              (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
                        TopCat) :
                    Type u)) →
                (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                            (Scheme.forgetToLocallyRingedSpace.obj Y)).toPresheafedSpace :
                      TopCat) :
                  Type u))
            x))
        (PresheafedSpace.Hom.stalkMap
          (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x)) :
    (a :
        (↑((LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj Y)).presheaf.stalk
              ((ConcreteCategory.hom
                    (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom.base :
                  (a :
                      (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                                  (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
                            TopCat) :
                        Type u)) →
                    (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                                (Scheme.forgetToLocallyRingedSpace.obj Y)).toPresheafedSpace :
                          TopCat) :
                      Type u))
                x)) :
          Type u)) →
      (↑((LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).presheaf.stalk x) :
        Type u))
Tactic: apply ConcreteCategory.mono_of_injective