awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
w :
  PresheafedSpace.Hom.base
        (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec) ≫
      (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base =
    (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).base
h :
  ∀ (r : (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)),
    Eq (α :=
      unop (op (Functor.obj (𝟭 CommRingCat) R)) ⟶
        (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).presheaf.obj
          (op
            ((Opens.map
                  (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).base).obj
              (basicOpen r))))
      ((SpecΓIdentity.inv.app R).op.unop ≫
        (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map
          (Quiver.Hom.op (homOfLE ⋯)))
      (CommRingCat.ofHom
          (algebraMap (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)
            (Functor.obj (C :=
              (Opens (↑(PrimeSpectrum.Top (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)) : Type u_1))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology
                    (↑(PrimeSpectrum.Top (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)) : Type u_1)))
                (structureSheafInType (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)
                  (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)))
              (op (basicOpen r)))) ≫
        (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).c.app
          (op (basicOpen r)))
⊢ identityToΓSpec.app (Spec.toLocallyRingedSpace.obj (op R)) ≫
      Spec.toLocallyRingedSpace.map (SpecΓIdentity.inv.app R).op =
    𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R)))

Tactic:
apply LocallyRingedSpace.comp_ring_hom_ext

Premises used: AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
w :
  ∀ (p : PrimeSpectrum (↑R : Type u_1)),
    Eq (α :=
      (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
        Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier)
              (PresheafedSpace.Hom.base
                  (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec) ≫
                (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base) :
            (a :
                (↑(↑((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toPresheafedSpace : TopCat) :
                  Type u_1)) →
              (↑(↑(Spec.locallyRingedSpaceObj (unop (op ((𝟭 CommRingCat).obj R)))).toPresheafedSpace : TopCat) :
                Type u_1))
          p :
        (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
          Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier)
              (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).base :
            (a :
                (↑(↑((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toPresheafedSpace : TopCat) :
                  Type u_1)) →
              (↑(↑(Spec.locallyRingedSpaceObj (unop (op ((𝟭 CommRingCat).obj R)))).toPresheafedSpace : TopCat) :
                Type u_1))
          p :
        (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
          Type u_1))
⊢ PresheafedSpace.Hom.base
        (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec) ≫
      (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base =
    (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).base

Tactic:
ext (p : PrimeSpectrum R)

Premises used: CommRingCat.carrier, PrimeSpectrum
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
w :
  (TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
        (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
          PrimeSpectrum (↑R : Type u_1))
      (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
            C((↑(Spec.topObj R) : Type u_1),
              (↑(Spec.topObj
                    (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                        (structureSheaf (↑R : Type u_1)))
                      (op ⊤))) :
                Type u_1))) :
          (a : PrimeSpectrum (↑R : Type u_1)) →
            PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
        p) =
    p
⊢ Eq (α :=
    (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (PresheafedSpace.Hom.base
                (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec) ≫
              (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base) :
          (a :
              (↑(↑((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toPresheafedSpace : TopCat) :
                Type u_1)) →
            (↑(↑(Spec.locallyRingedSpaceObj (unop (op ((𝟭 CommRingCat).obj R)))).toPresheafedSpace : TopCat) :
              Type u_1))
        p :
      (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).base :
          (a :
              (↑(↑((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toPresheafedSpace : TopCat) :
                Type u_1)) →
            (↑(↑(Spec.locallyRingedSpaceObj (unop (op ((𝟭 CommRingCat).obj R)))).toPresheafedSpace : TopCat) :
              Type u_1))
        p :
      (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
        Type u_1))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
⊢ (TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
        (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
          PrimeSpectrum (↑R : Type u_1))
      (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
            C((↑(Spec.topObj R) : Type u_1),
              (↑(Spec.topObj
                    (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                        (structureSheaf (↑R : Type u_1)))
                      (op ⊤))) :
                Type u_1))) :
          (a : PrimeSpectrum (↑R : Type u_1)) →
            PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
        p) =
    p

Tactic:
PrimeSpectrum.ext (Ideal.ext fun x => ?_)

Premises used: PrimeSpectrum.ext, Ideal.ext
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
w :
  ∀ (x : (↑R : Type u_1)),
    Membership.mem (γ := Ideal (↑R : Type u_1))
        (asIdeal
          ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
              (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
                PrimeSpectrum (↑R : Type u_1))
            (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
                  C((↑(Spec.topObj R) : Type u_1),
                    (↑(Spec.topObj
                          (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                            (ObjectProperty.FullSubcategory.obj (P :=
                              Presheaf.IsSheaf
                                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                              (structureSheaf (↑R : Type u_1)))
                            (op ⊤))) :
                      Type u_1))) :
                (a : PrimeSpectrum (↑R : Type u_1)) →
                  PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
              p)))
        x ↔
      x ∈ p.asIdeal
⊢ (TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
        (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
          PrimeSpectrum (↑R : Type u_1))
      (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
            C((↑(Spec.topObj R) : Type u_1),
              (↑(Spec.topObj
                    (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                        (structureSheaf (↑R : Type u_1)))
                      (op ⊤))) :
                Type u_1))) :
          (a : PrimeSpectrum (↑R : Type u_1)) →
            PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
        p) =
    p

Tactic:
refine PrimeSpectrum.ext (Ideal.ext fun x => ?_)

Premises used: PrimeSpectrum.ext, Ideal.ext
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
x : (↑R : Type u_1)
⊢ Membership.mem (γ := Ideal (↑R : Type u_1))
      (asIdeal
        ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
            (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
              PrimeSpectrum (↑R : Type u_1))
          (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
                C((↑(Spec.topObj R) : Type u_1),
                  (↑(Spec.topObj
                        (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            Presheaf.IsSheaf
                              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                            (structureSheaf (↑R : Type u_1)))
                          (op ⊤))) :
                    Type u_1))) :
              (a : PrimeSpectrum (↑R : Type u_1)) →
                PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
            p)))
      x ↔
    Membership.mem (α := (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1)) (γ :=
      Ideal (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
      (IsLocalRing.maximalIdeal (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
      ((algebraMap (↑R : Type u_1) (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1) :
            (a : (↑R : Type u_1)) → (↑((structureSheaf (↑R : Type u_1)).presheaf.stalk p) : Type u_1))
          x :
        (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
r : (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)
⊢ Eq (α :=
    unop (op (Functor.obj (𝟭 CommRingCat) R)) ⟶
      (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).presheaf.obj
        (op
          ((Opens.map
                (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).base).obj
            (basicOpen r))))
    ((SpecΓIdentity.inv.app R).op.unop ≫
      (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map
        (Quiver.Hom.op (homOfLE ⋯)))
    (CommRingCat.ofHom
        (algebraMap (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)
          (Functor.obj (C :=
            (Opens (↑(PrimeSpectrum.Top (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)) : Type u_1))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology
                  (↑(PrimeSpectrum.Top (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)) : Type u_1)))
              (structureSheafInType (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)
                (↑(unop (op (Functor.obj (𝟭 CommRingCat) R))) : Type u_1)))
            (op (basicOpen r)))) ≫
      (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).c.app
        (op (basicOpen r)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
simp :
  Quiver.Hom.op ((identityToΓSpec.app X).c.app (op ⊤)) ≫ Quiver.Hom.op (toSpecΓ (X.presheaf.obj (op ⊤))) =
    𝟙 (op (X.presheaf.obj (op ⊤)))
⊢ Γ.rightOp.map (identityToΓSpec.app X) ≫ (NatIso.op SpecΓIdentity).inv.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)

Tactic:
simp only [Functor.id_obj, Functor.rightOp_obj, Γ_obj, Functor.comp_obj,
      Spec.toLocallyRingedSpace_obj, Spec.locallyRingedSpaceObj_toSheafedSpace,
      Spec.sheafedSpaceObj_carrier, Spec.sheafedSpaceObj_presheaf, Functor.rightOp_map, Γ_map,
      Quiver.Hom.unop_op, NatIso.op_inv, NatTrans.op_app, SpecΓIdentity_inv_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.rightOp_map, Quiver.Hom.unop_op, AlgebraicGeometry.Spec.sheafedSpaceObj_carrier, AlgebraicGeometry.Spec.toLocallyRingedSpace_obj, CategoryTheory.Functor.rightOp_obj, AlgebraicGeometry.Spec.locallyRingedSpaceObj_toSheafedSpace, CategoryTheory.NatTrans.op_app, AlgebraicGeometry.LocallyRingedSpace.Γ_map, CategoryTheory.Functor.id_obj, CategoryTheory.NatIso.op_inv, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_inv_app, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
⊢ Quiver.Hom.op ((identityToΓSpec.app X).c.app (op ⊤)) ≫ Quiver.Hom.op (toSpecΓ (X.presheaf.obj (op ⊤))) =
    𝟙 (op (X.presheaf.obj (op ⊤)))

Tactic:
congr_arg Quiver.Hom.op (left_triangle X)

Premises used: Quiver.Hom.op, AlgebraicGeometry.ΓSpec.left_triangle, congr_arg
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
⊢ Quiver.Hom.op ((identityToΓSpec.app X).c.app (op ⊤)) ≫ Quiver.Hom.op (toSpecΓ (X.presheaf.obj (op ⊤))) =
    𝟙 (op (X.presheaf.obj (op ⊤)))

Tactic:
exact congr_arg Quiver.Hom.op (left_triangle X)

Premises used: Quiver.Hom.op, AlgebraicGeometry.ΓSpec.left_triangle, congr_arg
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
⊢ identityToΓSpec.app (Spec.locallyRingedSpaceObj (unop R)) ≫ Spec.locallyRingedSpaceMap (toSpecΓ (unop R)) =
    𝟙 (Spec.locallyRingedSpaceObj (unop R))

Tactic:
right_triangle R.unop

Premises used: Set.Mem, Quiver.Hom.unop, AlgebraicGeometry.Spec.locallyRingedSpaceObj, AlgebraicGeometry.toSpecΓ, AlgebraicGeometry.Spec.locallyRingedSpaceMap, AlgebraicGeometry.ΓSpec.right_triangle, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
⊢ identityToΓSpec.app (Spec.locallyRingedSpaceObj (unop R)) ≫ Spec.locallyRingedSpaceMap (toSpecΓ (unop R)) =
    𝟙 (Spec.locallyRingedSpaceObj (unop R))

Tactic:
exact right_triangle R.unop

Premises used: AlgebraicGeometry.ΓSpec.right_triangle, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
⊢ Eq.{u_1 + 1} (α := unop R ⟶ Γ.obj (op (Spec.toLocallyRingedSpace.obj (op (unop R))))) (toSpecΓ (unop R))
    (CommRingCat.ofHom
      (algebraMap (↑R.1 : Type u_1)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (unop R))) : Type u_1)) : Type u_1))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (unop R))) : Type u_1)) : Type u_1)))
            (structureSheafInType (↑(unop (op (unop R))) : Type u_1) (↑(unop (op (unop R))) : Type u_1)))
          (op ⊤))))

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α := CommRingCat.of R ⟶ Γ.obj (op (Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R)))))
    (toSpecΓ (CommRingCat.of R))
    (CommRingCat.ofHom
      (algebraMap R
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u)))
            (structureSheafInType (↑(unop (op (CommRingCat.of R))) : Type u)
              (↑(unop (op (CommRingCat.of R))) : Type u)))
          (op ⊤))))

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceAdjunction.counit.app R =
    Quiver.Hom.op
      (CommRingCat.ofHom
        (algebraMap (↑R.1 : Type u_1)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop R) : Type u_1)) : Type u_1))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop R) : Type u_1)) : Type u_1)))
              (structureSheafInType (↑(unop R) : Type u_1) (↑(unop R) : Type u_1)))
            (op ⊤))))

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, setOf, AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α :=
    (Spec.toLocallyRingedSpace ⋙ Γ.rightOp).obj (op (CommRingCat.of R)) ⟶
      Functor.obj (𝟭 CommRingCatᵒᵖ) (op (CommRingCat.of R)))
    (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R)))
    (Quiver.Hom.op
      (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (op (CommRingCat.of R))) : Type u)
                (↑(unop (op (CommRingCat.of R))) : Type u)))
            (op ⊤)))))

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, setOf, AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α :=
    unop (Functor.obj (𝟭 CommRingCatᵒᵖ) (op (CommRingCat.of R))) ⟶
      unop ((Spec.toLocallyRingedSpace ⋙ Γ.rightOp).obj (op (CommRingCat.of R))))
    (Quiver.Hom.unop (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))))
    (CommRingCat.ofHom
      (algebraMap R
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u)))
            (structureSheafInType (↑(unop (op (CommRingCat.of R))) : Type u)
              (↑(unop (op (CommRingCat.of R))) : Type u)))
          (op ⊤))))

Tactic:
rfl

Premises used: Set.Mem, setOf, Quiver.Hom.unop, AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
R : CommRingCatᵒᵖ
f : Γ.rightOp.obj X ⟶ R
⊢ (locallyRingedSpaceAdjunction.homEquiv X R : (a : Γ.rightOp.obj X ⟶ R) → X ⟶ Spec.toLocallyRingedSpace.obj R) f =
    identityToΓSpec.app X ≫ Spec.locallyRingedSpaceMap f.unop

Tactic:
rfl

Premises used: AlgebraicGeometry.Spec.locallyRingedSpaceObj, AlgebraicGeometry.LocallyRingedSpace.comp, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
R : Type u
inst : CommRing R
f : CommRingCat.of R ⟶ Γ.obj (op X)
⊢ (locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
        (a : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) → X ⟶ Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R)))
      (op f) =
    identityToΓSpec.app X ≫ Spec.locallyRingedSpaceMap f

Tactic:
rfl

Premises used: Quiver.Hom.unop, AlgebraicGeometry.Spec.locallyRingedSpaceObj, AlgebraicGeometry.LocallyRingedSpace.comp, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
R : Type u
inst : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens (↑(↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
dsimp :
  Eq (α :=
    CommRingCat.of R ⟶
      X.presheaf.obj
        (op
          (Functor.obj
            (Opens.map
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            (unop U))))
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            U)) ≫
      NatTrans.app
        (PresheafedSpace.Hom.c
          (Hom.toHom
            ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                  X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
              f)))
        U)
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α :=
    CommRingCat.of R ⟶
      Functor.obj
        (Functor.obj
          (pushforward CommRingCat
            (PresheafedSpace.Hom.base
              (Hom.toHom
                ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                    (a : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) →
                      X ⟶ Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R)))
                  f))))
          X.presheaf)
        U)
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (op (CommRingCat.of R))) : Type u)
                (↑(unop (op (CommRingCat.of R))) : Type u)))
            U)) ≫
      NatTrans.app
        (PresheafedSpace.Hom.c
          (Hom.toHom
            ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                (a : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) →
                  X ⟶ Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R)))
              f)))
        U)
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
dsimp