-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
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))
⊢ 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)

Tactic:
apply ConcreteCategory.mono_of_injective

Premises used: CategoryTheory.ConcreteCategory.mono_of_injective