awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))ᶜ
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))ᶜ)
⊢ 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))ᶜ)

Tactic:
erw [Set.iInter₂_congr this]

Premises used: Set.iInter₂_congr
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))ᶜ
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}))
⊢ 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:
simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    compl_compl]

Premises used: compl_compl, TopologicalSpace.Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Set.preimage_iInter₂
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))ᶜ
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})))
⊢ 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:
rw [← PrimeSpectrum.zeroLocus_iUnion₂]

Premises used: PrimeSpectrum.zeroLocus_iUnion₂
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))
      (zeroLocus (⋃ i ∈ s, {i})))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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 = β

Tactic:
LocallyRingedSpace.forgetToSheafedSpace.map_injective
    (Spec.basicOpen_hom_ext w ?_)

Premises used: AlgebraicGeometry.Spec.basicOpen_hom_ext, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Functor.map_injective
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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)))
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 ⋯))
      (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))
⊢ X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Tactic:
refine LocallyRingedSpace.forgetToSheafedSpace.map_injective
    (Spec.basicOpen_hom_ext w ?_)

Premises used: AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Functor.map_injective
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
erw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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))

Tactic:
erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
h r

Premises used: Set.Mem, setOf, CategoryTheory.homOfLE
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact h r
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
⊢ 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

Tactic:
this
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
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
⊢ 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)))

Tactic:
convert! this
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
e_1 :
  (Γ.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:
(X.presheaf.map_id ..).symm

Premises used: Set.Mem, Set.univ, setOf, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Set.preimage, CategoryTheory.Functor.map_id, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, TopologicalSpace.Opens.leTop, Eq.symm