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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this_1 : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i V).obj j)
r : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u)
hrU : (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r ≤ U
hxr :
  (↑(Subtype.mk (p := fun (x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)) ↦ x ∈ U) x hxU) :
      ↥(((Functor.const I).obj c.pt).obj i)) ∈
    (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r
j : Over i
s : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) : Type u)
hs :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const (Over i)ᵒᵖ)
          ((Scheme.Γ ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).mapCocone
              (opensCone D c i V).op).pt)
        (Opposite.op j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Scheme.Γ ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).mapCocone
                    (opensCone D c i V).op).ι.app
              (Opposite.op j)) :
          (a : (fun (X : Type u) ↦ X) (((opensDiagram D i V).op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj (Opposite.op j))) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Over i)ᵒᵖ).obj
                    ((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).pt).obj
                (Opposite.op j)))
        (((D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv :
            (a : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) : Type u)) → (↑Γ((↑(D.map j.hom ⁻¹ᵁ V) : Scheme), ⊤) : Type u))
          s) :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const (Over i)ᵒᵖ)
            ((Scheme.Γ ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier)).mapCocone
                (opensCone D c i V).op).pt)
          (Opposite.op j)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (c.π.app i ⁻¹ᵁ V).topIso.inv :
          (a : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u)) →
            (↑Γ((↑(c.π.app i ⁻¹ᵁ V) : Scheme), ⊤) : Type u))
        r :
      (↑Γ((↑(c.π.app i ⁻¹ᵁ V) : Scheme), ⊤) : Type u))
⊢ c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ V

Tactic:
have h : c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ V := congr($(c.w j.hom) ⁻¹ᵁ V)
-- 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)
U : c.pt.Opens
hU : IsCompact (↑U : Set ↥c.pt)
obtain :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = U

Tactic:
obtain ⟨s, hs, hsf, rfl⟩ := (isBasis_preimage_isAffineOpen D c hc).exists_finite_of_isCompact hU

Premises used: AlgebraicGeometry.isBasis_preimage_isAffineOpen, TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact, 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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
have : Finite s := hsf
-- 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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
choose :
  ∀ (i : (x : (↑s : Type u)) → I) (V : (x : (↑s : Type u)) → (D.obj (i x)).Opens)
    (hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x))
    (hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
choose i V hV hVi using fun x : s ↦ hs x.2

Premises used: Subtype.property
-- 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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
x : ↥(hsf.toFinset (s := s))
⊢ (↑x : TopologicalSpace.Opens ↥c.pt) ∈ s

Tactic:
simpa only [Set.Finite.mem_toFinset] using x.2

Premises used: Set.Finite.mem_toFinset, Subtype.property
-- 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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
obtain :
  ∀ (j : I)
    (fj :
      ∀ {X : I},
        Membership.mem (γ := Finset I)
            (Finset.image
              (fun (x : ↥(hsf.toFinset (s := s))) ↦
                i
                  (Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥c.pt) ↦ x ∈ s) (↑x : TopologicalSpace.Opens ↥c.pt)
                    ⋯))
              hsf.toFinset (s := s).attach)
            X →
          Nonempty.{u + 1} (j ⟶ X)),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
obtain ⟨j, fj⟩ := IsCofiltered.inf_objs_exists (hsf.toFinset.attach.image
    fun x ↦ i ⟨x.1, (by simpa only [Set.Finite.mem_toFinset] using x.2)⟩:)

Premises used: CategoryTheory.IsCofiltered.inf_objs_exists, Subtype.mk, Set.Finite.toFinset, Finset.attach, 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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj :
  ∀ {X : I},
    Membership.mem (γ := Finset I)
        (Finset.image
          (fun (x : ↥(hsf.toFinset (s := s))) ↦
            i (Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥c.pt) ↦ x ∈ s) (↑x : TopologicalSpace.Opens ↥c.pt) ⋯))
          hsf.toFinset (s := s).attach)
        X →
      Nonempty.{u + 1} (j ⟶ X)
b : (↑s : Type u)
⊢ Membership.mem (γ := Finset I)
    (Finset.image
      (fun (x : ↥(hsf.toFinset (s := s))) ↦
        i (Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥c.pt) ↦ x ∈ s) (↑x : TopologicalSpace.Opens ↥c.pt) ⋯))
      hsf.toFinset (s := s).attach)
    (i b)

Tactic:
simpa using ⟨b.1, b.2, 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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj :
  ∀ {X : I},
    Membership.mem (γ := Finset I)
        (Finset.image
          (fun (x : ↥(hsf.toFinset (s := s))) ↦
            i (Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥c.pt) ↦ x ∈ s) (↑x : TopologicalSpace.Opens ↥c.pt) ⋯))
          hsf.toFinset (s := s).attach)
        X →
      Nonempty.{u + 1} (j ⟶ X)
replace :
  ∀ (fj : (b : (↑s : Type u)) → j ⟶ i b),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj : (b : (↑s : Type u)) → j ⟶ i b
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩

Premises used: iSup, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, And.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, 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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj : (b : (↑s : Type u)) → j ⟶ i b
refine_1 : IsCompact (↑(⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k) : Set ↥(D.obj j))
refine_2 : c.π.app j ⁻¹ᵁ ⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k = sSup s
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
-- 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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj : (b : (↑s : Type u)) → j ⟶ i b
refine_1 :
  IsCompact.{u} (X := ↥(D.obj j)) (⋃ (i_1 : (↑s : Type u)), ⇑(D.map (fj i_1)) ⁻¹' (↑(V i_1) : Set ↥(D.obj (i i_1))))
⊢ IsCompact (↑(⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k) : Set ↥(D.obj j))

Tactic:
simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
      TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_mk]

Premises used: TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj : (b : (↑s : Type u)) → j ⟶ i b
⊢ IsCompact.{u} (X := ↥(D.obj j)) (⋃ (i_1 : (↑s : Type u)), ⇑(D.map (fj i_1)) ⁻¹' (↑(V i_1) : Set ↥(D.obj (i i_1))))

Tactic:
isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, CategoryTheory.Functor.map, isCompact_iUnion, 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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj : (b : (↑s : Type u)) → j ⟶ i b
⊢ IsCompact.{u} (X := ↥(D.obj j)) (⋃ (i_1 : (↑s : Type u)), ⇑(D.map (fj i_1)) ⁻¹' (↑(V i_1) : Set ↥(D.obj (i i_1))))

Tactic:
exact isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, isCompact_iUnion, 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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
this : Finite.{u + 1} (↑s : Type u)
i : (x : (↑s : Type u)) → I
V : (x : (↑s : Type u)) → (D.obj (i x)).Opens
hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x)
hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)
j : I
fj : (b : (↑s : Type u)) → j ⟶ i b
⊢ c.π.app j ⁻¹ᵁ ⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k = sSup s

Tactic:
simp [-TopologicalSpace.Opens.iSup_mk, Scheme.Hom.preimage_iSup,
      ← Scheme.Hom.comp_preimage, c.w, hVi, sSup_eq_iSup']

Premises used: TopologicalSpace.Opens.iSup_mk, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Limits.Cone.w, sSup_eq_iSup'
-- 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)
obtain : ∀ (i : I), CompactSpace.{u} ↥c.pt
⊢ CompactSpace.{u} ↥c.pt

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

Premises used: CategoryTheory.IsCofiltered.nonempty
-- 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)
i : I
⊢ ∀ (i : I), IsAffineHom (c.π.app i)

Tactic:
have := isAffineHom_π_app _ _ 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)
i : I
this : ∀ (i : I), IsAffineHom (c.π.app i)
⊢ CompactSpace.{u} ↥c.pt

Tactic:
QuasiCompact.compactSpace_of_compactSpace (c.π.app i)

Premises used: CategoryTheory.Limits.Cone.π, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, 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)
i : I
this : ∀ (i : I), IsAffineHom (c.π.app i)
⊢ CompactSpace.{u} ↥c.pt

Tactic:
exact QuasiCompact.compactSpace_of_compactSpace (c.π.app i)

Premises used: CategoryTheory.Limits.Cone.π, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, CategoryTheory.NatTrans.app
-- 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 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : IsAffine S
inst_5 : IsAffine X
inst_6 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_7 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
inr :
  ∀
    (this :
      ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFiniteType f] [IsAffine S]
        (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
        ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b)
    (hS : ¬∃ (R : CommRingCat.{u}), S = Spec R), ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
wlog :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFiniteType f] [IsAffine S]
    (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b

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 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : IsAffine S
inst_5 : IsAffine X
inst_6 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_7 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
this :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFiniteType f] [IsAffine S]
    (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hS : ¬∃ (R : CommRingCat.{u}), S = Spec R
⊢ (t ≫ Iso.hom (Functor.mapIso (Functor.const I) S.isoSpec)).app i = a ≫ f ≫ S.isoSpec.hom

Tactic:
simp [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 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : IsAffine S
inst_5 : IsAffine X
inst_6 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_7 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
this :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFiniteType f] [IsAffine S]
    (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hS : ¬∃ (R : CommRingCat.{u}), S = Spec R
⊢ (t ≫ Iso.hom (Functor.mapIso (Functor.const I) S.isoSpec)).app j = b ≫ f ≫ S.isoSpec.hom

Tactic:
simp [hb]
-- 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 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : IsAffine S
inst_5 : IsAffine X
inst_6 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_7 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
this :
  ∀ {S : Scheme.{u}} (t : D ⟶ Functor.obj (Functor.const I) S) (f : X ⟶ S) [LocallyOfFiniteType f] [IsAffine S]
    (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f) (hS : ∃ (R : CommRingCat.{u}), S = Spec R),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hS : ¬∃ (R : CommRingCat.{u}), S = Spec R
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b

Tactic:
exact this (t ≫ ((Functor.const I).mapIso S.isoSpec).hom)
      (f ≫ S.isoSpec.hom) (by simp [ha]) (by simp [hb]) ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.const, CategoryTheory.Iso.hom, CategoryTheory.Functor.mapIso, rfl