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)
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
i : I
obtain :
  ∀ (U : TopologicalSpace.Opens ↥(D.obj i))
    (hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U)
    (hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((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))
⊢ ∃ (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 ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (c.π.app i x)) isOpen_univ

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
obtain :
  ∀ (r : (↑Γ(c.pt, ⊤) : Type u)) (hr : IsAffineOpen (c.pt.basicOpen r)) (hxr : x ∈ (↑(c.pt.basicOpen r) : Set ↥c.pt))
    (hrU : (↑(c.pt.basicOpen r) : Set ↥c.pt) ⊆ (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).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))
⊢ ∃ (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 ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, hrU⟩ :=
      (IsQuasiAffine.isBasis_basicOpen c.pt).exists_subset_of_mem_open hxU (c.π.app i ⁻¹ᵁ U).isOpen

Premises used: CategoryTheory.Limits.Cone.π, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Limits.Cone.pt, TopologicalSpace.Opens.isOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
r : (↑Γ(c.pt, ⊤) : Type u)
hr : IsAffineOpen (c.pt.basicOpen r)
hxr : x ∈ (↑(c.pt.basicOpen r) : Set ↥c.pt)
hrU : (↑(c.pt.basicOpen r) : Set ↥c.pt) ⊆ (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
obtain :
  ∀ (j : I) (r : (↑Γ(D.obj j, ⊤) : Type u))
    (hr :
      IsAffineOpen.{u} (X := c.pt)
        (c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)))
    (hxr :
      x ∈
        (↑(c.pt.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
                  (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
                r)) :
          Set ↥c.pt))
    (hrU :
      (↑(c.pt.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
                  (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
                r)) :
          Set ↥c.pt) ⊆
        (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).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))
⊢ ∃ (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 ⟨j, r, rfl⟩ := exists_appTop_π_eq_of_isLimit D c hc r

Premises used: AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, 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)
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
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
obtain :
  ∀ (k : I) (fki : k ⟶ i) (fkj : k ⟶ j),
    ∃ (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 ⟨k, fki, fkj, -⟩ := IsCofilteredOrEmpty.cone_objs i j

Premises used: CategoryTheory.IsCofilteredOrEmpty.cone_objs
-- 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
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
rwa : c.π.app k ⁻¹ᵁ D.map fkj ⁻¹ᵁ (D.obj j).basicOpen r ≤ c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ U
rwa₁ : (c.π.app k ≫ D.map fkj) ⁻¹ᵁ (D.obj j).basicOpen r ≤ c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ U
rwa₂ : (c.π.app k ≫ D.map fkj) ⁻¹ᵁ (D.obj j).basicOpen r ≤ (c.π.app k ≫ D.map fki) ⁻¹ᵁ U
rwa₃ : c.π.app j ⁻¹ᵁ (D.obj j).basicOpen r ≤ (c.π.app k ≫ D.map fki) ⁻¹ᵁ U
rwa₄ : c.π.app j ⁻¹ᵁ (D.obj j).basicOpen r ≤ c.π.app i ⁻¹ᵁ U
rwa₅ rwa₆ rwa₇ rwa₈ :
  (Functor.obj (Functor.obj (Functor.const I) c.pt) k).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj k, ⊤) : Type u))
        r) ≤
    c.π.app i ⁻¹ᵁ U
⊢ c.π.app k ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ U

Tactic:
rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Limits.Cone.w
-- 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
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
obtain :
  ∀ (l : I) (flk : l ⟶ k)
    (hl :
      D.map flk ⁻¹ᵁ
          (D.obj k).basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
                (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
              r) ≤
        D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U),
    ∃ (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 ⟨l, flk, hl⟩ := exists_map_preimage_le_map_preimage D c hc (isCompact_basicOpen _
      isCompact_univ ((D.map fkj).appTop r)) (V := D.map fki ⁻¹ᵁ U) (by
        rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top])

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.appTop, CategoryTheory.Functor.map, AlgebraicGeometry.exists_map_preimage_le_map_preimage, DFunLike.coe, AlgebraicGeometry.isCompact_basicOpen
-- 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
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ ∃ (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:
⟨l, (D.map (flk ≫ fkj)).appTop r, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.appTop, CategoryTheory.Functor.map, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, DFunLike.coe
-- 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
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
refine_1 :
  IsAffineOpen.{u} (X := D.obj l)
    ((D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r))
refine_2 :
  Membership.mem (α := ↥(D.obj l)) (γ := (D.obj l).Opens)
    ((D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r))
    ((c.π.app l) x : ↥(D.obj l))
⊢ ∃ (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:
refine ⟨l, (D.map (flk ≫ fkj)).appTop r, ?_, ?_⟩
-- 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),
    ∃ (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:
have (x : c.pt) : ∃ (i : I) (f : Γ(D.obj i, ⊤)),
      IsAffineOpen (Scheme.basicOpen _ f) ∧ c.π.app i x ∈ (Scheme.basicOpen _ f) := by
    obtain ⟨i⟩ := IsCofiltered.nonempty (C := I)
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (c.π.app i x)) isOpen_univ
    obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, hrU⟩ :=
      (IsQuasiAffine.isBasis_basicOpen c.pt).exists_subset_of_mem_open hxU (c.π.app i ⁻¹ᵁ U).isOpen
    obtain ⟨j, r, rfl⟩ := exists_appTop_π_eq_of_isLimit D c hc r
    obtain ⟨k, fki, fkj, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    obtain ⟨l, flk, hl⟩ := exists_map_preimage_le_map_preimage D c hc (isCompact_basicOpen _
      isCompact_univ ((D.map fkj).appTop r)) (V := D.map fki ⁻¹ᵁ U) (by
        rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top])
    refine ⟨l, (D.map (flk ≫ fkj)).appTop r, ?_, ?_⟩
    · convert!
      (hU.preimage (D.map (flk ≫ fki))).basicOpen
        ((D.obj _).presheaf.map (homOfLE le_top).op ((D.map (flk ≫ fkj)).appTop r)) using 1
      rwa [Scheme.basicOpen_res, eq_comm, inf_eq_right, Functor.map_comp,
        elementwise_of% Scheme.Hom.comp_appTop, ← Scheme.preimage_basicOpen_top, Functor.map_comp,
        Scheme.Hom.comp_preimage]
    · change x ∈ c.π.app l ⁻¹ᵁ (D.obj l).basicOpen _
      rwa [Scheme.preimage_basicOpen_top, ← elementwise_of% Scheme.Hom.comp_appTop, Cone.w]
-- 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
this :
  ∀ (x : ↥c.pt),
    ∃ (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))
choose :
  ∀ (i : (x : ↥c.pt) → I) (f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u))
    (hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x)))
    (hi :
      ∀ (x : ↥c.pt),
        Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))),
    ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
choose i f hf hi using this
-- 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
i : (x : ↥c.pt) → I
f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi :
  ∀ (x : ↥c.pt),
    Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))
x : ↥c.pt
⊢ x ∈ (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier

Tactic:
hi x

Premises used: Set.Mem, setOf, Set.preimage