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)
inst_5 : IsQuasiAffine.{u} c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
rwa : c.π.app k ⁻¹ᵁ D.map fkj ⁻¹ᵁ (D.obj j).basicOpen r ≤ c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ U
rwa₁ : (c.π.app k ≫ D.map fkj) ⁻¹ᵁ (D.obj j).basicOpen r ≤ c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ U
rwa₂ : (c.π.app k ≫ D.map fkj) ⁻¹ᵁ (D.obj j).basicOpen r ≤ (c.π.app k ≫ D.map fki) ⁻¹ᵁ U
rwa₃ : c.π.app j ⁻¹ᵁ (D.obj j).basicOpen r ≤ (c.π.app k ≫ D.map fki) ⁻¹ᵁ U
rwa₄ : c.π.app j ⁻¹ᵁ (D.obj j).basicOpen r ≤ c.π.app i ⁻¹ᵁ U
⊢ c.π.app k ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ U
have rwa₅ : (Functor.obj (Functor.obj (Functor.const I) c.pt) k).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
        (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj k, ⊤) : Type u))
      r) ≤
  c.π.app i ⁻¹ᵁ U
Tactic: rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top]
-- 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)
inst_5 : IsQuasiAffine.{u} c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
⊢ ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
    IsAffineOpen ((D.obj i).basicOpen f) ∧
      Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))
have obtain : ∀ (l : I) (flk : l ⟶ k)
  (hl :
    D.map flk ⁻¹ᵁ
        (D.obj k).basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
            r) ≤
      D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U),
  ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
    IsAffineOpen ((D.obj i).basicOpen f) ∧
      Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))
Tactic: obtain ⟨l, flk, hl⟩ := exists_map_preimage_le_map_preimage D c hc (isCompact_basicOpen _
      isCompact_univ ((D.map fkj).appTop r)) (V := D.map fki ⁻¹ᵁ U) (by
        rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top])
-- 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)
inst_5 : IsQuasiAffine.{u} c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
    IsAffineOpen ((D.obj i).basicOpen f) ∧
      Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))
have refine_1 : IsAffineOpen.{u} (X := D.obj l)
  ((D.obj l).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
        (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
      r))
Tactic: refine ⟨l, (D.map (flk ≫ fkj)).appTop r, ?_, ?_⟩
-- 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)
inst_5 : IsQuasiAffine.{u} c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
refine_1 :
  IsAffineOpen.{u} (X := D.obj l)
    ((D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r))
⊢ ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
    IsAffineOpen ((D.obj i).basicOpen f) ∧
      Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))
have refine_2 : Membership.mem (α := ↥(D.obj l)) (γ := (D.obj l).Opens)
  ((D.obj l).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
        (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
      r))
  ((c.π.app l) x : ↥(D.obj l))
Tactic: refine ⟨l, (D.map (flk ≫ fkj)).appTop r, ?_, ?_⟩
-- 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)
inst_5 : IsQuasiAffine.{u} c.pt
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have this : ∀ (x : ↥c.pt),
  ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
    IsAffineOpen ((D.obj i).basicOpen f) ∧
      Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))
Tactic: have (x : c.pt) : ∃ (i : I) (f : Γ(D.obj i, ⊤)),
      IsAffineOpen (Scheme.basicOpen _ f) ∧ c.π.app i x ∈ (Scheme.basicOpen _ f) := by
    obtain ⟨i⟩ := IsCofiltered.nonempty (C := I)
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (c.π.app i x)) isOpen_univ
    obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, hrU⟩ :=
      (IsQuasiAffine.isBasis_basicOpen c.pt).exists_subset_of_mem_open hxU (c.π.app i ⁻¹ᵁ U).isOpen
    obtain ⟨j, r, rfl⟩ := exists_appTop_π_eq_of_isLimit D c hc r
    obtain ⟨k, fki, fkj, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    obtain ⟨l, flk, hl⟩ := exists_map_preimage_le_map_preimage D c hc (isCompact_basicOpen _
      isCompact_univ ((D.map fkj).appTop r)) (V := D.map fki ⁻¹ᵁ U) (by
        rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top])
    refine ⟨l, (D.map (flk ≫ fkj)).appTop r, ?_, ?_⟩
    · convert!
      (hU.preimage (D.map (flk ≫ fki))).basicOpen
        ((D.obj _).presheaf.map (homOfLE le_top).op ((D.map (flk ≫ fkj)).appTop r)) using 1
      rwa [Scheme.basicOpen_res, eq_comm, inf_eq_right, Functor.map_comp,
        elementwise_of% Scheme.Hom.comp_appTop, ← Scheme.preimage_basicOpen_top, Functor.map_comp,
        Scheme.Hom.comp_preimage]
    · change x ∈ c.π.app l ⁻¹ᵁ (D.obj l).basicOpen _
      rwa [Scheme.preimage_basicOpen_top, ← elementwise_of% Scheme.Hom.comp_appTop, Cone.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)
inst_5 : IsQuasiAffine.{u} c.pt
this :
  ∀ (x : ↥c.pt),
    ∃ (i : I) (f : (↑Γ(D.obj i, ⊤) : Type u)),
      IsAffineOpen ((D.obj i).basicOpen f) ∧
        Membership.mem (α := ↥(D.obj i)) ((D.obj i).basicOpen f) ((c.π.app i) x : ↥(D.obj i))
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have choose : ∀ (i : (x : ↥c.pt) → I) (f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u))
  (hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x)))
  (hi :
    ∀ (x : ↥c.pt),
      Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))),
  ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
Tactic: choose i f hf hi using this
Cleared hypotheses: this
-- 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)
inst_5 : IsQuasiAffine.{u} c.pt
i : (x : ↥c.pt) → I
f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi :
  ∀ (x : ↥c.pt),
    Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have obtain : ∀ (σ : Finset ↥c.pt)
  (hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤),
  ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
Tactic: obtain ⟨σ, hσ⟩ := CompactSpace.elim_nhds_subcover
    (fun x ↦ (((c.π.app (i x)) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).1))
    (fun x ↦ ((c.π.app (i x)) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).2.mem_nhds (by exact hi 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)
inst_5 : IsQuasiAffine.{u} c.pt
i : (x : ↥c.pt) → I
f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi :
  ∀ (x : ↥c.pt),
    Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have choose : ∀ (σi : (x : ↥c.pt) → ↥c.pt) (hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ)
  (hσi :
    ∀ (x : ↥c.pt),
      Membership.mem (γ := Set ↥c.pt)
        (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
          Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
        x),
  ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
Tactic: choose σi hσiσ hσi using fun x ↦ Set.mem_iUnion₂.mp (hσ.ge (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)
inst_5 : IsQuasiAffine.{u} c.pt
i : (x : ↥c.pt) → I
f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi :
  ∀ (x : ↥c.pt),
    Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have obtain : ∀ (j : I) (fj : ∀ {X : I}, X ∈ Finset.image i σ → Nonempty.{u + 1} (j ⟶ X)), ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
Tactic: obtain ⟨j, fj⟩ := IsCofiltered.inf_objs_exists (σ.image i)
-- 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)
inst_5 : IsQuasiAffine.{u} c.pt
i : (x : ↥c.pt) → I
f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi :
  ∀ (x : ↥c.pt),
    Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : ∀ {X : I}, X ∈ Finset.image i σ → Nonempty.{u + 1} (j ⟶ X)
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have replace : ∀ (fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1), ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
Tactic: replace fj := fun i h ↦ (@fj i h).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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
inst_5 : IsQuasiAffine.{u} c.pt
i : (x : ↥c.pt) → I
f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi :
  ∀ (x : ↥c.pt),
    Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
⊢ c.π.app j ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
have refine : ∀ (x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)),
  Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)) ⊤ x →
    Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi x)) sorry) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x)))
      ((c.π.app j) x : ↥(D.obj j))
Tactic: refine top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨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)
inst_5 : IsQuasiAffine.{u} c.pt
i : (x : ↥c.pt) → I
f : (x : ↥c.pt) → (↑Γ(D.obj (i x), ⊤) : Type u)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi :
  ∀ (x : ↥c.pt),
    Membership.mem (α := ↥(D.obj (i x))) ((D.obj (i x)).basicOpen (f x)) ((c.π.app (i x)) x : ↥(D.obj (i x)))
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)
h : Membership.mem (γ := TopologicalSpace.Opens ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) j)) ⊤ x
⊢ Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi x)) ⋯) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x)))
    ((c.π.app j) x : ↥(D.obj j))
have change : Membership.mem (α := ↥(D.obj (i (σi x)))) (γ := (D.obj (i (σi x))).Opens) ((D.obj (i (σi x))).basicOpen (f (σi x)))
  ((c.π.app j ≫ D.map (fj (i (σi x)) sorry)) x : ↥(D.obj (i (σi x))))
Tactic: change (c.π.app j ≫ D.map _).base x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))