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), QuasiSeparatedSpace.{u} ↥(D.obj i)
U : c.pt.Opens
hU : IsAffineOpen U
obtain :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsAffineOpen V ∧ c.π.app i ⁻¹ᵁ V = U
have obtain₁ : ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
  (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)),
  ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Tactic: classical
  obtain ⟨i, U, hU', rfl⟩ := exists_preimage_eq D c hc U hU.isCompact
  have (j : Over i) : CompactSpace ((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage _ U.2 hU')
  have (j : Over i) : QuasiSeparatedSpace ((opensDiagram D i U).obj j) :=
    (isQuasiSeparated_iff_quasiSeparatedSpace _ (D.map _ ⁻¹ᵁ _).2).mp (.of_quasiSeparatedSpace _)
  have : IsAffine (opensCone D c i U).pt := hU
  obtain ⟨j, hj⟩ := Scheme.exists_isAffine_of_isLimit _ _ (isLimitOpensCone D c hc i U)
  exact ⟨_, _, hj, by simp [← Scheme.Hom.comp_preimage]⟩
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), QuasiSeparatedSpace.{u} ↥(D.obj i)
U : c.pt.Opens
hU : IsAffineOpen U
obtain :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
obtain₁ :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
    (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsAffineOpen V ∧ c.π.app i ⁻¹ᵁ V = U
have obtain₂ : ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
  (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j))
  (this : ∀ (j : Over i), QuasiSeparatedSpace.{u} ↥((opensDiagram D i U).obj j)),
  ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Tactic: classical
  obtain ⟨i, U, hU', rfl⟩ := exists_preimage_eq D c hc U hU.isCompact
  have (j : Over i) : CompactSpace ((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage _ U.2 hU')
  have (j : Over i) : QuasiSeparatedSpace ((opensDiagram D i U).obj j) :=
    (isQuasiSeparated_iff_quasiSeparatedSpace _ (D.map _ ⁻¹ᵁ _).2).mp (.of_quasiSeparatedSpace _)
  have : IsAffine (opensCone D c i U).pt := hU
  obtain ⟨j, hj⟩ := Scheme.exists_isAffine_of_isLimit _ _ (isLimitOpensCone D c hc i U)
  exact ⟨_, _, hj, by simp [← Scheme.Hom.comp_preimage]⟩
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), QuasiSeparatedSpace.{u} ↥(D.obj i)
U : c.pt.Opens
hU : IsAffineOpen U
obtain :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
obtain₁ :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
    (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
obtain₂ :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
    (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j))
    (this : ∀ (j : Over i), QuasiSeparatedSpace.{u} ↥((opensDiagram D i U).obj j)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsAffineOpen V ∧ c.π.app i ⁻¹ᵁ V = U
have obtain₃ : ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
  (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j))
  (this : ∀ (j : Over i), QuasiSeparatedSpace.{u} ↥((opensDiagram D i U).obj j))
  (this : IsAffine.{u} (opensCone D c i U).pt),
  ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Tactic: classical
  obtain ⟨i, U, hU', rfl⟩ := exists_preimage_eq D c hc U hU.isCompact
  have (j : Over i) : CompactSpace ((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage _ U.2 hU')
  have (j : Over i) : QuasiSeparatedSpace ((opensDiagram D i U).obj j) :=
    (isQuasiSeparated_iff_quasiSeparatedSpace _ (D.map _ ⁻¹ᵁ _).2).mp (.of_quasiSeparatedSpace _)
  have : IsAffine (opensCone D c i U).pt := hU
  obtain ⟨j, hj⟩ := Scheme.exists_isAffine_of_isLimit _ _ (isLimitOpensCone D c hc i U)
  exact ⟨_, _, hj, by simp [← Scheme.Hom.comp_preimage]⟩
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), QuasiSeparatedSpace.{u} ↥(D.obj i)
U : c.pt.Opens
hU : IsAffineOpen U
obtain :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
obtain₁ :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
    (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
obtain₂ :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
    (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j))
    (this : ∀ (j : Over i), QuasiSeparatedSpace.{u} ↥((opensDiagram D i U).obj j)),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
obtain₃ :
  ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
    (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j))
    (this : ∀ (j : Over i), QuasiSeparatedSpace.{u} ↥((opensDiagram D i U).obj j))
    (this : IsAffine.{u} (opensCone D c i U).pt),
    ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsAffineOpen V ∧ c.π.app i ⁻¹ᵁ V = U
have obtain₄ : ∀ (i : I) (U : (D.obj i).Opens) (hU' : IsCompact (↑U : Set ↥(D.obj i))) (hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U))
  (this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j))
  (this : ∀ (j : Over i), QuasiSeparatedSpace.{u} ↥((opensDiagram D i U).obj j))
  (this : IsAffine.{u} (opensCone D c i U).pt) (j : Over i) (hj : IsAffine.{u} ((opensDiagram D i U).obj j)),
  ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Tactic: classical
  obtain ⟨i, U, hU', rfl⟩ := exists_preimage_eq D c hc U hU.isCompact
  have (j : Over i) : CompactSpace ((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage _ U.2 hU')
  have (j : Over i) : QuasiSeparatedSpace ((opensDiagram D i U).obj j) :=
    (isQuasiSeparated_iff_quasiSeparatedSpace _ (D.map _ ⁻¹ᵁ _).2).mp (.of_quasiSeparatedSpace _)
  have : IsAffine (opensCone D c i U).pt := hU
  obtain ⟨j, hj⟩ := Scheme.exists_isAffine_of_isLimit _ _ (isLimitOpensCone D c hc i U)
  exact ⟨_, _, hj, by simp [← Scheme.Hom.comp_preimage]⟩
Cleared hypotheses: U, hU
-- 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)
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 this : CompactSpace.{u} ↥c.pt
Tactic: have := compactSpace_of_isLimit D c hc
-- 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)
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 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
Tactic: choose j V hV hVU using fun k ↦ exists_isAffineOpen_preimage_eq D c hc (U k) (hU' 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)
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
⊢ ∃ (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 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
Tactic: obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge
-- 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)
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
have 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
Tactic: obtain ⟨i, fi⟩ := IsCofiltered.inf_objs_exists (s.image j)
-- 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)
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
have 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
Tactic: replace fi : ∀ k ∈ s, i ⟶ j k := fun k hk ↦ (fi (Finset.mem_image_of_mem _ hk)).some
Cleared hypotheses: fi
-- 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)
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)
⊢ c.π.app i ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤
have simp_rw : Eq.{u + 1} (α := (Functor.obj (Functor.obj (Functor.const I) c.pt) i).Opens) (⨆ i_1 ∈ s, U i_1) ⊤
Tactic: simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, c.w, hVU]
-- 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)
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)
⊢ ∃ (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 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
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))
-- 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)
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
have refine_1 : IsOpenCover.{u_1, u} (X := ↥(D.obj k)) fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) sorry) ⁻¹ᵁ V (↑x : J)
Tactic: refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩
-- 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)
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)
⊢ ∃ (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 refine_2 : ∀ (k_1 : ↥s), U (↑k_1 : J) = c.π.app k ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) sorry) ⁻¹ᵁ V (↑x : J)) k_1
Tactic: refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩
-- 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)
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)
have 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) sorry) ⁻¹ᵁ V (↑x : J)
Tactic: refine top_le_iff.mp (e.symm.trans_le ?_)
-- 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)
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 = ⊤
⊢ 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)
have refine_1 : LE.le.{u} (α := (D.obj k).Opens) (⨆ (i_1 : J), ⨆ (x : i_1 ∈ s), D.map (fkj ≫ fi i_1 sorry) ⁻¹ᵁ V i_1)
  (⨆ (i_1 : J), ⨆ (x : i_1 ∈ s), D.map (fkj ≫ fi i_1 sorry) ⁻¹ᵁ V i_1)
Tactic: simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, iSup_subtype, ← D.map_comp]
-- 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)
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
⊢ U (↑k : J) = c.π.app k_1 ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)) k
have refine_2 : c.π.app (j (↑k : J)) ⁻¹ᵁ V (↑k : J) = c.π.app k_1 ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) sorry) ⁻¹ᵁ V (↑x : J)) k
Tactic: 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)
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
⊢ U (↑k : J) = c.π.app k_1 ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)) k
have refine_2₁ : c.π.app (j (↑k : J)) ⁻¹ᵁ V (↑k : J) = (c.π.app k_1 ≫ D.map (fkj ≫ fi (↑k : J) sorry)) ⁻¹ᵁ V (↑k : J)
Tactic: 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)
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)
⊢ U (↑k : J) = c.π.app k_1 ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)) k
have 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))
Tactic: rw [← hVU, ← Hom.comp_preimage, c.w]