awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
a : M
b : R
hb : U ≤ basicOpen b
x : ↥(unop (op V))
⊢ Eq (α := Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑((comapₗ f U V hUV : (a : (structureSheafInType R M).obj.obj (op U)) → (structureSheafInType S N).obj.obj (op V))
              (const a b U hb)) :
          (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        x :
      Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑(const ((f : (a : M) → N) a) ((σ : (a : R) → S) b) V ⋯) :
          (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        x :
      Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))

Tactic:
simp [comapₗ, comapFun]

Premises used: AlgebraicGeometry.StructureSheaf.comapₗ, AlgebraicGeometry.StructureSheaf.comapFun
-- 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
dsimp :
  Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
        ((↑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))) ⋯)) :
      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)
        ((↑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)
⊢ Eq (α := Localizations S (↑p : (↑(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))
              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:
dsimp [comapₗ, comapFun]

Premises used: AlgebraicGeometry.StructureSheaf.comapₗ, AlgebraicGeometry.StructureSheaf.comapFun
-- 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
suffices :
  Eq (α :=
    (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    (⇑(Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u))) :
      (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
        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)
⊢ Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
        ((↑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))) ⋯)) :
      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)
        ((↑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:
suffices ⇑(Localizations.comapFun f.toSemilinearMap p.1) =
      ⇑(Localization.localRingHom (PrimeSpectrum.comap f p.1).asIdeal _ f rfl) from
    congr($this _)
-- 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
h :
  ∀ (m : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))),
    Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
      ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
            (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
              Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
          m :
        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)
          m :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
⊢ Eq (α :=
    (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    (⇑(Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u))) :
      (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
        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)

Tactic:
ext m
-- 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_1 :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥V
m : R
s : ↥(PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal.primeCompl
⊢ Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
        (LocalizedModule.mk m s) :
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    (LocalizedModule.mk ((f : (a : R) → S) m)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) (↑s : R)) ⋯) :
      LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)

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)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s_1 :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥V
m : R
s : ↥(PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal.primeCompl
convert_15 :
  Eq (α := Localization (M := S) (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
    (Localization.mk ((f : (a : R) → S) m)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) (↑s : R)) ⋯) :
      Localization (M := S) (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
    ((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 m s) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
⊢ Eq (α := LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
    (LocalizedModule.mk ((f : (a : R) → S) m)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) (↑s : R)) ⋯) :
      LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
    ((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 m s) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)

Tactic:
convert_to Localization.mk _ _ = Localization.localRingHom _ _ _ _ (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
s_1 :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥V
m : R
s : ↥(PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal.primeCompl
⊢ Eq (α := Localization (M := S) (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
    (Localization.mk ((f : (a : R) → S) m)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) (↑s : R)) ⋯) :
      Localization (M := S) (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
    ((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 m s) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)

Tactic:
simp [Localization.mk_eq_mk']

Premises used: Localization.mk_eq_mk'
-- 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
m : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
h :
  ∀ (m : R) (s : ↥(PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal.primeCompl),
    Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
      ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
            (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
              Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
          (LocalizedModule.mk m s) :
        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 m s) :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
⊢ Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
        m :
      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)
        m :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)

Tactic:
induction m using LocalizedModule.induction_on with | h m s =>
  trans LocalizedModule.mk (f m) ⟨f ↑s, s.2⟩
  · simp
  convert_to Localization.mk _ _ = Localization.localRingHom _ _ _ _ (Localization.mk _ _)
  simp [Localization.mk_eq_mk']

Premises used: Localization.mk, Localization.mk_eq_mk', Localization.localRingHom, DFunLike.coe
-- 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))
            1) :
        (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
    ((↑1 : (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)) 1) :
          (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        x :
      Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑1 : (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)
      ((↑1 : (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))) ⋯)))
    ((↑1 : (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))
            1) :
        (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
    ((↑1 : (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)
      ((↑1 : (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))) ⋯)))
    ((↑1 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)

Tactic:
(Localization.localRingHom ..).map_one

Premises used: Localization.localRingHom, RingHom.map_one, 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)
      ((↑1 : (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))) ⋯)))
    ((↑1 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)

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

Premises used: Localization.localRingHom, RingHom.map_one