awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
U : X.AffineZariskiSite
r : (↑Γ(X, (↑U : X.Opens)) : Type u)
this_1 :
  IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
            (α.app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(F.obj (Opposite.op U)) : Type u))
        r :
      (↑(F.obj (Opposite.op U)) : Type u))
    (↑(F.obj (Opposite.op (U.basicOpen r))) : Type u)
this : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen r))) : Type u) :=
  (CommRingCat.Hom.hom (F.map (homOfLE ⋯).op)).toAlgebra
⊢ (↑(Hom.opensRange ((relativeGluingData H).functor.map (homOfLE ⋯))) : Set ↥((relativeGluingData H).functor.obj U)) =
    (↑(PrimeSpectrum.basicOpen
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                  (α.app (Opposite.op U)) :
                (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                  (↑(F.obj (Opposite.op U)) : Type u))
              r) :
          TopologicalSpace.Opens (PrimeSpectrum (↑(F.obj (Opposite.op U)) : Type u))) :
      Set ↥((relativeGluingData H).functor.obj U))

Tactic:
refine PrimeSpectrum.localization_away_comap_range (F.obj (.op <| U.basicOpen r))
    (α.app (.op U) r)

Premises used: CommRingCat.carrier, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, Opposite.op, DFunLike.coe, PrimeSpectrum.localization_away_comap_range, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
U : X.AffineZariskiSite
⊢ Eq (α := (relativeGluingData H).glued.Opens) ((relativeGluingData H).toBase ⁻¹ᵁ (↑U : X.Opens))
    (Hom.opensRange (X :=
      PreZeroHypercover.X (S := (relativeGluingData H).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (relativeGluingData H).cover) U)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (relativeGluingData H).cover) U))

Tactic:
simpa using (relativeGluingData H).toBase_preimage_eq_opensRange_ι U

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
⊢ IsIso (X := (colimit.cocone F).pt) (Y := (cocone X).pt) (IsColimit.desc (colimit.isColimit F) (cocone X))

Tactic:
(IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms _)
      (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X))).mpr fun U ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
refine :
  ∀ (U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1),
    MorphismProperty.isomorphisms Scheme (X :=
      PreZeroHypercover.X (S := (colimit.cocone F).pt)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
          (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
            (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)))
        U)
      (Cover.pullbackHom (P := IsOpenImmersion)
          (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
          (IsColimit.desc (colimit.isColimit F) (cocone X)) U :
        PreZeroHypercover.X (S := (colimit.cocone F).pt)
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
                (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)))
            U ⟶
          (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).X U)
⊢ IsIso (X := (colimit.cocone F).pt) (Y := (cocone X).pt) (IsColimit.desc (colimit.isColimit F) (cocone X))

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms _)
      (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X))).mpr fun U ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
change :
  IsIso (X := pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
    (pullback.snd (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
⊢ MorphismProperty.isomorphisms Scheme (X :=
    PreZeroHypercover.X (S := (colimit.cocone F).pt)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
        (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
          (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)))
      U)
    (Cover.pullbackHom (P := IsOpenImmersion)
        (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
        (IsColimit.desc (colimit.isColimit F) (cocone X)) U :
      PreZeroHypercover.X (S := (colimit.cocone F).pt)
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
            (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
              (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)))
          U ⟶
        (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).X U)

Tactic:
change IsIso (pullback.snd (colimit.desc F (cocone X)) U.1.ι)

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.cocone, CategoryTheory.IsIso, CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.colimit.desc, AlgebraicGeometry.Scheme.Opens.ι, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
rw :
  (↑(colimit.desc F (cocone X) ⁻¹ᵁ (↑U : X.Opens)) : Set ↥(colimit F)) =
    (↑(Hom.opensRange (colimit.ι F U)) : Set ↥(colimit F))
⊢ Eq (α := Set ↥(colimit F))
    (Set.range (ι := ↥(pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι))
      ⇑(pullback.fst (colimit.desc F (cocone X)) (↑U : X.Opens).ι))
    (Set.range (ι := ↥(↑(↑U : X.Opens) : Scheme)) ⇑((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U))

Tactic:
rw [Pullback.range_fst, Opens.range_ι, ← Hom.coe_opensRange, Hom.opensRange_comp_of_isIso,
        ← Scheme.Hom.coe_preimage]

Premises used: AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.Scheme.Hom.opensRange_comp_of_isIso, AlgebraicGeometry.Scheme.Hom.coe_opensRange
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
⊢ Eq (α := Set ↥D.glued) (TopologicalSpace.Opens.carrier (D.toBase ⁻¹ᵁ Hom.opensRange ((directedCover X).f U)))
    (TopologicalSpace.Opens.carrier (Hom.opensRange (colimit.ι D.functor U)))

Tactic:
congr($(D.toBase_preimage_eq_opensRange_ι U).1)

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, congrArg, id, TopologicalSpace.Opens.carrier
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
h :
  (cocone X).pt.Opens = X.Opens →
    HEq.{u + 2} (α := Category.{u, u} (cocone X).pt.Opens)
        (Preorder.smallCategory (TopologicalSpace.Opens ↥(cocone X).pt)) (β := Category.{u, u} X.Opens)
        (Preorder.smallCategory (TopologicalSpace.Opens ↥X)) →
      (↑(cocone X).pt.toPresheafedSpace : TopCat) = (↑X.toPresheafedSpace : TopCat) →
        (cocone X).pt.toPresheafedSpace = X.toPresheafedSpace →
          (cocone X).pt.toLocallyRingedSpace = X.toLocallyRingedSpace →
            (cocone X).pt = X → Eq (α := (colimit F).Hom (cocone X).pt) (colimit.desc F (cocone X)) D.toBase
h₁ : (cocone X).pt.Opens = X.Opens → (↑U : X.Opens) = Hom.opensRange ((directedCover X).f U)
⊢ (↑(colimit.desc F (cocone X) ⁻¹ᵁ (↑U : X.Opens)) : Set ↥(colimit F)) =
    (↑(Hom.opensRange (colimit.ι F U)) : Set ↥(colimit F))

Tactic:
convert! congr($(D.toBase_preimage_eq_opensRange_ι U).1)
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e_1 : (cocone X).pt.Opens = X.Opens
e_2 :
  HEq.{u + 2} (α := Category.{u, u} (cocone X).pt.Opens)
    (Preorder.smallCategory (TopologicalSpace.Opens ↥(cocone X).pt)) (β := Category.{u, u} X.Opens)
    (Preorder.smallCategory (TopologicalSpace.Opens ↥X))
e_2_1 : (↑(cocone X).pt.toPresheafedSpace : TopCat) = (↑X.toPresheafedSpace : TopCat)
e_4 : (cocone X).pt.toPresheafedSpace = X.toPresheafedSpace
e_2_2 : (cocone X).pt.toLocallyRingedSpace = X.toLocallyRingedSpace
e_2_3 : (cocone X).pt = X
h :
  Eq (α :=
    (colimit F).Hom
      (Cocone.pt (J := (directedCover X).I₀) (F := F)
        { pt := X, ι := { app := fun (U : X.AffineZariskiSite) ↦ ⋯.fromSpec, naturality := ⋯ } }))
    (colimit.desc F { pt := X, ι := { app := fun (U : X.AffineZariskiSite) ↦ ⋯.fromSpec, naturality := ⋯ } }) D.toBase
⊢ Eq (α := (colimit F).Hom (cocone X).pt) (colimit.desc F (cocone X)) D.toBase

Tactic:
delta cocone

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.cocone
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e_1 : (cocone X).pt.Opens = X.Opens
e_2 :
  HEq.{u + 2} (α := Category.{u, u} (cocone X).pt.Opens)
    (Preorder.smallCategory (TopologicalSpace.Opens ↥(cocone X).pt)) (β := Category.{u, u} X.Opens)
    (Preorder.smallCategory (TopologicalSpace.Opens ↥X))
e_2_1 : (↑(cocone X).pt.toPresheafedSpace : TopCat) = (↑X.toPresheafedSpace : TopCat)
e_4 : (cocone X).pt.toPresheafedSpace = X.toPresheafedSpace
e_2_2 : (cocone X).pt.toLocallyRingedSpace = X.toLocallyRingedSpace
e_2_3 : (cocone X).pt = X
h :
  ∀ (U : X.AffineZariskiSite),
    ⋯.fromSpec =
      D.natTrans.app U ≫ NatTrans.app (Cover.functorOfLocallyDirectedHomBase (P := IsOpenImmersion) (directedCover X)) U
⊢ Eq (α :=
    (colimit F).Hom
      (Cocone.pt (J := (directedCover X).I₀) (F := F)
        { pt := X, ι := { app := fun (U : X.AffineZariskiSite) ↦ ⋯.fromSpec, naturality := ⋯ } }))
    (colimit.desc F { pt := X, ι := { app := fun (U : X.AffineZariskiSite) ↦ ⋯.fromSpec, naturality := ⋯ } }) D.toBase

Tactic:
congr with U
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U_1 : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e_1 : (cocone X).pt.Opens = X.Opens
e_2 :
  HEq.{u + 2} (α := Category.{u, u} (cocone X).pt.Opens)
    (Preorder.smallCategory (TopologicalSpace.Opens ↥(cocone X).pt)) (β := Category.{u, u} X.Opens)
    (Preorder.smallCategory (TopologicalSpace.Opens ↥X))
e_2_1 : (↑(cocone X).pt.toPresheafedSpace : TopCat) = (↑X.toPresheafedSpace : TopCat)
e_4 : (cocone X).pt.toPresheafedSpace = X.toPresheafedSpace
e_2_2 : (cocone X).pt.toLocallyRingedSpace = X.toLocallyRingedSpace
e_2_3 : (cocone X).pt = X
U : X.AffineZariskiSite
⊢ ⋯.fromSpec =
    D.natTrans.app U ≫ NatTrans.app (Cover.functorOfLocallyDirectedHomBase (P := IsOpenImmersion) (directedCover X)) U

Tactic:
simp [D, relativeGluingData, restrictIsoSpec]

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e_1 : (cocone X).pt.Opens = X.Opens
⊢ (↑U : X.Opens) = Hom.opensRange ((directedCover X).f U)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e : pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι ≅ (↑(↑U : X.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
⊢ IsIso e.hom

Tactic:
(inferInstance : IsIso e.hom)

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e : pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι ≅ (↑(↑U : X.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
h : pullback.snd (colimit.desc F (cocone X)) (↑U : X.Opens).ι = e.hom
⊢ IsIso (X := pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
    (pullback.snd (colimit.desc F (cocone X)) (↑U : X.Opens).ι)

Tactic:
convert! (inferInstance : IsIso e.hom)

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e : pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι ≅ (↑(↑U : X.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
h : e.inv ≫ pullback.snd (colimit.desc F (cocone X)) (↑U : X.Opens).ι ≫ (↑U : X.Opens).ι = (↑U : X.Opens).ι
⊢ pullback.snd (colimit.desc F (cocone X)) (↑U : X.Opens).ι = e.hom

Tactic:
rw [← cancel_mono U.1.ι, ← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
e : pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι ≅ (↑(↑U : X.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
⊢ e.inv ≫ pullback.snd (colimit.desc F (cocone X)) (↑U : X.Opens).ι ≫ (↑U : X.Opens).ι = (↑U : X.Opens).ι

Tactic:
simp [e, ← pullback.condition, IsAffineOpen.isoSpec_hom]

Premises used: CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ ToType (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier) (topObj R) =
    PrimeSpectrum (↑R : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ topMap (𝟙 R) = 𝟙 (topObj R)

Tactic:
rfl

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, setOf, AlgebraicGeometry.Spec.topMap, ContinuousMap.id, Set.preimage, Ideal.comap, PrimeSpectrum.comap, rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ topMap (f ≫ g) = topMap g ≫ topMap f

Tactic:
rfl

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, setOf, ContinuousMap.comp, AlgebraicGeometry.Spec.topMap, Set.preimage, Ideal.comap, PrimeSpectrum.comap, rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
x x_1 : (TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
x_2 : x ⟶ x_1
hf :
  ∀ (x_3 : (↑((sheafedSpaceObj R).presheaf.obj x) : Type u)),
    Eq (α :=
      (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).obj x_1) :
        Type u))
      ((CommRingCat.Hom.hom
              ((sheafedSpaceObj R).presheaf.map x_2 ≫
                CommRingCat.ofHom
                  (comap (CommRingCat.Hom.hom f) (unop x_1) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x_1))
                    ⋯)) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj x) : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat (topMap f)).obj (sheafedSpaceObj S).presheaf).obj x_1) :
                Type u))
          x_3 :
        (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).obj x_1) :
          Type u))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                  (comap (CommRingCat.Hom.hom f) (unop x) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x)) ⋯) ≫
                (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).map
                  x_2) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj x) : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat (topMap f)).obj (sheafedSpaceObj S).presheaf).obj x_1) :
                Type u))
          x_3 :
        (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).obj x_1) :
          Type u))
⊢ (sheafedSpaceObj R).presheaf.map x_2 ≫
      CommRingCat.ofHom
        (comap (CommRingCat.Hom.hom f) (unop x_1) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x_1)) ⋯) =
    CommRingCat.ofHom
        (comap (CommRingCat.Hom.hom f) (unop x) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x)) ⋯) ≫
      (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).map x_2

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
x x_1 : (TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
x_2 : x ⟶ x_1
x_3 : (↑((sheafedSpaceObj R).presheaf.obj x) : Type u)
⊢ Eq (α :=
    (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).obj x_1) :
      Type u))
    ((CommRingCat.Hom.hom
            ((sheafedSpaceObj R).presheaf.map x_2 ≫
              CommRingCat.ofHom
                (comap (CommRingCat.Hom.hom f) (unop x_1) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x_1)) ⋯)) :
          (a : (↑((sheafedSpaceObj R).presheaf.obj x) : Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat (topMap f)).obj (sheafedSpaceObj S).presheaf).obj x_1) :
              Type u))
        x_3 :
      (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).obj x_1) :
        Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
                (comap (CommRingCat.Hom.hom f) (unop x) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x)) ⋯) ≫
              (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).map x_2) :
          (a : (↑((sheafedSpaceObj R).presheaf.obj x) : Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat (topMap f)).obj (sheafedSpaceObj S).presheaf).obj x_1) :
              Type u))
        x_3 :
      (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (topMap f)) (sheafedSpaceObj S).presheaf).obj x_1) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
w : (sheafedSpaceMap (𝟙 R)).hom.base = (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base
h :
  (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).c
⊢ sheafedSpaceMap (𝟙 R) = 𝟙 (sheafedSpaceObj R)

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.base = (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base

Tactic:
Spec.topMap_id R

Premises used: AlgebraicGeometry.Spec.topObj, AlgebraicGeometry.Spec.topMap_id, AlgebraicGeometry.Spec.topMap
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.base = (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base

Tactic:
exact Spec.topMap_id R

Premises used: AlgebraicGeometry.Spec.topMap_id