-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : 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))))
have 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))
Tactic: simp only [inducedFunctor_obj, Submonoid.powers_le, Submonoid.mem_comap]