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)
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)
⊢ ∃ (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
have have : ∀ (this : CompactSpace.{u} ↥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
Tactic: classical
  have := compactSpace_of_isLimit D c hc
  choose j V hV hVU using fun k ↦ exists_isAffineOpen_preimage_eq D c hc (U k) (hU' k)
  obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge
  obtain ⟨i, fi⟩ := IsCofiltered.inf_objs_exists (s.image j)
  replace fi : ∀ k ∈ s, i ⟶ j k := fun k hk ↦ (fi (Finset.mem_image_of_mem _ hk)).some
  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))
  refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩
  · refine top_le_iff.mp (e.symm.trans_le ?_)
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, iSup_subtype, ← D.map_comp]
    simp
  · rw [← hVU, ← Hom.comp_preimage, c.w]
-- 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)
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)
have have₁ have₂ :
  ∀ (this : CompactSpace.{u} ↥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
have have₃ : ∀ (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),
  ∃ (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: classical
  have := compactSpace_of_isLimit D c hc
  choose j V hV hVU using fun k ↦ exists_isAffineOpen_preimage_eq D c hc (U k) (hU' k)
  obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge
  obtain ⟨i, fi⟩ := IsCofiltered.inf_objs_exists (s.image j)
  replace fi : ∀ k ∈ s, i ⟶ j k := fun k hk ↦ (fi (Finset.mem_image_of_mem _ hk)).some
  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))
  refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩
  · refine top_le_iff.mp (e.symm.trans_le ?_)
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, iSup_subtype, ← D.map_comp]
    simp
  · rw [← hVU, ← Hom.comp_preimage, c.w]
-- 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)
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)
have have₁ have₂ :
  ∀ (this : CompactSpace.{u} ↥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
have₃ :
  ∀ (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),
    ∃ (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
have have₄ : ∀ (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) (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: classical
  have := compactSpace_of_isLimit D c hc
  choose j V hV hVU using fun k ↦ exists_isAffineOpen_preimage_eq D c hc (U k) (hU' k)
  obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge
  obtain ⟨i, fi⟩ := IsCofiltered.inf_objs_exists (s.image j)
  replace fi : ∀ k ∈ s, i ⟶ j k := fun k hk ↦ (fi (Finset.mem_image_of_mem _ hk)).some
  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))
  refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩
  · refine top_le_iff.mp (e.symm.trans_le ?_)
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, iSup_subtype, ← D.map_comp]
    simp
  · rw [← hVU, ← Hom.comp_preimage, c.w]
-- 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)
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)
have have₁ have₂ :
  ∀ (this : CompactSpace.{u} ↥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
have₃ :
  ∀ (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),
    ∃ (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
have₄ :
  ∀ (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) (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
have have₅ : ∀ (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)),
  ∃ (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: classical
  have := compactSpace_of_isLimit D c hc
  choose j V hV hVU using fun k ↦ exists_isAffineOpen_preimage_eq D c hc (U k) (hU' k)
  obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge
  obtain ⟨i, fi⟩ := IsCofiltered.inf_objs_exists (s.image j)
  replace fi : ∀ k ∈ s, i ⟶ j k := fun k hk ↦ (fi (Finset.mem_image_of_mem _ hk)).some
  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))
  refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩
  · refine top_le_iff.mp (e.symm.trans_le ?_)
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, iSup_subtype, ← D.map_comp]
    simp
  · rw [← hVU, ← Hom.comp_preimage, c.w]
-- 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 : 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)
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have 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
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 : 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
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have 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
Tactic: wlog hS : ∃ R, S = Spec R generalizing S
Cleared hypotheses: S, t, f, inst_2, inst_3, ha
-- 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 : 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), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have 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
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⟩
-- 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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
S : Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_4 : LocallyOfFinitePresentation f
inst_5 : 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
have obtain : ∀ (R : CommRingCat.{u}) (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (f : X ⟶ Spec R)
  [LocallyOfFinitePresentation f] [IsAffine.{u} (Spec R)]
  (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)),
  ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
Tactic: obtain ⟨R, rfl⟩ := hS
Cleared hypotheses: S, t, f, inst_4, inst_5, ha, 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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
      (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
      ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
        (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f))
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), ∃ (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
have wlog : ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
  (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
  ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
Cleared hypotheses: X, inst_2, a, f, inst_4, ha
-- 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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
this :
  ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have inr : ∀ (i : I) (f_1 : D.obj i ⟶ Spec Γ(X, ⊤)) (hf : c.π.app i ≫ f_1 = a ≫ X.isoSpec.hom ∧ f_1 ≫ X.isoSpec.inv ≫ f = t.app i),
  ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
Tactic: obtain ⟨i, f, hf⟩ := this (a ≫ X.isoSpec.hom) (X.isoSpec.inv ≫ f)
      (by simp [ha, - Functor.map_comp]) ⟨_, rfl⟩
-- 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 : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
X : Scheme
inst_4 : IsAffine X
a : c.pt ⟶ X
f : X ⟶ Spec R
inst_5 : LocallyOfFinitePresentation f
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have obtain : ∀ (S : CommRingCat.{u}) [IsAffine.{u} (Spec S)] (a : c.pt ⟶ Spec S) (f : Spec S ⟶ Spec R)
  [LocallyOfFinitePresentation f] (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)),
  ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, inst_4, a, f, inst_5, ha, 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 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
f : Spec S ⟶ Spec R
inst_5 : LocallyOfFinitePresentation f
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFinitePresentation (Spec.map φ)]
  (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)),
  ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst_5, ha
-- 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 : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
have inr : ∀
  (this :
    ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
      (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
      (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
      (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
      ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i)
  (hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
  ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
Tactic: wlog hD : ∃ D' : I ⥤ CommRingCatᵒᵖ, D = D' ⋙ Scheme.Spec generalizing D
-- 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 : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
inr :
  ∀
    (this :
      ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
        (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
        (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
        (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
        ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i)
    (hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
have wlog : ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
  (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
  (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
  (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
  ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
Tactic: wlog hD : ∃ D' : I ⥤ CommRingCatᵒᵖ, D = D' ⋙ Scheme.Spec generalizing D
Cleared hypotheses: D, c, hc, inst_2, t, a, ha
-- 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 : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
i : I
⊢ IsIso (e.app i)
have dsimp : IsIso.{u, u + 1} (X := D.obj i) (D.obj i).toSpecΓ
Tactic: dsimp [e]