awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
U : X.Opens
f g : X ⟶ Y
hf : f = g
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
M : Y.Modules
⊢ Eq (α := Γ((restrictFunctor g).obj M, U) ⟶ Γ((restrictFunctor f).obj M, U))
    (Hom.app (NatTrans.app (Iso.inv (restrictFunctorCongr hf)) M) U) (M.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, AddMonoidHom.mk', Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M_1 N K : X.Modules
φ : M_1 ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ Membership.mem (α := ↥Y) (f ''ᵁ Opposite.unop (Opposite.op U)) (f x : ↥Y)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ CategoryStruct.comp (Y := ((restrictFunctor f).obj M).presheaf.stalk x)
      (((restrictFunctor f).obj M).presheaf.germ U x hxU) (NatTrans.app (Iso.hom (restrictStalkNatIso f x)) M) =
    M.presheaf.germ (f ''ᵁ Opposite.unop (Opposite.op U)) (f x) ⋯

Tactic:
haveI := Functor.initial_of_adjunction (f.isOpenEmbedding.adjunctionNhds x)
  Functor.Final.ι_colimitIso_hom
    (f.isOpenEmbedding.functorNhds x).op
    ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op ⋙ M.presheaf) _

Premises used: CategoryTheory.Functor.op, IsOpenMap.functorMap, CategoryTheory.ConcreteCategory.hom, Set.Mem, IsOpenMap.functorNhds, CategoryTheory.Functor.comp, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.colimit, Subtype.mk, TopCat.Presheaf.germ, Monotone.functor, Opposite.op, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.OpenNhds, Topology.IsOpenEmbedding.functorNhds, CategoryTheory.Functor.Final.ι_colimitIso_hom, DFunLike.coe, TopologicalSpace.OpenNhds.inclusion, AlgebraicGeometry.Scheme.Modules.presheaf
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
rw :
  ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      NatTrans.app (𝟙 (restrictFunctor f ⋙ toPresheaf X ⋙ TopCat.Presheaf.stalkFunctor Ab x)) M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU
⊢ CategoryStruct.comp (Y := M.presheaf.stalk (f x)) (M.presheaf.germ (f ''ᵁ Opposite.unop (Opposite.op U)) (f x) ⋯)
      (NatTrans.app (Iso.inv (restrictStalkNatIso f x)) M) =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
rw [← germ_restrictStalkNatIso_hom_app f x M hxU, Category.assoc, ← NatTrans.comp_app,
    Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, CategoryTheory.Iso.hom_inv_id, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      NatTrans.app (𝟙 (restrictFunctor f ⋙ toPresheaf X ⋙ TopCat.Presheaf.stalkFunctor Ab x)) M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
U V : Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)
i : V ⟶ U
⊢ toOpen M U ≫ (Functor.obj modulesSpecToSheaf (tilde M)).presheaf.map i.op = toOpen M V

Tactic:
rfl

Premises used: AlgebraicGeometry.tilde.toOpen, Set.Mem, setOf, Quotient.mk', AlgebraicGeometry.StructureSheaf.const, OreLocalization.oreDiv, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
f : (↑R : Type u)
⊢ IsLocalizedModule.Away (M' :=
    (↑((Functor.obj modulesSpecToSheaf (tilde M)).presheaf.obj (op (basicOpen f))) : Type u)) f
    (ModuleCat.Hom.hom (toOpen M (basicOpen f)))

Tactic:
.of_linearEquiv (.powers f) (StructureSheaf.toOpenₗ R M (basicOpen f))
    ((modulesSpecToSheafIso M).app _).toLinearEquiv.symm

Premises used: LinearEquiv.symm, CommRingCat.carrier, PrimeSpectrum.basicOpen, Set.Mem, setOf, CategoryTheory.Iso.toLinearEquiv, AlgebraicGeometry.StructureSheaf.toOpenₗ, AlgebraicGeometry.tilde.modulesSpecToSheafIso, Submonoid.powers, ModuleCat.carrier, AlgebraicGeometry.StructureSheaf.const, CategoryTheory.Iso.app, IsLocalizedModule.of_linearEquiv
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
x : (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)
⊢ IsLocalizedModule x.asIdeal.primeCompl (ModuleCat.Hom.hom (toStalk M x))

Tactic:
inferInstanceAs (IsLocalizedModule x.asIdeal.primeCompl (StructureSheaf.toStalkₗ ..))

Premises used: _private.0.AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk._proof_1
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
H :
  ∀ (p : (Spec R).Opens) (x : (↑Γ(tilde M, p) : Type u)),
    Eq (α := (↑Γ(tilde M, p) : Type u))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (tilde.map (𝟙 M)) p) :
            (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
          x :
        (↑Γ(tilde M, p) : Type u))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (𝟙 (tilde M)) p) :
            (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
          x :
        (↑Γ(tilde M, p) : Type u))
⊢ tilde.map (𝟙 M) = 𝟙 (tilde M)

Tactic:
ext p x
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
p : (Spec R).Opens
x : (↑Γ(tilde M, p) : Type u)
⊢ Eq (α := (↑Γ(tilde M, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (tilde.map (𝟙 M)) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
        x :
      (↑Γ(tilde M, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (𝟙 (tilde M)) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
        x :
      (↑Γ(tilde M, p) : Type u))

Tactic:
Subtype.ext (funext fun y ↦ DFunLike.congr_fun (LocalizedModule.map_id _) _)

Premises used: DFunLike.congr_fun, CommRingCat.carrier, AlgebraicGeometry.StructureSheaf.comapFun._proof_2, AlgebraicGeometry.tilde.modulesSpecToSheafIso, Subtype.mk, funext, ModuleCat.Hom.hom', Opposite.op, LocalizedModule.map_id, Ideal.primeCompl, AlgebraicGeometry.tilde.map._proof_2, PrimeSpectrum.comap, Subtype.val, CategoryTheory.Iso.hom, RingHom.id, DFunLike.coe, Opposite.unop, PrimeSpectrum.asIdeal, CategoryTheory.NatTrans.app, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
p : (Spec R).Opens
x : (↑Γ(tilde M, p) : Type u)
⊢ Eq (α := (↑Γ(tilde M, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (tilde.map (𝟙 M)) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
        x :
      (↑Γ(tilde M, p) : Type u))
    ((AddCommGrpCat.Hom.hom (Scheme.Modules.Hom.app (𝟙 (tilde M)) p) :
          (a : (↑Γ(tilde M, p) : Type u)) → (↑Γ(tilde M, p) : Type u))
        x :
      (↑Γ(tilde M, p) : Type u))

Tactic:
exact Subtype.ext (funext fun y ↦ DFunLike.congr_fun (LocalizedModule.map_id _) _)

Premises used: funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N P : ModuleCat (↑R : Type u)
f : M ⟶ N
g : N ⟶ P
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))
⊢ tilde.map (f ≫ g) = tilde.map f ≫ tilde.map g

Tactic:
ext p x
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N P : ModuleCat (↑R : Type u)
f : M ⟶ N
g : N ⟶ P
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:
Subtype.ext (funext
    fun y ↦ DFunLike.congr_fun (IsLocalizedModule.map_comp' y.1.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl P) _ _) _)

Premises used: DFunLike.congr_fun, CommRingCat.carrier, IsLocalizedModule.map_comp', AlgebraicGeometry.StructureSheaf.comapFun._proof_2, AlgebraicGeometry.tilde.modulesSpecToSheafIso, Subtype.mk, funext, ModuleCat.Hom.hom', Opposite.op, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl, AlgebraicGeometry.tilde.map._proof_2, PrimeSpectrum.comap, Subtype.val, CategoryTheory.Iso.hom, RingHom.id, DFunLike.coe, Opposite.unop, PrimeSpectrum.asIdeal, CategoryTheory.NatTrans.app, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N P : ModuleCat (↑R : Type u)
f : M ⟶ N
g : N ⟶ P
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:
exact Subtype.ext (funext
    fun y ↦ DFunLike.congr_fun (IsLocalizedModule.map_comp' y.1.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl P) _ _) _)

Premises used: funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N : ModuleCat (↑R : Type u)
f : M ⟶ N
U : Opens (PrimeSpectrum (↑R : Type u))
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))
⊢ toOpen M U ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map f))) (op U) =
    f ≫ toOpen N U

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N : ModuleCat (↑R : Type u)
f : M ⟶ N
U : Opens (PrimeSpectrum (↑R : Type u))
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:
Subtype.ext (funext fun y ↦ IsLocalizedModule.map_apply y.1.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
     (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N) _ x)

Premises used: AlgebraicGeometry.StructureSheaf.Localizations.comapFun._proof_10, LinearMap.toAddHom, IsLocalizedModule.map_apply, funext, ModuleCat.carrier, LinearMap.mk, LocalizedModule.mkLinearMap, Ideal.primeCompl, Subtype.val, ModuleCat.Hom.hom, PrimeSpectrum.asIdeal, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N : ModuleCat (↑R : Type u)
f : M ⟶ N
U : Opens (PrimeSpectrum (↑R : Type u))
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:
exact Subtype.ext (funext fun y ↦ IsLocalizedModule.map_apply y.1.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
     (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N) _ x)

Premises used: funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
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))
⊢ IsIso (Y := (Functor.obj modulesSpecToSheaf (tilde M)).presheaf.obj (op ⊤)) (toOpen M ⊤)

Tactic:
rw [toOpen, isIso_comp_right_iff, ConcreteCategory.isIso_iff_bijective]

Premises used: AlgebraicGeometry.tilde.toOpen, CategoryTheory.isIso_comp_right_iff, CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
⊢ 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:
StructureSheaf.toOpenₗ_top_bijective

Premises used: Set.Mem, AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
⊢ 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:
exact StructureSheaf.toOpenₗ_top_bijective

Premises used: AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
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))
⊢ 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))

Tactic:
rw [Module.End.isUnit_iff]

Premises used: Module.End.isUnit_iff
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
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))
⊢ 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:
change Function.Bijective (algebraMap Γ(Spec R, basicOpen f)
      (Module.End Γ(Spec R, basicOpen f) Γ(M, basicOpen f)) (algebraMap R _ f))

Premises used: AlgebraicGeometry.Spec, CommRingCat.carrier, PrimeSpectrum.basicOpen, Algebra.algebraMap, AddCommGrpCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, Function.Bijective, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Module.End, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace, AlgebraicGeometry.Scheme.Modules.presheaf