awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
have 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
Tactic: choose i V hV hVi using fun x : s ↦ hs x.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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)
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
have 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)
                  sorry))
            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
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)⟩:)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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)
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
have 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
Tactic: replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).some
Cleared hypotheses: fj
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
have refine_1 : IsCompact (↑(⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k) : Set ↥(D.obj j))
Tactic: refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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))
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
have refine_2 : c.π.app j ⁻¹ᵁ ⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k = sSup s
Tactic: refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 (↑(⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k) : Set ↥(D.obj j))
have 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))))
Tactic: simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
      TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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)
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = U
have 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
Tactic: classical
  obtain ⟨s, hs, hsf, rfl⟩ := (isBasis_preimage_isAffineOpen D c hc).exists_finite_of_isCompact hU
  have : Finite s := hsf
  choose i V hV hVi using fun x : s ↦ hs x.2
  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)⟩:)
  replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).some
  refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
  · simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
      TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_mk]
    exact isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact
  · simp [-TopologicalSpace.Opens.iSup_mk, Scheme.Hom.preimage_iSup,
      ← Scheme.Hom.comp_preimage, c.w, hVi, sSup_eq_iSup']
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
have 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)) (this : Finite.{u + 1} (↑s : Type u)),
  ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
Tactic: classical
  obtain ⟨s, hs, hsf, rfl⟩ := (isBasis_preimage_isAffineOpen D c hc).exists_finite_of_isCompact hU
  have : Finite s := hsf
  choose i V hV hVi using fun x : s ↦ hs x.2
  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)⟩:)
  replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).some
  refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
  · simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
      TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_mk]
    exact isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact
  · simp [-TopologicalSpace.Opens.iSup_mk, Scheme.Hom.preimage_iSup,
      ← Scheme.Hom.comp_preimage, c.w, hVi, sSup_eq_iSup']
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
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)) (this : Finite.{u + 1} (↑s : Type u)),
    ∃ (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
have 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)) (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)),
  ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
Tactic: classical
  obtain ⟨s, hs, hsf, rfl⟩ := (isBasis_preimage_isAffineOpen D c hc).exists_finite_of_isCompact hU
  have : Finite s := hsf
  choose i V hV hVi using fun x : s ↦ hs x.2
  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)⟩:)
  replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).some
  refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
  · simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
      TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_mk]
    exact isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact
  · simp [-TopologicalSpace.Opens.iSup_mk, Scheme.Hom.preimage_iSup,
      ← Scheme.Hom.comp_preimage, c.w, hVi, sSup_eq_iSup']
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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)
⊢ CompactSpace.{u} ↥c.pt
have obtain : ∀ (i : I), CompactSpace.{u} ↥c.pt
Tactic: obtain ⟨i⟩ := IsCofiltered.nonempty (C := I)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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
⊢ CompactSpace.{u} ↥c.pt
have this : ∀ (i : I), IsAffineHom (c.π.app i)
Tactic: have := isAffineHom_π_app _ _ hc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have 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
Tactic: wlog hS : ∃ R, S = Spec R generalizing S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have 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
Tactic: wlog hS : ∃ R, S = Spec R generalizing S
Cleared hypotheses: S, t, f, inst_2, inst_4, ha, hb
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : IsAffine X
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
S : Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_6 : LocallyOfFiniteType f
inst_7 : 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
have obtain : ∀ (R : CommRingCat.{u}) (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
  [IsAffine.{u} (Spec R)] (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f),
  ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
Tactic: obtain ⟨R, rfl⟩ := hS
Cleared hypotheses: S, t, f, inst_6, inst_7, ha, hb, hS
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : IsAffine X
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_6 : LocallyOfFiniteType f
inst_7 : IsAffine.{u} (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X) (hab : c.π.app i ≫ a = c.π.app j ≫ b)
      (f : X ⟶ Spec R) [LocallyOfFiniteType f] (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f)
      (hX : ∃ (S : CommRingCat.{u}), X = Spec S), ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : IsAffine X
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_6 : LocallyOfFiniteType f
inst_7 : IsAffine.{u} (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X) (hab : c.π.app i ≫ a = c.π.app j ≫ b)
        (f : X ⟶ Spec R) [LocallyOfFiniteType f] (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
        ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), ∃ (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
have wlog : ∀ {X : Scheme.{u}} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X) (hab : c.π.app i ≫ a = c.π.app j ≫ b)
  (f : X ⟶ Spec R) [LocallyOfFiniteType f] (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f)
  (hX : ∃ (S : CommRingCat.{u}), X = Spec S), ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
Cleared hypotheses: X, inst_3, a, b, hab, f, inst_6, ha, hb
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_4 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_5 : IsAffine.{u} (Spec R)
X : Scheme
inst_6 : IsAffine X
a : D.obj i ⟶ X
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : X ⟶ Spec R
inst_7 : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have obtain : ∀ (S : CommRingCat.{u}) [IsAffine.{u} (Spec S)] (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S)
  (hab : c.π.app i ≫ a = c.π.app j ≫ b) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f] (ha : t.app i = a ≫ f)
  (hb : t.app j = b ≫ f), ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, inst_6, a, b, hab, f, inst_7, ha, hb, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_4 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_5 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_6 : IsAffine.{u} (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : Spec S ⟶ Spec R
inst_7 : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)] (ha : t.app i = a ≫ Spec.map φ) (hb : t.app j = b ≫ Spec.map φ),
  ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst_7, ha, hb
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_4 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_5 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_6 : IsAffine.{u} (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst_7 : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have inr : ∀
  (this :
    ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace.{u} ↥(D.obj i)]
      [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
      (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b)
      (ha : t.app i = a ≫ Spec.map φ) (hb : t.app j = b ≫ Spec.map φ)
      (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
      ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b)
  (hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
  ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
Tactic: wlog hD : ∃ D' : I ⥤ CommRingCatᵒᵖ, D = D' ⋙ Scheme.Spec generalizing D