awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M N P : ModuleCat (↑R : Type u)
f : M ⟶ N
g : N ⟶ P
⊢ tilde.map (f ≫ g) = tilde.map f ≫ tilde.map g
have H : ∀ (p : (Spec R).Opens) (x : (↑Γ(tilde M, p) : Type u)),
  Eq (α := (↑Γ(tilde P, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (tilde.map (f ≫ g)) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde P, p) : Type u))
        x :
      (↑Γ(tilde P, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (tilde.map f ≫ tilde.map g) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde P, p) : Type u))
        x :
      (↑Γ(tilde P, p) : Type u))
Tactic: ext p x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M N : ModuleCat (↑R : Type u)
f : M ⟶ N
U : Opens (PrimeSpectrum (↑R : Type u))
⊢ toOpen M U ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map f))) (op U) =
    f ≫ toOpen N U
have hf : ∀ (x : (↑M : Type u)),
  Eq (α :=
    (↑((Functor.obj modulesSpecToSheaf (tilde N)).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
          (op U)) :
      Type u))
    ((ModuleCat.Hom.hom
            (toOpen M U ≫
              NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map f)))
                (op U)) :
          (a : (↑M : Type u)) → (↑((modulesSpecToSheaf.obj (tilde N)).obj.obj (op U)) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf (tilde N)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
            (op U)) :
        Type u))
    ((ModuleCat.Hom.hom (f ≫ toOpen N U) :
          (a : (↑M : Type u)) → (↑((modulesSpecToSheaf.obj (tilde N)).obj.obj (op U)) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf (tilde N)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
            (op U)) :
        Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
⊢ IsIso (Y := (Functor.obj modulesSpecToSheaf (tilde M)).presheaf.obj (op ⊤)) (toOpen M ⊤)
have rw : Function.Bijective (α := (↑M : Type u)) (β :=
  (↑(ModuleCat.of (↑R : Type u)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑M : Type u)))
          (op ⊤))) :
    Type u))
  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
        LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
        ModuleCat.carrier) (X := M) (Y :=
        ModuleCat.of (↑R : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑M : Type u)))
            (op ⊤)))
        (ModuleCat.ofHom (StructureSheaf.toOpenₗ (↑R : Type u) (↑M : Type u) ⊤))) :
    (a : (↑M : Type u)) →
      (↑(ModuleCat.of (↑R : Type u) ((structureSheafInType (↑R : Type u) (↑M : Type u)).obj.obj (op ⊤))) : Type u))
Tactic: rw [toOpen, isIso_comp_right_iff, ConcreteCategory.isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
⊢ IsUnit (M :=
    Module.End (↑R : Type u) (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u) (↑((modulesSpecToSheaf.obj M).presheaf.obj (op (basicOpen f))) : Type u))
        f :
      Module.End (↑R : Type u) (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u))
have rw : Function.Bijective (α := (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u)) (β :=
  (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u))
  (⇑((algebraMap (↑R : Type u)
              (Module.End (↑R : Type u)
                (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u) (↑((modulesSpecToSheaf.obj M).presheaf.obj (op (basicOpen f))) : Type u))
          f :
        Module.End (↑R : Type u) (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u)) :
    (a : (↑((modulesSpecToSheaf.obj M).presheaf.obj (op (basicOpen f))) : Type u)) →
      (↑((modulesSpecToSheaf.obj M).presheaf.obj (op (basicOpen f))) : Type u))
Tactic: rw [Module.End.isUnit_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
⊢ Function.Bijective (α := (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u)) (β :=
    (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u))
    (⇑((algebraMap (↑R : Type u)
                (Module.End (↑R : Type u)
                  (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u)) :
              (a : (↑R : Type u)) →
                Module.End (↑R : Type u) (↑((modulesSpecToSheaf.obj M).presheaf.obj (op (basicOpen f))) : Type u))
            f :
          Module.End (↑R : Type u) (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op (basicOpen f))) : Type u)) :
      (a : (↑((modulesSpecToSheaf.obj M).presheaf.obj (op (basicOpen f))) : Type u)) →
        (↑((modulesSpecToSheaf.obj M).presheaf.obj (op (basicOpen f))) : Type u))
have change : Function.Bijective (α := (↑Γ(M, basicOpen f) : Type u)) (β := (↑Γ(M, basicOpen f) : Type u))
  (⇑((algebraMap (↑Γ(Spec R, basicOpen f) : Type u)
              (Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
            (a : (↑Γ(Spec R, basicOpen f) : Type u)) →
              Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
          ((algebraMap (↑R : Type u) (↑Γ(Spec R, basicOpen f) : Type u) :
              (a : (↑R : Type u)) → (↑Γ(Spec R, basicOpen f) : Type u))
            f) :
        Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
    (a : (↑Γ(M, basicOpen f) : Type u)) → (↑Γ(M, basicOpen f) : Type u))
Tactic: change Function.Bijective (algebraMap Γ(Spec R, basicOpen f)
      (Module.End Γ(Spec R, basicOpen f) Γ(M, basicOpen f)) (algebraMap R _ f))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
⊢ Function.Bijective (α := (↑Γ(M, basicOpen f) : Type u)) (β := (↑Γ(M, basicOpen f) : Type u))
    (⇑((algebraMap (↑Γ(Spec R, basicOpen f) : Type u)
                (Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
              (a : (↑Γ(Spec R, basicOpen f) : Type u)) →
                Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
            ((algebraMap (↑R : Type u) (↑Γ(Spec R, basicOpen f) : Type u) :
                (a : (↑R : Type u)) → (↑Γ(Spec R, basicOpen f) : Type u))
              f) :
          Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
      (a : (↑Γ(M, basicOpen f) : Type u)) → (↑Γ(M, basicOpen f) : Type u))
have rw : IsUnit (M := Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
  ((algebraMap (↑Γ(Spec R, basicOpen f) : Type u)
          (Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
        (a : (↑Γ(Spec R, basicOpen f) : Type u)) →
          Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
      ((algebraMap (↑R : Type u) (↑Γ(Spec R, basicOpen f) : Type u) :
          (a : (↑R : Type u)) → (↑Γ(Spec R, basicOpen f) : Type u))
        f) :
    Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
Tactic: rw [← Module.End.isUnit_iff]
-- 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)ᵒᵖ
⊢ Functor.obj
      (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
        (Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
      f ⟶
    Functor.obj
      (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
        (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
      f
have refine : ∀ (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: refine (ModuleCat.ofHom (IsLocalizedModule.lift (.powers (M := R) f.unop)
          (tilde.toOpen _ (PrimeSpectrum.basicOpen f.unop)).hom
          ((modulesSpecToSheaf.obj M).obj.map (homOfLE le_top).op).hom ?_):)
-- 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)ᵒᵖ
⊢ ∀ (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))
have 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))
Tactic: rw [Subtype.forall]
-- 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)ᵒᵖ
⊢ ∀ (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))
have change : 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: change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
-- 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 g : (↑R : Type u)ᵒᵖ
i : f ⟶ g
N : ModuleCat (↑(CommRingCat.of (↑R : Type u)) : Type u) := (Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)
⊢ 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))))
have hf : 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))
      (unop f) :
    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: simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
U : (Spec (CommRingCat.of (↑R : Type u))).Opens
⊢ tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) U ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op U) =
    (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE ⋯))
have inr : ∀
  (this :
    ∀ (U : (Spec (CommRingCat.of (↑R : Type u))).Opens) (hU : U = PrimeSpectrum.basicOpen 1),
      tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) U ≫
          NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op U) =
        (Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
          (Quiver.Hom.op (homOfLE sorry)))
  (hU : ¬U = PrimeSpectrum.basicOpen 1),
  tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) U ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op U) =
    (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE sorry))
Tactic: wlog hU : U = PrimeSpectrum.basicOpen 1 generalizing U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
U : (Spec (CommRingCat.of (↑R : Type u))).Opens
inr :
  ∀
    (this :
      ∀ (U : (Spec (CommRingCat.of (↑R : Type u))).Opens) (hU : U = PrimeSpectrum.basicOpen 1),
        tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) U ≫
            NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op U) =
          (Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
            (Quiver.Hom.op (homOfLE ⋯)))
    (hU : ¬U = PrimeSpectrum.basicOpen 1),
    tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) U ≫
        NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op U) =
      (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
        (Quiver.Hom.op (homOfLE ⋯))
⊢ tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) U ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op U) =
    (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE ⋯))
have wlog : ∀ (U : (Spec (CommRingCat.of (↑R : Type u))).Opens) (hU : U = PrimeSpectrum.basicOpen 1),
  tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) U ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op U) =
    (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE sorry))
Tactic: wlog hU : U = PrimeSpectrum.basicOpen 1 generalizing U
Cleared hypotheses: U