awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
        (structureSheaf (↑(Γ.obj (op X)) : Type u)))
      (op (basicOpen r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst :
  IsLocalization.Away r
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
            (structureSheaf (↑(Γ.obj (op X)) : Type u)))
          (op (basicOpen r))) :
      Type u)
h :
  Eq (α :=
    (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : Type u))
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f))
    (@RingHom.comp _
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
              (structureSheaf (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen r))) :
        Type u)
      _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r ⋯)
      (algebraMap (↑(Γ.obj (op X)) : Type u)
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheaf (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r))) :
          Type u)))
mp : CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)
⊢ f = X.toΓSpecCApp r

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
        (structureSheaf (↑(Γ.obj (op X)) : Type u)))
      (op (basicOpen r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst :
  IsLocalization.Away r
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
            (structureSheaf (↑(Γ.obj (op X)) : Type u)))
          (op (basicOpen r))) :
      Type u)
h :
  Eq (α :=
    (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : Type u))
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f))
    (@RingHom.comp _
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
              (structureSheaf (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen r))) :
        Type u)
      _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r ⋯)
      (algebraMap (↑(Γ.obj (op X)) : Type u)
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheaf (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r))) :
          Type u)))
⊢ CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)

Tactic:
IsLocalization.ringHom_ext (Submonoid.powers r) h

Premises used: Submonoid.powers, IsLocalization.ringHom_ext
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
        (structureSheaf (↑(Γ.obj (op X)) : Type u)))
      (op (basicOpen r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst :
  IsLocalization.Away r
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
            (structureSheaf (↑(Γ.obj (op X)) : Type u)))
          (op (basicOpen r))) :
      Type u)
h :
  Eq (α :=
    (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : Type u))
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f))
    (@RingHom.comp _
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
              (structureSheaf (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen r))) :
        Type u)
      _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r ⋯)
      (algebraMap (↑(Γ.obj (op X)) : Type u)
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheaf (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r))) :
          Type u)))
⊢ CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)

Tactic:
exact IsLocalization.ringHom_ext (Submonoid.powers r) h

Premises used: Submonoid.powers, IsLocalization.ringHom_ext
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
        (structureSheaf (↑(Γ.obj (op X)) : Type u)))
      (op (basicOpen r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst :
  IsLocalization.Away r
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
            (structureSheaf (↑(Γ.obj (op X)) : Type u)))
          (op (basicOpen r))) :
      Type u)
⊢ f = X.toΓSpecCApp r →
    Eq (α :=
      (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
        (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : Type u))
        (CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)) : Type u)
              (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf
                    (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                  (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
                (op (basicOpen r)))) ≫
          f))
      (@RingHom.comp _
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheaf (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r))) :
          Type u)
        _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r ⋯)
        (algebraMap (↑(Γ.obj (op X)) : Type u)
          (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf
                    (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                  (structureSheaf (↑(Γ.obj (op X)) : Type u)))
                (op (basicOpen r))) :
            Type u)))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)) : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
              (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen r)))) ≫
      X.toΓSpecCApp r =
    X.toToΓSpecMapBasicOpen r

Tactic:
(X.toΓSpecCApp_iff r _).2 rfl

Premises used: Iff.mpr, rfl, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
r s : (InducedCategory (C := (↑(Γ.obj (op X)) : Type u)) (Opens (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ Eq (α := CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s))))
    (CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)) : Type u)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
              (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen (unop s))))) ≫
      X.toΓSpecCApp (unop s))
    (X.toToΓSpecMapBasicOpen (unop s))

Tactic:
X.toΓSpecCApp_spec s.unop

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
r s : (InducedCategory (C := (↑(Γ.obj (op X)) : Type u)) (Opens (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) basicOpen)ᵒᵖ
f : r ⟶ s
e_1 :
  (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s) =
    (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s))))
h :
  Eq (α :=
    CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s)
    (X.toToΓSpecMapBasicOpen (unop s))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        r)
      (X.toToΓSpecMapBasicOpen (unop r))
      (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        f))
⊢ Eq (α :=
    CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        r)
      (X.toToΓSpecMapBasicOpen (unop r))
      (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        f))
    (X.toToΓSpecMapBasicOpen (unop s))

Tactic:
symm
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
r s : (InducedCategory (C := (↑(Γ.obj (op X)) : Type u)) (Opens (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) basicOpen)ᵒᵖ
f : r ⟶ s
e_1 :
  (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s) =
    (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s))))
⊢ Eq (α :=
    CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s)
    (X.toToΓSpecMapBasicOpen (unop s))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        r)
      (X.toToΓSpecMapBasicOpen (unop r))
      (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        f))

Tactic:
apply X.presheaf.map_comp

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen r)) = X.toΓSpecCApp r

Tactic:
apply TopCat.Sheaf.extend_hom_app _ _ _

Premises used: TopCat.Sheaf.extend_hom_app
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ 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 r)))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen r)) =
    X.toToΓSpecMapBasicOpen r

Tactic:
(X.toΓSpecSheafedSpace_app_eq r).symm ▸ X.toΓSpecCApp_spec r

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, Eq.rec, Eq.symm, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
rw :
  Membership.mem (α := (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) (γ :=
    Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) ⊤
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpecSheafedSpace.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
⊢ Membership.mem (α := (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) (γ :=
    Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) (basicOpen 1)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpecSheafedSpace.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))

Tactic:
rw [basicOpen_one]

Premises used: PrimeSpectrum.basicOpen_one
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ Membership.mem (α := (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) (γ :=
    Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) ⊤
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpecSheafedSpace.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))

Tactic:
trivial
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
rw :
  Eq (α := CommRingCat.of (↑(unop (op (Γ.obj (op X)))) : Type u) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y :=
        (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).obj (op (basicOpen 1)))
        (X.toToΓSpecMapBasicOpen 1)
        ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                X.toΓSpecSheafedSpace.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
            x)
          ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
    ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ ⊤
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x)
        True.intro ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
rw₁ : TopCat
rw₂ : (↑X.toPresheafedSpace : TopCat) ⟶ (↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat)
⊢ toStalk (↑(unop (op (Γ.obj (op X)))) : Type u)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x =
    X.presheaf.Γgerm x

Tactic:
rw [PresheafedSpace.Hom.stalkMap,
    ← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
    ← Category.assoc, Category.assoc (CommRingCat.ofHom _), stalkFunctor_map_germ, ← Category.assoc,
    X.toΓSpecSheafedSpace_app_eq, X.toΓSpecCApp_spec, Γgerm,
    ← dsimp% stalkPushforward_germ _ _ X.presheaf ⊤]

Premises used: CategoryTheory.Category.assoc, PrimeSpectrum.basicOpen, AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, CommRingCat.ofHom, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.stalkPushforward_germ, TopCat.Presheaf.Γgerm, AlgebraicGeometry.StructureSheaf.algebraMap_germ, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Top.top, TopCat.Presheaf.stalkFunctor_map_germ, OfNat.ofNat, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec