-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (hypothesis)
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)
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
⊢ 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))
have this : Module.FaithfullyFlat.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)
Tactic: have : Module.FaithfullyFlat (Y.presheaf.stalk (f x)) (X.presheaf.stalk x) :=
    @Module.FaithfullyFlat.of_flat_of_isLocalHom _ _ _ _ _ _ _
      (Flat.stalkMap f x) (f.toLRSHom.prop x)