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
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:
exact hi 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)
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)))
obtain :
  ∀ (σ : Finset ↥c.pt)
    (hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤),
    ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
obtain ⟨σ, hσ⟩ := CompactSpace.elim_nhds_subcover
    (fun x ↦ (((c.π.app (i x)) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).1))
    (fun x ↦ ((c.π.app (i x)) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).2.mem_nhds (by exact hi x))

Premises used: CategoryTheory.Limits.Cone.π, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.carrier, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CompactSpace.elim_nhds_subcover, CategoryTheory.Functor.obj, 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)
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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
choose :
  ∀ (σi : (x : ↥c.pt) → ↥c.pt) (hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ)
    (hσi :
      ∀ (x : ↥c.pt),
        Membership.mem (γ := Set ↥c.pt)
          (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
            Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
          x),
    ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
choose σi hσiσ hσi using fun x ↦ Set.mem_iUnion₂.mp (hσ.ge (Set.mem_univ x))

Premises used: Eq.ge, Set.mem_iUnion₂, Iff.mp, Set.mem_univ
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
obtain :
  ∀ (j : I) (fj : ∀ {X : I}, X ∈ Finset.image i σ → Nonempty.{u + 1} (j ⟶ X)), ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
obtain ⟨j, fj⟩ := IsCofiltered.inf_objs_exists (σ.image i)

Premises used: CategoryTheory.IsCofiltered.inf_objs_exists, Finset.image
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : ∀ {X : I}, X ∈ Finset.image i σ → Nonempty.{u + 1} (j ⟶ X)
replace : ∀ (fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1), ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
replace fj := fun i h ↦ (@fj i h).some
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
refine :
  ∀ (x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)),
    Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)) ⊤ x →
      Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi x)) ⋯) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x)))
        ((c.π.app j) x : ↥(D.obj j))
⊢ c.π.app j ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤

Tactic:
refine top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, ?_⟩

Premises used: top_le_iff, Iff.mp
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)
h : Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)) ⊤ x
change :
  Membership.mem (α := ↥(D.obj (i (σi x)))) (γ := (D.obj (i (σi x))).Opens) ((D.obj (i (σi x))).basicOpen (f (σi x)))
    ((c.π.app j ≫ D.map (fj (i (σi x)) ⋯)) x : ↥(D.obj (i (σi x))))
⊢ Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi x)) ⋯) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x)))
    ((c.π.app j) x : ↥(D.obj j))

Tactic:
change (c.π.app j ≫ D.map _).base x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.Scheme.basicOpen, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.Functor.obj, 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)
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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)
h : Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)) ⊤ x
rw :
  Membership.mem (α := ↥(D.obj (i (σi x)))) (γ := (D.obj (i (σi x))).Opens) ((D.obj (i (σi x))).basicOpen (f (σi x)))
    ((c.π.app (i (σi x))) x : ↥(D.obj (i (σi x))))
⊢ Membership.mem (α := ↥(D.obj (i (σi x)))) (γ := (D.obj (i (σi x))).Opens) ((D.obj (i (σi x))).basicOpen (f (σi x)))
    ((c.π.app j ≫ D.map (fj (i (σi x)) ⋯)) x : ↥(D.obj (i (σi x))))

Tactic:
rw [Cone.w]

Premises used: 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
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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)
h : Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)) ⊤ x
⊢ Membership.mem (α := ↥(D.obj (i (σi x)))) (γ := (D.obj (i (σi x))).Opens) ((D.obj (i (σi x))).basicOpen (f (σi x)))
    ((c.π.app (i (σi x))) x : ↥(D.obj (i (σi x))))

Tactic:
hσi _

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)
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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)
h : Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)) ⊤ x
⊢ Membership.mem (α := ↥(D.obj (i (σi x)))) (γ := (D.obj (i (σi x))).Opens) ((D.obj (i (σi x))).basicOpen (f (σi x)))
    ((c.π.app (i (σi x))) x : ↥(D.obj (i (σi x))))

Tactic:
exact hσi _
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
obtain :
  ∀ (k : I) (fkj : k ⟶ j)
    (hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤),
    ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
obtain ⟨k, fkj, hk⟩ := exists_map_eq_top D c hc
    (⨆ k, D.map (fj _ (Finset.mem_image_of_mem i (hσiσ k))) ⁻¹ᵁ (D.obj (i _)).basicOpen (f _)) (by
      refine top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, ?_⟩
      change (c.π.app j ≫ D.map _).base x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))
      rw [Cone.w]
      exact hσi _)

Premises used: iSup, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.exists_map_eq_top, Finset.mem_image_of_mem, CategoryTheory.Functor.obj
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
⟨k, .of_forall_exists_mem_basicOpen _ fun x ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpen, Exists.intro
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
refine :
  ∀ (x : ↥(D.obj k)),
    ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)

Tactic:
refine ⟨k, .of_forall_exists_mem_basicOpen _ fun 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)
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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
obtain :
  ∀ (y : ↥c.pt)
    (hy :
      Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y)))
        ((D.map fkj) x : ↥(D.obj j))),
    ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r
⊢ ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r

Tactic:
obtain ⟨y, hy⟩ := TopologicalSpace.Opens.mem_iSup.mp (hk.ge (Set.mem_univ x))

Premises used: Eq.ge, TopologicalSpace.Opens.mem_iSup, Iff.mp, Set.mem_univ
-- 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)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
y : ↥c.pt
hy :
  Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y)))
    ((D.map fkj) x : ↥(D.obj j))
h :
  IsAffineOpen.{u} (X := D.obj 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))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop (D.map (fj (i (σi y)) ⋯))) :
                (a : (↑Γ(D.obj (i (σi y)), ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
              (f (σi y)) :
            (↑Γ(D.obj j, ⊤) : Type u)))) ∧
    Membership.mem (γ := (D.obj k).Opens)
      ((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))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop (D.map (fj (i (σi y)) ⋯))) :
                (a : (↑Γ(D.obj (i (σi y)), ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
              (f (σi y)) :
            (↑Γ(D.obj j, ⊤) : Type u))))
      x
⊢ ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r

Tactic:
use (D.map fkj).appTop ((D.map (fj _ (Finset.mem_image_of_mem i (hσiσ y)))).appTop (f _))

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.appTop, CategoryTheory.Functor.map, Finset.mem_image_of_mem, DFunLike.coe