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
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_1 : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r 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))
⊢ (Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
          Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑(r * s) : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
          (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) =
    HMul.hMul (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u))) (β :=
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
      ((Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
              (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
            (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
              Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          ((↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
              (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
            (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
              Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          ((↑s : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)

Tactic:
(Localization.localRingHom ..).map_mul _ _

Premises used: LocalizedModule.liftOn₂, Set.Mem, Localization.localRingHom, setOf, OreLocalization.oreNum, Ideal.comap, RingHom.map_mul, OreLocalization.liftExpand, LocalizedModule.mul
-- 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_1 : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r 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))
⊢ (Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
          Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑(r * s) : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
          (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) =
    HMul.hMul (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u))) (β :=
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
      ((Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
              (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
            (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
              Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          ((↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
              (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
            (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
              Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          ((↑s : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)

Tactic:
exact (Localization.localRingHom ..).map_mul _ _

Premises used: Localization.localRingHom, RingHom.map_mul
-- 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_1 : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x : ↥(unop (op V))
dsimp :
  Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑((comapₗ f.toSemilinearMap U V hUV :
              (a : (structureSheafInType R R).obj.obj (op U)) → (structureSheafInType S S).obj.obj (op V))
            0) :
        (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
    ((↑0 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)
⊢ Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑(AddHom.toFun (M :=
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                  (structureSheafInType R R))
                (op U))
              (LinearMap.toAddHom (comapₗ f.toSemilinearMap U V hUV)) 0) :
          (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        x :
      Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑0 : (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x :
      Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))

Tactic:
dsimp
-- 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_1 : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x : ↥(unop (op V))
simp :
  Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (Ideal.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (Ideal.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
          Localization.AtPrime (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑0 : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
          (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)))
    ((↑0 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)
⊢ Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑((comapₗ f.toSemilinearMap U V hUV :
              (a : (structureSheafInType R R).obj.obj (op U)) → (structureSheafInType S S).obj.obj (op V))
            0) :
        (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
    ((↑0 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)

Tactic:
simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]

Premises used: PrimeSpectrum.comap_asIdeal, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom
-- 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_1 : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x : ↥(unop (op V))
⊢ Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (Ideal.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (Ideal.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
          Localization.AtPrime (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑0 : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
          (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)))
    ((↑0 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)

Tactic:
(Localization.localRingHom ..).map_zero

Premises used: Localization.localRingHom, RingHom.map_zero, Ideal.comap
-- 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_1 : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x : ↥(unop (op V))
⊢ Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (Ideal.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (Ideal.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
          Localization.AtPrime (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑0 : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
          (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)))
    ((↑0 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)

Tactic:
exact (Localization.localRingHom ..).map_zero

Premises used: Localization.localRingHom, RingHom.map_zero
-- 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)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥V
⊢ Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑((comap f U V hUV :
                (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf S).obj.obj (op V)) : Type u))
              s) :
          (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        p :
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
          (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : 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 f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)

Tactic:
comapₗ_eq_localRingHom ..

Premises used: AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom
-- 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)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
rw :
  Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
          (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
        (LocalizedModule.mk a
          (Subtype.mk (p := fun (x : R) ↦
            x ∈
              (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
                        (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯) :
                    (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
            b ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
    (LocalizedModule.mk ((f : (a : R) → S) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) b) ⋯) :
      LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
⊢ Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑((comap f U V hUV :
                (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf S).obj.obj (op V)) : Type u))
              (const a b U hb)) :
          (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        p :
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑(const ((f : (a : R) → S) a) ((f : (a : R) → S) b) V ⋯) :
          (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        p :
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))

Tactic:
rw [comap_apply, const_apply, const_apply]

Premises used: AlgebraicGeometry.StructureSheaf.comap_apply, AlgebraicGeometry.StructureSheaf.const_apply
-- 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)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
convert_15 :
  Eq (α := Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
          (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
        (Localization.mk a
          (Subtype.mk (p := fun (x : R) ↦
            x ∈
              (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
                        (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯) :
                    (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
            b ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
    (Localization.mk ((f : (a : R) → S) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) b) ⋯) :
      Localization (M := S) (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
⊢ Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
          (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
        (LocalizedModule.mk a
          (Subtype.mk (p := fun (x : R) ↦
            x ∈
              (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
                        (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯) :
                    (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
            b ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
    (LocalizedModule.mk ((f : (a : R) → S) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) b) ⋯) :
      LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)

Tactic:
convert_to Localization.localRingHom _ _ _ _ (Localization.mk _ _) = Localization.mk _ _

Premises used: Localization.mk, Localization.localRingHom, DFunLike.coe
-- 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)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ Eq (α := Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
          (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
        (Localization.mk a
          (Subtype.mk (p := fun (x : R) ↦
            x ∈
              (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
                        (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯) :
                    (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
            b ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
    (Localization.mk ((f : (a : R) → S) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) b) ⋯) :
      Localization (M := S) (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)

Tactic:
simp [Localization.mk_eq_mk']

Premises used: Localization.mk_eq_mk'
-- 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))
rw :
  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)))
⊢ Eq.{u + 1} (α := Localizations R (↑p : (↑(PrimeSpectrum.Top R) : Type u)))
    ((↑((comap (RingHom.id R) U V ⋯ :
              (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)
    ((↑((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)

Tactic:
rw [comap_apply]

Premises used: AlgebraicGeometry.StructureSheaf.comap_apply