awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x : (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
r : R
m :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
⊢ r • m =
    HSMul.hSMul (α := (↑(Functor.obj (structurePresheafInCommRingCat R) (op U)) : Type u))
      ((algebraMap R
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                  (structureSheafInType R R))
                (op U)) :
            (a : R) → (structureSheafInType R R).obj.obj (op U))
          ((RingHom.id R : (a : R) → R) r) :
        Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R R))
          (op U))
      m

Tactic:
(IsScalarTower.algebraMap_smul Γ(R, U) r m).symm

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, IsScalarTower.algebraMap_smul, Opposite.op, AlgebraicGeometry.structureSheafInType, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x : (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
r : R
m :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
⊢ r • m =
    HSMul.hSMul (α := (↑(Functor.obj (structurePresheafInCommRingCat R) (op U)) : Type u))
      ((algebraMap R
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                  (structureSheafInType R R))
                (op U)) :
            (a : R) → (structureSheafInType R R).obj.obj (op U))
          ((RingHom.id R : (a : R) → R) r) :
        Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R R))
          (op U))
      m

Tactic:
exact (IsScalarTower.algebraMap_smul Γ(R, U) r m).symm

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, IsScalarTower.algebraMap_smul, Opposite.op, AlgebraicGeometry.structureSheafInType, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
⊢ IsScalarTower R (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
    (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u)

Tactic:
.of_algebraMap_smul fun _ _ ↦ rfl

Premises used: IsScalarTower.of_algebraMap_smul, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
r : R
α : Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x ≅
  Functor.obj
    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
      ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
    (Presheaf.stalk (structurePresheafInModuleCat R M) x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        Functor.mapCocone
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
s :
  ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
    (Functor.obj (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) (op U))
⊢ Presheaf.germ (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) U x hxU ≫ α.hom =
    CategoryTheory.Functor.map
      (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
        ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      (Presheaf.germ (structurePresheafInModuleCat R M) U x hxU)

Tactic:
have : TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
        (forget₂ _ _).map ((structurePresheafInModuleCat R M).germ U x hxU) :=
      Limits.colimit.isoColimitCocone_ι_hom (C := Ab) ..
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : (↑(PrimeSpectrum.Top R) : Type u)
r : R
m : (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)
rw :
  HSMul.hSMul (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)) (β :=
      (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (toStalk R x) :
            (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
          r :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
      ((LinearEquiv.symm (modulePresheafStalkIso R M x) :
            (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
              (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
          m :
        (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u)) =
    HSMul.hSMul (β := (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u)) r
      ((LinearEquiv.symm (modulePresheafStalkIso R M x) :
            (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
              (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
          m :
        (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
⊢ (modulePresheafStalkIso R M x :
        (a : (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u)) →
          (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
      (HSMul.hSMul (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)) (β :=
        (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (toStalk R x) :
              (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
            r :
          (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
        ((LinearEquiv.symm (modulePresheafStalkIso R M x) :
              (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
                (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
            m :
          (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))) =
    r • m

Tactic:
rw [← (modulePresheafStalkIso R M x).eq_symm_apply, map_smul]

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.modulePresheafStalkIso, LinearEquiv.eq_symm_apply, map_smul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : (↑(PrimeSpectrum.Top R) : Type u)
r : R
m : (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)
⊢ HSMul.hSMul (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)) (β :=
      (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (toStalk R x) :
            (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
          r :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
      ((LinearEquiv.symm (modulePresheafStalkIso R M x) :
            (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
              (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
          m :
        (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u)) =
    HSMul.hSMul (β := (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u)) r
      ((LinearEquiv.symm (modulePresheafStalkIso R M x) :
            (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
              (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
          m :
        (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
rw :
  Eq (α := ModuleCat.of R M ⟶ Presheaf.stalk (structurePresheafInModuleCat R M) x)
    (ModuleCat.ofHom (toOpenₗ R M U) ≫ Presheaf.germ (structurePresheafInModuleCat R M) U x hx)
    (CategoryStruct.comp (Y :=
        ModuleCat.of R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            (op ⊤)))
        (ModuleCat.ofHom (toOpenₗ R M ⊤))
        (CategoryTheory.Functor.map (structurePresheafInModuleCat R M) (Quiver.Hom.op (homOfLE ⋯))) ≫
      Presheaf.germ (structurePresheafInModuleCat R M) U x hx)
⊢ Eq (α := ModuleCat.of R M ⟶ Presheaf.stalk (structurePresheafInModuleCat R M) x)
    (ModuleCat.ofHom (toOpenₗ R M U) ≫ Presheaf.germ (structurePresheafInModuleCat R M) U x hx) (toStalkₗ' R M x)

Tactic:
rw [toStalkₗ', ← Presheaf.germ_res _ (homOfLE le_top) _ hx, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, TopCat.Presheaf.germ_res, _private.0.AlgebraicGeometry.StructureSheaf.toStalkₗ', le_top, CategoryTheory.homOfLE
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
⊢ Eq (α := ModuleCat.of R M ⟶ Presheaf.stalk (structurePresheafInModuleCat R M) x)
    (ModuleCat.ofHom (toOpenₗ R M U) ≫ Presheaf.germ (structurePresheafInModuleCat R M) U x hx)
    (CategoryStruct.comp (Y :=
        ModuleCat.of R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            (op ⊤)))
        (ModuleCat.ofHom (toOpenₗ R M ⊤))
        (CategoryTheory.Functor.map (structurePresheafInModuleCat R M) (Quiver.Hom.op (homOfLE ⋯))) ≫
      Presheaf.germ (structurePresheafInModuleCat R M) U x hx)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
x : (↑(PrimeSpectrum.Top R) : Type u)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
⊢ IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((CommRingCat.Hom.hom (Presheaf.germ (structurePresheafInCommRingCat R) (basicOpen f) x hf) :
          (a : (structureSheafInType R R).obj.obj (op (basicOpen f))) →
            (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        ((algebraMap R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R R))
                  (op (basicOpen f))) :
              (a : R) → (structureSheafInType R R).obj.obj (op (basicOpen f)))
            f :
          Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (op (basicOpen f))) :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))

Tactic:
(isUnit_basicOpen f).map ((structurePresheafInCommRingCat R).germ _ x hf).hom

Premises used: CommRingCat.Hom.hom, TopCat.Presheaf.germ, _private.0.AlgebraicGeometry.StructureSheaf.isUnit_basicOpen, IsUnit.map, AlgebraicGeometry.structurePresheafInCommRingCat
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
x : (↑(PrimeSpectrum.Top R) : Type u)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
h :
  Eq (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (toStalk R x) :
          (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        f :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((CommRingCat.Hom.hom (Presheaf.germ (structurePresheafInCommRingCat R) (basicOpen f) x hf) :
          (a : (structureSheafInType R R).obj.obj (op (basicOpen f))) →
            (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        ((algebraMap R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R R))
                  (op (basicOpen f))) :
              (a : R) → (structureSheafInType R R).obj.obj (op (basicOpen f)))
            f :
          Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (op (basicOpen f))) :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
⊢ IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (toStalk R x) :
          (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        f :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))

Tactic:
convert! (isUnit_basicOpen f).map ((structurePresheafInCommRingCat R).germ _ x hf).hom

Premises used: CommRingCat.Hom.hom, TopCat.Presheaf.germ, _private.0.AlgebraicGeometry.StructureSheaf.isUnit_basicOpen, IsUnit.map, AlgebraicGeometry.structurePresheafInCommRingCat
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
x : (↑(PrimeSpectrum.Top R) : Type u)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
⊢ Eq (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (toStalk R x) :
          (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        f :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((CommRingCat.Hom.hom (Presheaf.germ (structurePresheafInCommRingCat R) (basicOpen f) x hf) :
          (a : (structureSheafInType R R).obj.obj (op (basicOpen f))) →
            (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        ((algebraMap R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R R))
                  (op (basicOpen f))) :
              (a : R) → (structureSheafInType R R).obj.obj (op (basicOpen f)))
            f :
          Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (op (basicOpen f))) :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))

Tactic:
((structurePresheafInCommRingCat R).germ_res_apply (homOfLE (le_top : basicOpen f ≤ ⊤))
    x hf (algebraMap R Γ(R, ⊤) f)).symm

Premises used: TopCat.Presheaf.germ_res_apply, Set.Mem, setOf, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.structurePresheafInCommRingCat, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
x : (↑(PrimeSpectrum.Top R) : Type u)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
⊢ Eq (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (toStalk R x) :
          (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        f :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((CommRingCat.Hom.hom (Presheaf.germ (structurePresheafInCommRingCat R) (basicOpen f) x hf) :
          (a : (structureSheafInType R R).obj.obj (op (basicOpen f))) →
            (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        ((algebraMap R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R R))
                  (op (basicOpen f))) :
              (a : R) → (structureSheafInType R R).obj.obj (op (basicOpen f)))
            f :
          Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (op (basicOpen f))) :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))

Tactic:
exact ((structurePresheafInCommRingCat R).germ_res_apply (homOfLE (le_top : basicOpen f ≤ ⊤))
    x hf (algebraMap R Γ(R, ⊤) f)).symm

Premises used: TopCat.Presheaf.germ_res_apply, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.structurePresheafInCommRingCat, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : (↑(PrimeSpectrum.Top R) : Type u)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
⊢ IsUnit (M :=
    Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
      (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((algebraMap (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
            (Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
              (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (↑((structurePresheafInCommRingCat R).stalk x) : Type u)) →
            Module.End (↑((structurePresheafInCommRingCat R).stalk x) : Type u)
              (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (toStalk R x) :
            (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
          f) :
      Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
        (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
have := (isUnit_toStalk x f hf).map (algebraMap _
    (Module.End ((structurePresheafInCommRingCat R).stalk x)
      ((structurePresheafInModuleCat R M).stalk x)))