awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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.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)
have 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))) sorry)) :
    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 sorry :
        (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))) sorry)) :
    Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
Tactic: dsimp [comapₗ, comapFun]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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)))
    ((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)
have 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 sorry) :
    (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
      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 _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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 (α :=
    (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)
have 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 sorry :
          (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: ext m
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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)))
    ((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)
have trans : 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)) sorry) :
    LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
Tactic: trans LocalizedModule.mk (f m) ⟨f ↑s, s.2⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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
trans :
  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)
⊢ 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)
have trans₁ : 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)) sorry) :
    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 sorry :
        (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: trans LocalizedModule.mk (f m) ⟨f ↑s, s.2⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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 (α := 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)
have 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)) sorry) :
    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 sorry :
        (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: convert_to Localization.mk _ _ = Localization.localRingHom _ _ _ _ (Localization.mk _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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)))
⊢ 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)
have 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 sorry :
          (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: 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']
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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)))
    ((↑(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)))
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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)))
    ((↑((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)
have 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 sorry :
      (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))) sorry)))
  ((↑1 : (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u))) x)
Tactic: simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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)))
    ((↑(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)))
have 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)
Tactic: dsimp