awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
p : PrimeSpectrum (↑(Γ.obj (op X)) : Type u) := X.toΓSpecFun x
S : CommRingCat := stalk (TopCat.Sheaf.presheaf (structureSheaf (↑(Γ.obj (op X)) : Type u))) p
t : (↑S : Type u)
ht :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
          (a :
              (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
                    ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u)) →
            (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
r : (↑(Γ.obj (op X)) : Type u)
s : ↥p.asIdeal.primeCompl
t' : (↑S : Type u) :=
  (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
      (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
    (↑s : (↑(X.presheaf.obj (op ⊤)) : Type u))
he :
  t * t' =
    (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r
⊢ r ∈ p.asIdeal.primeCompl
have map_nonunit : IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.Γgerm x) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
      r :
    (↑(X.presheaf.stalk x) : Type u))
Tactic: apply (notMem_prime_iff_unit_in_stalk _ _ _).mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
i : (↑(Γ.obj (op X)) : Type u)
h : i ∈ s
⊢ (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
    Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (Opens.carrier (basicOpen i))ᶜ
have symm : Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          X.toΓSpec.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
        (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (Opens.carrier (basicOpen i))ᶜ =
  (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
i : (↑(Γ.obj (op X)) : Type u)
h : i ∈ s
⊢ ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpec.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u)) ⁻¹'
        (↑(basicOpen i) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))))ᶜ =
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ
have erw : (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
  (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ
Tactic: erw [X.toΓSpec_preimage_basicOpen_eq i]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (hypothesis)
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
⊢ Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (zeroLocus s))
    (⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ)
have this : ∀ i ∈ s,
  (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
    Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (Opens.carrier (basicOpen i))ᶜ
Tactic: have (i : LocallyRingedSpace.Γ.obj (op X)) (_ : i ∈ s) :
      (SetLike.coe (X.toRingedSpace.basicOpen i))ᶜ =
        X.toΓSpec.base ⁻¹' ((PrimeSpectrum.basicOpen i).carrier)ᶜ := by
    symm
    rw [Set.preimage_compl, Opens.carrier_eq_coe]
    erw [X.toΓSpec_preimage_basicOpen_eq i]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
this :
  ∀ i ∈ s,
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
      Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpec.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (Opens.carrier (basicOpen i))ᶜ
⊢ Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (zeroLocus s))
    (⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ)
have erw : Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
  (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          X.toΓSpec.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
        (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (zeroLocus s))
  (⋂ i ∈ s,
    Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (Opens.carrier (basicOpen i))ᶜ)
Tactic: erw [Set.iInter₂_congr this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
this :
  ∀ i ∈ s,
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
      Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpec.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (Opens.carrier (basicOpen i))ᶜ
⊢ Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (zeroLocus s))
    (⋂ i ∈ s,
      Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpec.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (Opens.carrier (basicOpen i))ᶜ)
have simp_rw : Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
  (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          X.toΓSpec.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
        (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (zeroLocus s))
  (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          X.toΓSpec.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
        (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (⋂ i ∈ s, zeroLocus {i}))
Tactic: simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    compl_compl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
this :
  ∀ i ∈ s,
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
      Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpec.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (Opens.carrier (basicOpen i))ᶜ
⊢ Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (zeroLocus s))
    (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⋂ i ∈ s, zeroLocus {i}))
have rw : Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
  (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          X.toΓSpec.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
        (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (zeroLocus s))
  (Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          X.toΓSpec.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
        (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
    (zeroLocus (⋃ i ∈ s, {i})))
Tactic: rw [← PrimeSpectrum.zeroLocus_iUnion₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : (↑R : Type u)),
    Eq (α := R ⟶ X.presheaf.obj (op ((Opens.map β.base).obj (basicOpen r))))
      (f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r)))
⊢ X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β
have refine : ∀ (r : (↑R : Type u)),
  let U : Opens (PrimeSpectrum (↑R : Type u)) := basicOpen r;
  Eq (α :=
    CommRingCat.of (↑R : Type u) ⟶
      (forgetToSheafedSpace.obj X).presheaf.obj ((Opens.map (forgetToSheafedSpace.map β).hom.base).op.obj (op U)))
    ((CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op U))) ≫
        (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.c.app (op U)) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom sorry))
    (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U))
Tactic: refine LocallyRingedSpace.forgetToSheafedSpace.map_injective
    (Spec.basicOpen_hom_ext w ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : (↑R : Type u)),
    Eq (α := R ⟶ X.presheaf.obj (op ((Opens.map β.base).obj (basicOpen r))))
      (f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r)))
r : (↑R : Type u)
U : Opens (PrimeSpectrum (↑R : Type u)) := basicOpen r
⊢ Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj (op ((Opens.map β.base).obj U)))
    (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      CategoryStruct.comp (Y := X.presheaf.obj (op ((Opens.map X.toΓSpecBase).obj ((Opens.map (Spec.topMap f)).obj U))))
        (CommRingCat.ofHom
            (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u)
              (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(X.presheaf.obj (op ⊤)) : Type u)) : Type u))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf
                        (Opens.grothendieckTopology
                          (↑(PrimeSpectrum.Top (↑(X.presheaf.obj (op ⊤)) : Type u)) : Type u)))
                      (structureSheaf (↑(X.presheaf.obj (op ⊤)) : Type u)))
                    (op
                      ((Opens.comap
                            { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ :
                              C(PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u), PrimeSpectrum (↑R : Type u)) } :
                          (a : Opens (PrimeSpectrum (↑R : Type u))) →
                            Opens (PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u)))
                        U))) :
                Type u)) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.topMap f)).obj U)))
        (X.presheaf.map (eqToHom ⋯)))
    (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op U))) ≫
      β.c.app (op U))
have erw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (hypothesis)
Goal:
X : LocallyRingedSpace
⊢ Eq (α := Γ.obj (op X) ⟶ (Functor.obj (pushforward CommRingCat X.toΓSpec.base) X.presheaf).obj (op ⊤))
    (CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)) : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (op (Γ.obj (op X)))) : Type u) (↑(unop (op (Γ.obj (op X)))) : Type u)))
            (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤))
    (𝟙 (Γ.obj (op X)))
have this : Eq (α :=
  CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
    (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).obj (op (basicOpen 1)))
  (CommRingCat.ofHom
      (algebraMap (↑(Γ.obj (op X)) : Type u)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u)))
            (structureSheafInType (↑(unop (op (Γ.obj (op X)))) : Type u) (↑(unop (op (Γ.obj (op X)))) : Type u)))
          (op (basicOpen 1)))) ≫
    X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen 1)))
  (X.toToΓSpecMapBasicOpen 1)
Tactic: have := X.toΓSpecSheafedSpace_app_spec 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)) : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (op (Γ.obj (op X)))) : Type u) (↑(unop (op (Γ.obj (op X)))) : Type u)))
            (op ⊤))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op ⊤) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
⊢ Eq (α := Γ.obj (op X) ⟶ (Functor.obj (pushforward CommRingCat X.toΓSpec.base) X.presheaf).obj (op ⊤))
    (CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)) : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (op (Γ.obj (op X)))) : Type u) (↑(unop (op (Γ.obj (op X)))) : Type u)))
            (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤))
    (𝟙 (Γ.obj (op X)))
have h : (Γ.obj (op X) ⟶ (Functor.obj (pushforward CommRingCat X.toΓSpec.base) X.presheaf).obj (op ⊤)) =
    (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).obj (op ⊤)) →
  𝟙 (Γ.obj (op X)) = X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec =
    X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f
have symm : X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f =
  CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f =
    CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec
have w : PresheafedSpace.Hom.base (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) X).toΓSpec) ≫
    (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base =
  PresheafedSpace.Hom.base (Hom.toHom (CategoryTheory.Functor.map (𝟭 LocallyRingedSpace) f ≫ Y.toΓSpec))
Tactic: apply LocallyRingedSpace.comp_ring_hom_ext