awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⊤)
x : (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) : Type u)
⊢ Eq (α :=
    (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
          (op (PrimeSpectrum.basicOpen (unop g)))) :
      Type u))
    ((ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) : Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop g)))) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop g)))) :
        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 :=
            (Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op ⊤))
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE ⋯) ≫ i.unop.hom.op)) :
          (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) : Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop g)))) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop g)))) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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 ⋯))
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 ⋯))
⊢ 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 ⋯))

Tactic:
wlog hU : U = PrimeSpectrum.basicOpen 1 generalizing U

Premises used: PrimeSpectrum.basicOpen, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
U : (Spec (CommRingCat.of (↑R : Type u))).Opens
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
⊢ U ≤ PrimeSpectrum.basicOpen 1

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
U : (Spec (CommRingCat.of (↑R : Type u))).Opens
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
inr :
  Eq.{u + 1} (α := (Spec (CommRingCat.of (↑R : Type u))).Opens) (PrimeSpectrum.basicOpen 1) (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 ⋯))

Tactic:
rw [← tilde.toOpen_res _ (PrimeSpectrum.basicOpen 1) _ (homOfLE (by simp)), Category.assoc,
      NatTrans.naturality, ← Category.assoc, this, ← Functor.map_comp, ← op_comp, homOfLE_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, PrimeSpectrum.basicOpen, CategoryTheory.NatTrans.naturality, CategoryTheory.homOfLE, CategoryTheory.homOfLE_comp, AlgebraicGeometry.tilde.toOpen_res, CategoryTheory.Functor.map_comp, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
U : (Spec (CommRingCat.of (↑R : Type u))).Opens
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
⊢ Eq.{u + 1} (α := (Spec (CommRingCat.of (↑R : Type u))).Opens) (PrimeSpectrum.basicOpen 1) (PrimeSpectrum.basicOpen 1)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
U : (Spec (CommRingCat.of (↑R : Type u))).Opens
hU : U = PrimeSpectrum.basicOpen 1
subst :
  Eq (α :=
    (Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤) ⟶
      (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op (PrimeSpectrum.basicOpen 1)))
    (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ))
        (op (PrimeSpectrum.basicOpen 1)))
    ((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 ⋯))

Tactic:
subst hU
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
simp :
  Eq (α :=
    (Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤) ⟶
      (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op (PrimeSpectrum.basicOpen 1)))
    (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
      ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers 1)
          (ModuleCat.Hom.hom
            (tilde.toOpen
              ((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op ⊤))
              (PrimeSpectrum.basicOpen 1)))
          (ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE ⋯))))
          ⋯))
    ((Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α :=
    (Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤) ⟶
      (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op (PrimeSpectrum.basicOpen 1)))
    (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ))
        (op (PrimeSpectrum.basicOpen 1)))
    ((Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [fromTildeΓ, inducedFunctor_obj,
    homOfLE_leOfHom, Functor.FullyFaithful.map_preimage, TopCat.Sheaf.extend_hom_app]

Premises used: AlgebraicGeometry.Scheme.Modules.fromTildeΓ, TopCat.Sheaf.extend_hom_app, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.FullyFaithful.map_preimage, CategoryTheory.inducedFunctor_obj
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
x : (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) : Type u)
⊢ ∀ (x : ↥(Submonoid.powers 1)),
    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 (PrimeSpectrum.basicOpen 1))) :
          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 1))) :
                  Type u)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u)
                (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen 1))) : 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 (PrimeSpectrum.basicOpen 1))) :
            Type u))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
x : (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) : Type u)
⊢ Eq (α :=
    (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
          (op (PrimeSpectrum.basicOpen 1))) :
      Type u))
    ((ModuleCat.Hom.hom
            (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
              ModuleCat.ofHom
                (IsLocalizedModule.lift (Submonoid.powers 1)
                  (ModuleCat.Hom.hom
                    (tilde.toOpen
                      ((Functor.obj modulesSpecToSheaf M).obj (P :=
                            CategoryTheory.Presheaf.IsSheaf
                              (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                        (op ⊤))
                      (PrimeSpectrum.basicOpen 1)))
                  (ModuleCat.Hom.hom
                    ((Functor.obj modulesSpecToSheaf M).obj (P :=
                          CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
                      (Quiver.Hom.op (homOfLE ⋯))))
                  ⋯)) :
          (a : (↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) : Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen 1))) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen 1))) :
        Type u))
    ((ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) : Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen 1))) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen 1))) :
        Type u))

Tactic:
refine (IsLocalizedModule.lift_apply (.powers (M := R) 1)
    (tilde.toOpen _ (PrimeSpectrum.basicOpen (R := R) 1)).hom
    ((modulesSpecToSheaf.obj M).obj.map (homOfLE le_top).op).hom (by simp) x)

Premises used: PrimeSpectrum.basicOpen, AlgebraicGeometry.tilde.toOpen, Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, le_top, CategoryTheory.homOfLE, Submonoid.powers, IsLocalizedModule.lift_apply, OfNat.ofNat, ModuleCat.Hom.hom, AlgebraicGeometry.modulesSpecToSheaf, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
apply :
  Eq (α :=
    Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M) ⟶ Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M))
    (CategoryTheory.Functor.map modulesSpecToSheaf
      ((tilde.functor R).map (NatTrans.app (Iso.hom toTildeΓNatIso) M) ≫
        NatTrans.app fromTildeΓNatTrans ((tilde.functor R).obj M)))
    (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 ((tilde.functor R).obj M)))
⊢ (tilde.functor R).map (NatTrans.app (Iso.hom toTildeΓNatIso) M) ≫
      NatTrans.app fromTildeΓNatTrans ((tilde.functor R).obj M) =
    𝟙 ((tilde.functor R).obj M)

Tactic:
apply SpecModulesToSheafFullyFaithful.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, AlgebraicGeometry.SpecModulesToSheafFullyFaithful
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
h :
  Eq (α :=
    (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))) ⟶
      (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map modulesSpecToSheaf
        ((tilde.functor R).map (NatTrans.app (Iso.hom toTildeΓNatIso) M) ≫
          NatTrans.app fromTildeΓNatTrans ((tilde.functor R).obj M))))
    (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 ((tilde.functor R).obj M))))
⊢ Eq (α :=
    Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M) ⟶ Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M))
    (CategoryTheory.Functor.map modulesSpecToSheaf
      ((tilde.functor R).map (NatTrans.app (Iso.hom toTildeΓNatIso) M) ≫
        NatTrans.app fromTildeΓNatTrans ((tilde.functor R).obj M)))
    (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 ((tilde.functor R).obj M)))

Tactic:
apply CategoryTheory.Sheaf.hom_ext

Premises used: CategoryTheory.Sheaf.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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)ᵒᵖ
h :
  ∀ (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))
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply IsLocalizedModule.ext (.powers (M := R) r.unop)
      (toOpen _ (PrimeSpectrum.basicOpen (R := R) r.unop)).hom

Premises used: PrimeSpectrum.basicOpen, AlgebraicGeometry.tilde.toOpen, IsLocalizedModule.ext, Submonoid.powers, ModuleCat.Hom.hom, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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)ᵒᵖ
h :
  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))
        (unop r) :
      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))
⊢ LE.le (α := Submonoid (↑R : Type u)) (Submonoid.powers (unop r))
    (Submonoid.comap (F :=
      (↑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))
      (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)))
      (IsUnit.submonoid
        (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:
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]

Premises used: Submonoid.mem_comap, IsUnit.mem_submonoid_iff, Submonoid.powers_le