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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
⊢ CompactSpace.{u} ↥c.pt

Tactic:
have := compactSpace_of_isLimit D c hc
-- 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
choose :
  ∀ (j : (k : J) → I) (V : (k : J) → (D.obj (j k)).Opens) (hV : ∀ (k : J), IsAffineOpen (V k))
    (hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j

Tactic:
choose j V hV hVU using fun k ↦ exists_isAffineOpen_preimage_eq D c hc (U k) (hU' k)

Premises used: AlgebraicGeometry.exists_isAffineOpen_preimage_eq
-- 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
obtain :
  ∀ (s : Finset J) (hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j

Tactic:
obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge

Premises used: Eq.ge, TopologicalSpace.IsOpenCover.iSup_set_eq_univ, IsCompact.elim_finite_subcover, TopologicalSpace.Opens.isOpen, isCompact_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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
obtain :
  ∀ (i : I) (fi : ∀ {X : I}, X ∈ Finset.image j s → Nonempty.{u + 1} (i ⟶ X)),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j

Tactic:
obtain ⟨i, fi⟩ := IsCofiltered.inf_objs_exists (s.image j)

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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : ∀ {X : I}, X ∈ Finset.image j s → Nonempty.{u + 1} (i ⟶ X)
replace :
  ∀ (fi : (k : J) → k ∈ s → (i ⟶ j k)),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j

Tactic:
replace fi : ∀ k ∈ s, i ⟶ j k := fun k hk ↦ (fi (Finset.mem_image_of_mem _ hk)).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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
simp_rw : Eq.{u + 1} (α := (Functor.obj (Functor.obj (Functor.const I) c.pt) i).Opens) (⨆ i_1 ∈ s, U i_1) ⊤
⊢ c.π.app i ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤

Tactic:
simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, c.w, hVU]

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_iSup, 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)
h : Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)) ⊤ x
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)) (⨆ i_1 ∈ s, U i_1)
    x

Tactic:
simpa using hs (Set.mem_univ x)

Premises used: 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
⊢ Eq.{u + 1} (α := (Functor.obj (Functor.obj (Functor.const I) c.pt) i).Opens) (⨆ i_1 ∈ s, U i_1) ⊤

Tactic:
exact top_le_iff.mp fun x _ ↦ by simpa using hs (Set.mem_univ 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
obtain :
  ∀ (k : I) (fkj : k ⟶ i) (e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j

Tactic:
obtain ⟨k, fkj, e⟩ := exists_map_eq_top D c hc (⨆ (k) (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k) (by
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, c.w, hVU]
    exact top_le_iff.mp fun x _ ↦ by simpa using hs (Set.mem_univ x))

Premises used: iSup, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.exists_map_eq_top, 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j

Tactic:
⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, Subtype.val, CategoryTheory.Functor.obj, Subtype.property, AlgebraicGeometry.IsAffineOpen.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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
refine_1 : IsOpenCover.{u_1, u} (X := ↥(D.obj k)) fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)
refine_2 : ∀ (k_1 : ↥s), U (↑k_1 : J) = c.π.app k ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)) k_1
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j

Tactic:
refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
⊢ IsOpenCover.{u_1, u} (X := ↥(D.obj k)) fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)

Tactic:
top_le_iff.mp (e.symm.trans_le ?_)

Premises used: TopologicalSpace.IsOpenCover, Eq.trans_le, top_le_iff, Iff.mp, Eq.symm
-- 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
refine_1 :
  D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k ≤
    ⨆ (x : ↥s), D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)
⊢ IsOpenCover.{u_1, u} (X := ↥(D.obj k)) fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)

Tactic:
refine top_le_iff.mp (e.symm.trans_le ?_)

Premises used: Eq.trans_le, top_le_iff, Iff.mp, Eq.symm
-- 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
refine_1 :
  LE.le.{u} (α := (D.obj k).Opens) (⨆ (i_1 : J), ⨆ (x : i_1 ∈ s), D.map (fkj ≫ fi i_1 ⋯) ⁻¹ᵁ V i_1)
    (⨆ (i_1 : J), ⨆ (x : i_1 ∈ s), D.map (fkj ≫ fi i_1 ⋯) ⁻¹ᵁ V i_1)
⊢ D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k ≤
    ⨆ (x : ↥s), D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)

Tactic:
simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, iSup_subtype, ← D.map_comp]

Premises used: iSup_subtype, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Functor.map_comp
-- 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
⊢ LE.le.{u} (α := (D.obj k).Opens) (⨆ (i_1 : J), ⨆ (x : i_1 ∈ s), D.map (fkj ≫ fi i_1 ⋯) ⁻¹ᵁ V i_1)
    (⨆ (i_1 : J), ⨆ (x : i_1 ∈ s), D.map (fkj ≫ fi i_1 ⋯) ⁻¹ᵁ V i_1)

Tactic:
simp
-- 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)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace.{u} ↥c.pt
j : (k : J) → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
s : Finset J
hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))
i : I
fi : (k : J) → k ∈ s → (i ⟶ j k)
k_1 : I
fkj : k_1 ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
k : ↥s
refine_2 :
  c.π.app (j (↑k : J)) ⁻¹ᵁ V (↑k : J) = c.π.app k_1 ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)) k
refine_2₁ : c.π.app (j (↑k : J)) ⁻¹ᵁ V (↑k : J) = (c.π.app k_1 ≫ D.map (fkj ≫ fi (↑k : J) ⋯)) ⁻¹ᵁ V (↑k : J)
refine_2₂ refine_2₃ :
  Eq (α := c.pt.Opens)
    (c.π.app (j (↑k : J)) ⁻¹ᵁ V (↑k : J) : (Functor.obj (Functor.obj (Functor.const I) c.pt) (j (↑k : J))).Opens)
    (c.π.app (j (↑k : J)) ⁻¹ᵁ V (↑k : J))
⊢ U (↑k : J) = c.π.app k_1 ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)) k

Tactic:
rw [← hVU, ← Hom.comp_preimage, c.w]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Limits.Cone.w
-- 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 : LocallyOfFinitePresentation f
inst_3 : IsAffine S
inst_4 : IsAffine X
inst_5 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
inr :
  ∀
    (this :
      ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFinitePresentation f]
        [IsAffine S] (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f))
        (hS : ∃ (R : CommRingCat.{u}), S = Spec R), ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i)
    (hS : ¬∃ (R : CommRingCat.{u}), S = Spec R), ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
wlog :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFinitePresentation f] [IsAffine S]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
wlog hS : ∃ R, S = Spec R generalizing S
-- 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 : LocallyOfFinitePresentation f
inst_3 : IsAffine S
inst_4 : IsAffine X
inst_5 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
this :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFinitePresentation f] [IsAffine S]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hS : ¬∃ (R : CommRingCat.{u}), S = Spec R
⊢ c.π ≫ t ≫ Iso.hom (Functor.mapIso (Functor.const I) S.isoSpec) =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ f ≫ S.isoSpec.hom)

Tactic:
simp [reassoc_of% ha]
-- 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 : LocallyOfFinitePresentation f
inst_3 : IsAffine S
inst_4 : IsAffine X
inst_5 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
this :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFinitePresentation f] [IsAffine S]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hS : ¬∃ (R : CommRingCat.{u}), S = Spec R
inr :
  ∀ (i : I) (g : D.obj i ⟶ X) (hg : c.π.app i ≫ g = a)
    (hg' : g ≫ f ≫ S.isoSpec.hom = (t ≫ Iso.hom (Functor.mapIso (Functor.const I) S.isoSpec)).app i),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
obtain ⟨i, g, hg, hg'⟩ := this (t ≫ ((Functor.const I).mapIso S.isoSpec).hom)
      (f ≫ S.isoSpec.hom) (by simp [reassoc_of% ha]) ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.const, CategoryTheory.Iso.hom, CategoryTheory.Functor.mapIso, rfl
-- 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 : LocallyOfFinitePresentation f
inst_3 : IsAffine S
inst_4 : IsAffine X
inst_5 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
this :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFinitePresentation f] [IsAffine S]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hS : ¬∃ (R : CommRingCat.{u}), S = Spec R
i : I
g : D.obj i ⟶ X
hg : c.π.app i ≫ g = a
hg' : g ≫ f ≫ S.isoSpec.hom = (t ≫ Iso.hom (Functor.mapIso (Functor.const I) S.isoSpec)).app i
⊢ g ≫ f = t.app i

Tactic:
simpa using congr($hg' ≫ S.isoSpec.inv)

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Iso.inv
-- 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 : LocallyOfFinitePresentation f
inst_3 : IsAffine S
inst_4 : IsAffine X
inst_5 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
this :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFinitePresentation f] [IsAffine S]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hS : ¬∃ (R : CommRingCat.{u}), S = Spec R
i : I
g : D.obj i ⟶ X
hg : c.π.app i ≫ g = a
hg' : g ≫ f ≫ S.isoSpec.hom = (t ≫ Iso.hom (Functor.mapIso (Functor.const I) S.isoSpec)).app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
exact ⟨i, g, hg, by simpa using congr($hg' ≫ S.isoSpec.inv)⟩