awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
t : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)
hj :
  Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensCone D c i U).π.app j)) :
          (a : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
        t :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))))
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1 :
  (↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u) =
    (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u)
⊢ Scheme.Hom.app (c.π.app j.left) ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) =
    Scheme.Hom.appTop ((opensCone D c i U).π.app j) ≫ c.pt.presheaf.map (homOfLE H).op

Tactic:
simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.resLE_appLE
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
t : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)
hj :
  Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensCone D c i U).π.app j)) :
          (a : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
        t :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))))
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1 :
  (↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u) =
    (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u)
⊢ Eq (α := (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤)) (Y :=
            c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
            (c.pt.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
        s :
      (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤))
            (c.pt.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ (homOfLE H).op)) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
        s :
      (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
⊢ ∀ (x : ↥c.pt),
    ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
      Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
      Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
            t :
          (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) ⋯ :
          ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))

Tactic:
have (x : c.pt) : ∃ (i : I) (U : (D.obj i).Opens) (hU : IsAffineOpen U)
      (hU : (c.π.app i).base x ∈ U) (t : Γ(D.obj i, U)), (c.π.app i).app U t = s |_ _ := by
    have i := IsCofiltered.nonempty (C := I).some
    obtain ⟨_, ⟨U, hU : IsAffineOpen U, rfl⟩, hxU, -⟩ :=
      (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open
        (Set.mem_univ ((c.π.app i).base x)) isOpen_univ
    have (j : Over i) : IsAffine ((opensDiagram D i U).obj j) := hU.preimage (D.map _)
    obtain ⟨j, t, hj⟩ := exists_appTop_π_eq_of_isAffine_of_isLimit _ _
      (isLimitOpensCone D c hc i U) (s |_ _)
    refine ⟨j.left, (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤, by simpa using hU.preimage (D.map _), ?_, t, ?_⟩
    · suffices (c.π.app j.1 ≫ D.map j.hom).base x ∈ U by simpa [-Cone.w] using this
      rwa [Cone.w]
    · have H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤ := by
        simp [← Scheme.Hom.comp_preimage]
      convert! congr(c.pt.presheaf.map (homOfLE H).op $hj)
      · convert! ConcreteCategory.comp_apply _ _ _
        congr
        simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
      · dsimp [TopCat.Presheaf.restrictOpen, TopCat.Presheaf.restrict]
        change _ = (c.pt.presheaf.map (homOfLE _).op ≫ c.pt.presheaf.map (homOfLE _).op) s
        rw [← Functor.map_comp]
        rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
i : (x : ↥c.pt) → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), Membership.mem (α := ↥(D.obj (i x))) (U x) ((c.π.app (i x)) x : ↥(D.obj (i x)))
t : (x : ↥c.pt) → (↑Γ(D.obj (i x), U x) : Type u)
ht :
  ∀ (x : ↥c.pt),
    Eq (α := (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x)) (Scheme.Hom.app (c.π.app (i x)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
          (t x) :
        (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app (i x) ⁻¹ᵁ U x) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app (i x) ⁻¹ᵁ U x))))
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ Eq (α := (↑Γ(c.pt, c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤)) (Y :=
            Γ(c.pt, c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
            (c.pt.presheaf.map
              (CategoryStruct.comp (Y := Opposite.op (c.π.app (i x) ⁻¹ᵁ U x)) (Quiver.Hom.op (homOfLE ⋯))
                (Quiver.Hom.op (homOfLE ⋯)))) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑Γ(c.pt, c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u))
        s :
      (↑Γ(c.pt, c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤)) (Y :=
            Γ(c.pt, c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
            (c.pt.presheaf.map
              (CategoryStruct.comp (Y := Opposite.op (c.π.app (i y) ⁻¹ᵁ U y)) (Quiver.Hom.op (homOfLE ⋯))
                (Quiver.Hom.op (homOfLE ⋯)))) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑Γ(c.pt, c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u))
        s :
      (↑Γ(c.pt, c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
i : (x : ↥c.pt) → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), Membership.mem (α := ↥(D.obj (i x))) (U x) ((c.π.app (i x)) x : ↥(D.obj (i x)))
t : (x : ↥c.pt) → (↑Γ(D.obj (i x), U x) : Type u)
ht :
  ∀ (x : ↥c.pt),
    Eq (α := (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x)) (Scheme.Hom.app (c.π.app (i x)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
          (t x) :
        (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app (i x) ⁻¹ᵁ U x) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app (i x) ⁻¹ᵁ U x))))
j : (x y : ↥c.pt) → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    Eq (α :=
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        ((D.obj (j x y)).presheaf.obj (Opposite.op (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj (i x), U x)) (Scheme.Hom.app (D.map (fjx x y)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(D.obj (j x y), D.map (fjx x y) ⁻¹ᵁ U x) : Type u))
          (t x))
        (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y) ⋯)
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj (i y), U y)) (Scheme.Hom.app (D.map (fjy x y)) (U y)) :
            (a : (↑Γ(D.obj (i y), U y) : Type u)) → (↑Γ(D.obj (j x y), D.map (fjy x y) ⁻¹ᵁ U y) : Type u))
          (t y))
        (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y) ⋯)
x : ↥c.pt
⊢ x ∈ (c.π.app (i x) ⁻¹ᵁ U x).carrier

Tactic:
hxU x

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
i : (x : ↥c.pt) → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), Membership.mem (α := ↥(D.obj (i x))) (U x) ((c.π.app (i x)) x : ↥(D.obj (i x)))
t : (x : ↥c.pt) → (↑Γ(D.obj (i x), U x) : Type u)
ht :
  ∀ (x : ↥c.pt),
    Eq (α := (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x)) (Scheme.Hom.app (c.π.app (i x)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
          (t x) :
        (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app (i x) ⁻¹ᵁ U x) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app (i x) ⁻¹ᵁ U x))))
j : (x y : ↥c.pt) → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    Eq (α :=
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        ((D.obj (j x y)).presheaf.obj (Opposite.op (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj (i x), U x)) (Scheme.Hom.app (D.map (fjx x y)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(D.obj (j x y), D.map (fjx x y) ⁻¹ᵁ U x) : Type u))
          (t x))
        (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y) ⋯)
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj (i y), U y)) (Scheme.Hom.app (D.map (fjy x y)) (U y)) :
            (a : (↑Γ(D.obj (i y), U y) : Type u)) → (↑Γ(D.obj (j x y), D.map (fjy x y) ⁻¹ᵁ U y) : Type u))
          (t y))
        (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y) ⋯)
x : ↥c.pt
⊢ x ∈ (c.π.app (i x) ⁻¹ᵁ U x).carrier

Tactic:
exact hxU x
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
⊢ ReflectsFilteredColimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))

Tactic:
have : ReflectsFilteredColimits (forget CommRingCat) :=
    ⟨fun _ ↦ reflectsColimitsOfShape_of_reflectsIsomorphisms⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this :
  ReflectsFilteredColimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
⊢ Nonempty.{u + 2} (IsColimit (Scheme.Γ.mapCocone c.op))

Tactic:
ReflectsColimit.reflects (F := forget _) (Types.FilteredColimit.isColimitOf' _ _ ?_ ?_)

Premises used: CategoryTheory.Limits.ReflectsColimit.reflects, CategoryTheory.Limits.Types.FilteredColimit.isColimitOf'
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this :
  ReflectsFilteredColimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
⊢ ∀
    (x :
      Cocone.pt (F :=
        (D.op ⋙ Scheme.Γ) ⋙
          forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
        (Functor.mapCocone
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Scheme.Γ.mapCocone c.op))),
    ∃ (i : Iᵒᵖ) (xi :
      (fun (X : Type u) ↦ X)
        (((D.op ⋙ Scheme.Γ) ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
          i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op)))
                i) :
            (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
          xi

Tactic:
fun s ↦ ⟨.op _, (exists_appTop_π_eq_of_isLimit D c hc s).choose_spec⟩

Premises used: CategoryTheory.Limits.Cone.π, Exists.choose_spec, Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, Exists, AlgebraicGeometry.Scheme.Hom.appTop, Opposite.op, Exists.intro, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, Subtype.val, Eq, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this :
  ReflectsFilteredColimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
⊢ ∀
    (x :
      Cocone.pt (F :=
        (D.op ⋙ Scheme.Γ) ⋙
          forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
        (Functor.mapCocone
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Scheme.Γ.mapCocone c.op))),
    ∃ (i : Iᵒᵖ) (xi :
      (fun (X : Type u) ↦ X)
        (((D.op ⋙ Scheme.Γ) ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
          i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op)))
                i) :
            (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
          xi

Tactic:
exact fun s ↦ ⟨.op _, (exists_appTop_π_eq_of_isLimit D c hc s).choose_spec⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
⊢ PreservesLimit D Scheme.Γ.rightOp

Tactic:
have : PreservesColimit D.op Scheme.Γ := ⟨fun hc ↦ nonempty_isColimit_Γ_mapCocone D _ hc.unop⟩
  preservesLimit_rightOp _ _

Premises used: AlgebraicGeometry.Scheme.Γ, CategoryTheory.Limits.Cocone.unop, CategoryTheory.Limits.PreservesColimit.mk, CategoryTheory.Limits.IsColimit.unop, AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone, CategoryTheory.Limits.preservesLimit_rightOp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
inst_5 : IsQuasiAffine.{u} c.pt
x : ↥c.pt
obtain :
  ∀ (i : I),
    ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
      IsAffineOpen ((D.obj i).basicOpen f) ∧
        Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))
⊢ ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
    IsAffineOpen ((D.obj i).basicOpen f) ∧
      Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))

Tactic:
obtain ⟨i⟩ := IsCofiltered.nonempty (C := I)

Premises used: CategoryTheory.IsCofiltered.nonempty