-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)ᵒᵖ
simp :
  Membership.mem (α :=
    Module.End (↑R : Type u)
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop f)))) :
        Type u))
    (γ :=
    Submonoid
      (Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u)))
    (IsUnit.submonoid
      (Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u)))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                    (op (PrimeSpectrum.basicOpen (unop f)))) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop f)))) : Type u))
        (unop f) :
      Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u))
⊢ LE.le (α := Submonoid (↑R : Type u)) (Submonoid.powers (unop f))
    (Submonoid.comap (F :=
      (↑R : Type u) →+*
        Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u))
      (algebraMap (↑R : Type u)
        (Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u)))
      (IsUnit.submonoid
        (Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u))))

Tactic:
simp only [inducedFunctor_obj, Submonoid.powers_le, Submonoid.mem_comap]

Premises used: Submonoid.mem_comap, CategoryTheory.inducedFunctor_obj, Submonoid.powers_le