-- 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)ᵒᵖ
rw :
  ∀ (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 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)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u)
                (↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f)))) :
                  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 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))
⊢ ∀ (x : ↥(Submonoid.powers (unop f))),
    IsUnit (M :=
      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)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u)
                (↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f)))) :
                  Type u))
          (↑x : (↑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))

Tactic:
rw [Subtype.forall]

Premises used: Subtype.forall