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
f : R
⊢ IsIso (C := ModuleCat R) (X := ModuleCat.of R (LocalizedModule.Away f M)) (ModuleCat.ofHom (toBasicOpenₗ R M f))

Tactic:
(ConcreteCategory.isIso_iff_bijective _).mpr ⟨toBasicOpenₗ_injective _, toBasicOpenₗ_surjective _⟩

Premises used: Iff.mpr, _private.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_injective, CategoryTheory.ConcreteCategory.isIso_iff_bijective, And.intro, _private.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_surjective
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsLocalizedModule (M' :=
    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 (basicOpen 1)))
    (Submonoid.powers 1) (toOpenₗ R M (basicOpen 1))

Tactic:
(inferInstance : IsLocalizedModule (.powers 1) (toOpenₗ R M (basicOpen 1)))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a :
  IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤) ↔
    IsLocalizedModule (M' :=
      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 (basicOpen 1)))
      (Submonoid.powers 1) (toOpenₗ R M (basicOpen 1))
⊢ IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)

Tactic:
convert! (inferInstance : IsLocalizedModule (.powers 1) (toOpenₗ R M (basicOpen 1)))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a :
  IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤) ↔
    IsLocalizedModule (M' :=
      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 ⊤))
      (Submonoid.powers 1) (toOpenₗ R M ⊤)
a₁ a₂ :
  IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤) ↔
    IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤)
⊢ IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤) ↔
    IsLocalizedModule (M' :=
      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 (basicOpen 1)))
      (Submonoid.powers 1) (toOpenₗ R M (basicOpen 1))

Tactic:
rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]

Premises used: Submonoid.powers_one, PrimeSpectrum.basicOpen_one
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)

Tactic:
have : IsLocalizedModule ⊥ (toOpenₗ R M ⊤) := by
    convert! (inferInstance : IsLocalizedModule (.powers 1) (toOpenₗ R M (basicOpen 1)))
    rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
this :
  IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
x y : M
e :
  Eq (α :=
    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 ⊤))
    ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) x :
      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 ⊤))
    ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) y :
      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 ⊤))
⊢ x = y

Tactic:
simpa using (IsLocalizedModule.eq_iff_exists ⊥ _).mp e

Premises used: Bot.bot, Iff.mp, IsLocalizedModule.eq_iff_exists
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
this :
  IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
refine :
  ∀
    (x :
      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 ⊤)),
    ∃ (a : M), (toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) a = x
⊢ Function.Bijective (α := M) (β :=
    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 ⊤))
    (⇑(toOpenₗ R M ⊤) : (a : M) → (structureSheafInType R M).obj.obj (op ⊤))

Tactic:
refine ⟨fun x y e ↦ by simpa using (IsLocalizedModule.eq_iff_exists ⊥ _).mp e, fun x ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
this :
  IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
x :
  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 ⊤)
obtain :
  ∀ (x : M),
    ∃ (a : M),
      Eq (α :=
        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 ⊤))
        ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) a :
          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 ⊤))
        (Function.uncurry (β := ↥⊥) (IsLocalizedModule.mk' (toOpenₗ R M ⊤))
            (x, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 ⋯) :
          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 ⊤))
⊢ ∃ (a : M), (toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) a = x

Tactic:
obtain ⟨⟨x, _, rfl⟩, rfl⟩ := IsLocalizedModule.mk'_surjective ⊥ (toOpenₗ R M ⊤) x

Premises used: AlgebraicGeometry.StructureSheaf.toOpenₗ, Bot.bot, IsLocalizedModule.mk'_surjective, Top.top, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
this :
  IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
x : M
⊢ ∃ (a : M),
    Eq (α :=
      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 ⊤))
      ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) a :
        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 ⊤))
      (Function.uncurry (β := ↥⊥) (IsLocalizedModule.mk' (toOpenₗ R M ⊤))
          (x, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 ⋯) :
        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 ⊤))

Tactic:
⟨x, (IsLocalizedModule.mk'_one ..).symm⟩

Premises used: IsLocalizedModule.mk'_one, Exists.intro, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
this :
  IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
x : M
⊢ ∃ (a : M),
    Eq (α :=
      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 ⊤))
      ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) a :
        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 ⊤))
      (Function.uncurry (β := ↥⊥) (IsLocalizedModule.mk' (toOpenₗ R M ⊤))
          (x, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 ⋯) :
        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 ⊤))

Tactic:
exact ⟨x, (IsLocalizedModule.mk'_one ..).symm⟩
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
⊢ Function.Bijective (α := 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 ⊤))
    (⇑(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 ⊤))) :
      (a : R) → (structureSheafInType R R).obj.obj (op ⊤))

Tactic:
toOpenₗ_top_bijective

Premises used: Set.Mem, setOf, Quotient.mk', AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.StructureSheaf.const, OreLocalization.oreDiv
-- 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
f : R
⊢ IsLocalization.Away 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)))

Tactic:
(isLocalizedModule_iff_isLocalization' _ _).mp <|
    inferInstanceAs (IsLocalizedModule.Away f (toOpenₗ R R (basicOpen f)))

Premises used: isLocalizedModule_iff_isLocalization', Iff.mp, _private.0.AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpen._proof_1
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x : (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
rw :
  Eq (α := CommRingCat.of R ⟶ Presheaf.stalk (structurePresheafInCommRingCat R) x)
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (op U))) ≫
      Presheaf.germ (structurePresheafInCommRingCat R) U x hxU)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (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 ⊤)))
      (CommRingCat.ofHom
        (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 ⊤))))
      (CategoryTheory.Functor.map (structurePresheafInCommRingCat R) (Quiver.Hom.op (homOfLE ⋯)) ≫
        Presheaf.germ (structurePresheafInCommRingCat R) U x hxU))
⊢ Eq (α := CommRingCat.of R ⟶ Presheaf.stalk (structurePresheafInCommRingCat R) x)
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (op U))) ≫
      Presheaf.germ (structurePresheafInCommRingCat R) U x hxU)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (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 ⊤)))
      (CommRingCat.ofHom
        (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 ⊤))))
      (Presheaf.germ (structurePresheafInCommRingCat R) ⊤ x _root_.trivial))

Tactic:
rw [← (structurePresheafInCommRingCat R).germ_res (homOfLE (le_top : U ≤ ⊤)) _ hxU]

Premises used: TopCat.Presheaf.germ_res, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.structurePresheafInCommRingCat
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x : (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
⊢ Eq (α := CommRingCat.of R ⟶ Presheaf.stalk (structurePresheafInCommRingCat R) x)
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (op U))) ≫
      Presheaf.germ (structurePresheafInCommRingCat R) U x hxU)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (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 ⊤)))
      (CommRingCat.ofHom
        (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 ⊤))))
      (CategoryTheory.Functor.map (structurePresheafInCommRingCat R) (Quiver.Hom.op (homOfLE ⋯)) ≫
        Presheaf.germ (structurePresheafInCommRingCat R) U x hxU))

Tactic:
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
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)
e_a :
  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
⊢ Eq (α := (↑(Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
    (ZeroHom.toFun
      (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) U x hxU)) :
        ZeroHom (↑((moduleStructurePresheaf R M).presheaf.obj (op U)) : Type u)
          (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
      (r • m))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (X := Functor.obj (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) (op U))
          (Y := Presheaf.stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x)
          (Presheaf.germ (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) U x hxU) :
        (a : (↑((moduleStructurePresheaf R M).presheaf.obj (op U)) : Type u)) →
          (↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
      (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:
congr 1