-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
r :
  (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
      basicOpen)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop r))),
    IsUnit (M :=
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              r) :
          Type u))
      ((algebraMap (↑R : Type u)
              (Module.End (↑R : Type u)
                (↑(Functor.obj
                      (Functor.op (inducedFunctor basicOpen) ⋙
                        (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                          CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                      r) :
                  Type u)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u)
                (↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r) :
                  Type u))
          (↑x : (↑R : Type u)) :
        Module.End (↑R : Type u)
          (↑(Functor.obj
                (Functor.op (inducedFunctor basicOpen) ⋙
                  (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                r) :
            Type u))
have h : ∀ (a : (↑R : Type u)) (b : Membership.mem (γ := Submonoid (↑R : Type u)) (Submonoid.powers (unop r)) a),
  IsUnit (M :=
    Module.End (↑R : Type u)
      (↑(Functor.obj
            (Functor.op (inducedFunctor basicOpen) ⋙
              (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
            r) :
        Type u))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑(Functor.obj
                    (Functor.op (inducedFunctor basicOpen) ⋙
                      (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                    r) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r) :
                Type u))
        (↑(Subtype.mk (p := fun (a : (↑R : Type u)) ↦
              Membership.mem (γ := Submonoid (↑R : Type u)) (Submonoid.powers (unop r)) a) a b) :
          (↑R : Type u)) :
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              r) :
          Type u))
Tactic: rw [Subtype.forall]