awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U V : Opens (↑(PrimeSpectrum.Top R) : Type u)
iVU : V ⟶ U
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥(unop (op V))
⊢ Eq (α := Localizations R (↑p : (↑(PrimeSpectrum.Top R) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap (RingHom.id R) (↑p : (↑(PrimeSpectrum.Top R) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal (RingHom.id R) ⋯ :
          (a :
              Localization.AtPrime
                (PrimeSpectrum.comap (RingHom.id R) (↑p : (↑(PrimeSpectrum.Top R) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal)
        ((↑s : (x : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
            (PrimeSpectrum.comap (RingHom.id R) (↑p : (↑(PrimeSpectrum.Top R) : Type u))) ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal)
    ((↑((CommRingCat.Hom.hom
                  (CategoryTheory.Functor.map
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                      (structureSheaf R))
                    iVU.op) :
                (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf R).obj.obj (op V)) : Type u))
              s) :
          (x : ↥(unop (op V))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        p :
      Localizations R (↑p : (↑(PrimeSpectrum.Top R) : Type u)))

Tactic:
congr($(Localization.localRingHom_id ..) _)

Premises used: congrArg, Localization.localRingHom_id, id, Subtype.mk, PrimeSpectrum.comap, Subtype.val, RingHom.id, DFunLike.coe, CategoryTheory.leOfHom, PrimeSpectrum.asIdeal, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U V : Opens (↑(PrimeSpectrum.Top R) : Type u)
iVU : V ⟶ U
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥(unop (op V))
⊢ Eq (α := Localizations R (↑p : (↑(PrimeSpectrum.Top R) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap (RingHom.id R) (↑p : (↑(PrimeSpectrum.Top R) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal (RingHom.id R) ⋯ :
          (a :
              Localization.AtPrime
                (PrimeSpectrum.comap (RingHom.id R) (↑p : (↑(PrimeSpectrum.Top R) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal)
        ((↑s : (x : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
            (PrimeSpectrum.comap (RingHom.id R) (↑p : (↑(PrimeSpectrum.Top R) : Type u))) ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal)
    ((↑((CommRingCat.Hom.hom
                  (CategoryTheory.Functor.map
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                      (structureSheaf R))
                    iVU.op) :
                (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf R).obj.obj (op V)) : Type u))
              s) :
          (x : ↥(unop (op V))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        p :
      Localizations R (↑p : (↑(PrimeSpectrum.Top R) : Type u)))

Tactic:
exact congr($(Localization.localRingHom_id ..) _)
-- 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
S_1 : Type u
inst_5 : CommRing S_1
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S_1 N
σ : R →+* S_1
f : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
U V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hUV : U = V
p : (↑(PrimeSpectrum.Top R) : Type u)
hpV : p ∈ V.carrier
rwa : p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' V.carrier
rwa₁ rwa₂ rwa₃ rwa₄ :
  Membership.mem (γ := Set (↑(PrimeSpectrum.Top R) : Type u)) ((fun (x : PrimeSpectrum R) ↦ x) ⁻¹' V.carrier) p
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
rwa [hUV, PrimeSpectrum.comap_id]

Premises used: PrimeSpectrum.comap_id
-- 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
S_1 : Type u
inst_5 : CommRing S_1
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S_1 N
σ : R →+* S_1
f : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
U V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hUV : U = V
rw rw₁ :
  Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheaf R))
      (op V) =
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheaf R))
      (op V)
⊢ Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheaf R))
      (op U) =
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheaf R))
      (op V)

Tactic:
rw [hUV]
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hUV : U = V
rw :
  Eq (α :=
    (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u) →+*
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op V)) :
        Type u))
    (CommRingCat.Hom.hom
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (Quiver.Hom.op (eqToHom ⋯))))
    (CommRingCat.Hom.hom (eqToHom ⋯))
rw₁ :
  Eq (α :=
    (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u) →+*
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op V)) :
        Type u))
    (CommRingCat.Hom.hom
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (eqToHom ⋯)))
    (CommRingCat.Hom.hom (eqToHom ⋯))
rw₂ rw₃ :
  Eq (α :=
    (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u) →+*
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op V)) :
        Type u))
    (CommRingCat.Hom.hom (eqToHom ⋯)) (CommRingCat.Hom.hom (eqToHom ⋯))
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom, CategoryTheory.eqToHom_op, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, Eq.symm
-- 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
S_1 : Type u
inst_5 : CommRing S_1
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S_1 N
σ : R →+* S_1
f : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
p : (↑(PrimeSpectrum.Top R) : Type u)
hpU : p ∈ U.carrier
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (γ := Set (↑(PrimeSpectrum.Top R) : Type u)) ((fun (x : PrimeSpectrum R) ↦ x) ⁻¹' U.carrier) p
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
rwa [PrimeSpectrum.comap_id]

Premises used: PrimeSpectrum.comap_id
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
rw :
  Eq.{u + 1} (α :=
    (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u) →+*
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u))
    (CommRingCat.Hom.hom (eqToHom ⋯))
    (RingHom.id
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u))
⊢ comap (RingHom.id R) U U ⋯ =
    RingHom.id
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u)

Tactic:
rw [comap_id rfl]

Premises used: AlgebraicGeometry.StructureSheaf.comap_id, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
⊢ Eq.{u + 1} (α :=
    (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u) →+*
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u))
    (CommRingCat.Hom.hom (eqToHom ⋯))
    (RingHom.id
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op U)) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
P : Type u
inst_2 : CommRing P
f : R →+* S
g : S →+* P
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
W : Opens (↑(PrimeSpectrum.Top P) : Type u)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥(unop (op W))
⊢ Eq (α := Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
    ((RingHom.comp (β := Localization.AtPrime (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal)
            (Localization.localRingHom (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
              (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal g ⋯)
            (Localization.localRingHom (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
              (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal f ⋯) :
          (a : Localization.AtPrime (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal)
        ((↑s : (x : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
            (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))) ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal)
    ((↑(((comap g V W hVW).comp (comap f U V hUV) :
                (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf P).obj.obj (op W)) : Type u))
              s) :
          (x : ↥(unop (op W))) → Localizations P (↑x : (↑(PrimeSpectrum.Top P) : Type u)))
        p :
      Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
P : Type u
inst_2 : CommRing P
f : R →+* S
g : S →+* P
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
W : Opens (↑(PrimeSpectrum.Top P) : Type u)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥(unop (op W))
⊢ (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal =
    Ideal.comap f (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
P : Type u
inst_2 : CommRing P
f : R →+* S
g : S →+* P
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
W : Opens (↑(PrimeSpectrum.Top P) : Type u)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥(unop (op W))
⊢ (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal =
    Ideal.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x_1 : (↑(CommRingCat.of R) : Type u)
x :
  ↥(unop
        (op
          ((Opens.comap
                { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ : C(PrimeSpectrum S, PrimeSpectrum R) } :
              (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
            U)) :
      Opens (↑(PrimeSpectrum.Top S) : Type u))
⊢ Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
          (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
          Localization.AtPrime (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑((algebraMap R
                  (↑(Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                          (structureSheaf R))
                        (op U)) :
                    Type u) :
                (a : R) → (↑((structureSheaf R).obj.obj (op U)) : Type u))
              x_1) :
          (x : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
          (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)))
    ((↑((algebraMap S
                (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top S) : Type u))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                        (structureSheaf S))
                      (op
                        ((Opens.comap
                              { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ :
                                C(PrimeSpectrum S, PrimeSpectrum R) } :
                            (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                          U))) :
                  Type u) :
              (a : S) →
                (↑((structureSheaf S).obj.obj
                      (op
                        ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                            (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                          U))) :
                  Type u))
            ((f : (a : R) → S) x_1)) :
        (x :
            ↥((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                  (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                U)) →
          Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)

Tactic:
Localization.localRingHom_to_map _ _ _ _ _

Premises used: Localization.localRingHom_to_map, Set.Mem, setOf, Quotient.mk', OreLocalization.oreDiv
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x_1 : (↑(CommRingCat.of R) : Type u)
x :
  ↥(unop
        (op
          ((Opens.comap
                { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ : C(PrimeSpectrum S, PrimeSpectrum R) } :
              (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
            U)) :
      Opens (↑(PrimeSpectrum.Top S) : Type u))
⊢ Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
          (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
          Localization.AtPrime (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑((algebraMap R
                  (↑(Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                          (structureSheaf R))
                        (op U)) :
                    Type u) :
                (a : R) → (↑((structureSheaf R).obj.obj (op U)) : Type u))
              x_1) :
          (x : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
          (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)))
    ((↑((algebraMap S
                (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top S) : Type u))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                        (structureSheaf S))
                      (op
                        ((Opens.comap
                              { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ :
                                C(PrimeSpectrum S, PrimeSpectrum R) } :
                            (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                          U))) :
                  Type u) :
              (a : S) →
                (↑((structureSheaf S).obj.obj
                      (op
                        ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                            (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                          U))) :
                  Type u))
            ((f : (a : R) → S) x_1)) :
        (x :
            ↥((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                  (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                U)) →
          Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)

Tactic:
exact Localization.localRingHom_to_map _ _ _ _ _

Premises used: Localization.localRingHom_to_map