awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
            0) :
        (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
    ((↑0 : (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)
    ((↑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))) sorry)))
  ((↑0 : (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 : 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 (α := 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)))
have 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 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 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))) sorry) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          b sorry)) :
    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) sorry) :
    LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
Tactic: rw [comap_apply, const_apply, const_apply]
-- 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
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ 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)
have 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 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 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))) sorry) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          b sorry)) :
    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) sorry) :
    Localization (M := S) (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
Tactic: convert_to Localization.localRingHom _ _ _ _ (Localization.mk _ _) = Localization.mk _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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.{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)
have 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) sorry :
        (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))) sorry)) :
    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: rw [comap_apply]
-- 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 : 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
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier
have rwa : p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' V.carrier
Tactic: rwa [hUV, PrimeSpectrum.comap_id]
-- 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 : 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
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier
have rwa₁ : Membership.mem (γ := Set (↑(PrimeSpectrum.Top R) : Type u)) ((fun (x : PrimeSpectrum R) ↦ x) ⁻¹' V.carrier) p
Tactic: rwa [hUV, PrimeSpectrum.comap_id]
-- 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 : 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
⊢ 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)
have 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)
Tactic: rw [hUV]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R : Type u
inst : CommRing R
U V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hUV : U = V
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)
have 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 sorry))))
  (CommRingCat.Hom.hom (eqToHom sorry))
Tactic: rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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 ⋯))
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)
have 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 sorry)))
  (CommRingCat.Hom.hom (eqToHom sorry))
Tactic: rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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 ⋯))
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)
have 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 sorry)) (CommRingCat.Hom.hom (eqToHom sorry))
Tactic: rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]
-- 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 : 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
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier
have rwa : Membership.mem (γ := Set (↑(PrimeSpectrum.Top R) : Type u)) ((fun (x : PrimeSpectrum R) ↦ x) ⁻¹' U.carrier) p
Tactic: rwa [PrimeSpectrum.comap_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R : Type u
inst : CommRing R
U : Opens (↑(PrimeSpectrum.Top R) : 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)
have 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 sorry))
  (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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.{u + 1} (α := Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
    ((↑((comap (g.comp f) U W ⋯ :
              (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)
    ((↑(((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)
have rw : 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 sorry)
          (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 sorry) :
        (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))) sorry)) :
    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: rw [comap_apply, Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal]