-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f g : (↑R : Type u)ᵒᵖ
i : f ⟶ g
N : ModuleCat (↑(CommRingCat.of (↑R : Type u)) : Type u) := (Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)
hf :
  LE.le (α := Submonoid (↑R : Type u)) (Submonoid.powers (unop f))
    (Submonoid.comap (F :=
      (↑R : Type u) →+*
        Module.End (↑R : Type u)
          (↑(Functor.obj
                (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                  (Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                g) :
            Type u))
      (algebraMap (↑R : Type u)
        (Module.End (↑R : Type u)
          (↑(Functor.obj
                (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                  (Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                g) :
            Type u)))
      (IsUnit.submonoid
        (Module.End (↑R : Type u)
          (↑(Functor.obj
                (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                  (Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                g) :
            Type u))))
⊢ ∀ (a : (↑R : Type u)) (b : Membership.mem (γ := Submonoid (↑R : Type u)) (Submonoid.powers (unop f)) a),
    IsUnit (M :=
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              g) :
          Type u))
      ((algebraMap (↑R : Type u)
              (Module.End (↑R : Type u)
                (↑(Functor.obj
                      (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                        (Functor.obj modulesSpecToSheaf M).obj (P :=
                          CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                      g) :
                  Type u)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u)
                (↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g) : Type u))
          (↑(Subtype.mk (p := fun (a : (↑R : Type u)) ↦
                Membership.mem (γ := Submonoid (↑R : Type u)) (Submonoid.powers (unop f)) a) a b) :
            (↑R : Type u)) :
        Module.End (↑R : Type u)
          (↑(Functor.obj
                (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                  (Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                g) :
            Type u))

Tactic:
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _

Premises used: IsUnit.submonoid, Submonoid.comap, Submonoid.powers