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
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 (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)) ⋯)) x : ↥(D.obj (i (σi x))))
have rw : Membership.mem (α := ↥(D.obj (i (σi x)))) (γ := (D.obj (i (σi x))).Opens) ((D.obj (i (σi x))).basicOpen (f (σi x)))
  ((c.π.app (i (σi x))) x : ↥(D.obj (i (σi x))))
Tactic: rw [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
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
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have obtain : ∀ (k : I) (fkj : k ⟶ j)
  (hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) sorry) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤),
  ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
Tactic: obtain ⟨k, fkj, hk⟩ := exists_map_eq_top D c hc
    (⨆ k, D.map (fj _ (Finset.mem_image_of_mem i (hσiσ k))) ⁻¹ᵁ (D.obj (i _)).basicOpen (f _)) (by
      refine top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, ?_⟩
      change (c.π.app j ≫ D.map _).base x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))
      rw [Cone.w]
      exact hσ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 : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
⊢ ∃ (i : I), IsQuasiAffine.{u} (D.obj i)
have refine : ∀ (x : ↥(D.obj k)), ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r
Tactic: refine ⟨k, .of_forall_exists_mem_basicOpen _ fun 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
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
⊢ ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r
have obtain : ∀ (y : ↥c.pt)
  (hy :
    Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi y)) sorry) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y)))
      ((D.map fkj) x : ↥(D.obj j))),
  ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r
Tactic: obtain ⟨y, hy⟩ := TopologicalSpace.Opens.mem_iSup.mp (hk.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
j : I
fj : (i_1 : I) → (h : i_1 ∈ Finset.image i σ) → j ⟶ i_1
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
y : ↥c.pt
hy :
  Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y)))
    ((D.map fkj) x : ↥(D.obj j))
⊢ ∃ (r : (↑Γ(D.obj k, ⊤) : Type u)), IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r
have h : IsAffineOpen.{u} (X := D.obj 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))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (D.map (fj (i (σi y)) sorry))) :
              (a : (↑Γ(D.obj (i (σi y)), ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
            (f (σi y)) :
          (↑Γ(D.obj j, ⊤) : Type u)))) ∧
  Membership.mem (γ := (D.obj k).Opens)
    ((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))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (D.map (fj (i (σi y)) sorry))) :
              (a : (↑Γ(D.obj (i (σi y)), ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
            (f (σi y)) :
          (↑Γ(D.obj j, ⊤) : Type u))))
    x
Tactic: use (D.map fkj).appTop ((D.map (fj _ (Finset.mem_image_of_mem i (hσiσ y)))).appTop (f _))
-- 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
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ (k : ↥c.pt), D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
y : ↥c.pt
hy :
  Membership.mem (α := ↥(D.obj j)) (D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y)))
    ((D.map fkj) x : ↥(D.obj j))
⊢ IsAffineOpen.{u} (X := D.obj 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))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop (D.map (fj (i (σi y)) ⋯))) :
                (a : (↑Γ(D.obj (i (σi y)), ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
              (f (σi y)) :
            (↑Γ(D.obj j, ⊤) : Type u)))) ∧
    Membership.mem (γ := (D.obj k).Opens)
      ((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))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop (D.map (fj (i (σi y)) ⋯))) :
                (a : (↑Γ(D.obj (i (σi y)), ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
              (f (σi y)) :
            (↑Γ(D.obj j, ⊤) : Type u))))
      x
have h : IsAffineOpen (D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) sorry) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))) ∧
  x ∈ D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) sorry) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))
Tactic: rw [← Scheme.preimage_basicOpen_top, ← Scheme.preimage_basicOpen_top]
-- 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 : IsAffine.{u} c.pt
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)
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
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 : IsAffine.{u} c.pt
this : ∀ (i : I), IsAffineHom (c.π.app i)
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)
have obtain : ∀ (i : I) (hi : IsQuasiAffine.{u} (D.obj i)), ∃ (i : I), IsAffine.{u} (D.obj i)
Tactic: obtain ⟨i, hi⟩ := Scheme.exists_isQuasiAffine_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)
inst_5 : IsAffine.{u} c.pt
this : ∀ (i : I), IsAffineHom (c.π.app i)
i : I
hi : IsQuasiAffine.{u} (D.obj i)
⊢ ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)
have dsimp : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Spec.map (Hom.appTop (D.map f)))
Tactic: dsimp
-- 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 : IsAffine.{u} c.pt
this : ∀ (i : I), IsAffineHom (c.π.app i)
i : I
hi : IsQuasiAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)
have this₁ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)
Tactic: have : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f) := by
    dsimp; infer_instance
-- 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 : IsAffine.{u} c.pt
this_1 : ∀ (i : I), IsAffineHom (c.π.app i)
i : I
hi : IsQuasiAffine.{u} (D.obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)
j : I
⊢ CompactSpace.{u} ↥((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j)
have dsimp : CompactSpace.{u} ↥(Spec Γ(D.obj j, ⊤))
Tactic: dsimp
-- 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 : IsAffine.{u} c.pt
this_1 : ∀ (i : I), IsAffineHom (c.π.app i)
i : I
hi : IsQuasiAffine.{u} (D.obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)
have this₁ : ∀ (j : I), CompactSpace.{u} ↥((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j)
Tactic: have (j : _) : CompactSpace ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j) := by dsimp; infer_instance
-- 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 : IsAffine.{u} c.pt
this_1 : ∀ (i : I), IsAffineHom (c.π.app i)
i : I
hi : IsQuasiAffine.{u} (D.obj i)
this_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)
this : ∀ (j : I), CompactSpace.{u} ↥((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j)
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)
have obtain : ∀ (j : I) (fij : j ⟶ i) (hj : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map fij ⁻¹ᵁ Hom.opensRange (D.obj i).toSpecΓ = ⊤),
  ∃ (i : I), IsAffine.{u} (D.obj i)
Tactic: obtain ⟨j, fij, hj⟩ := exists_map_eq_top _ _
    (isLimitOfPreserves (Scheme.Γ.rightOp ⋙ Scheme.Spec) hc) (D.obj i).toSpecΓ.opensRange
    ((preimage_opensRange_toSpecΓ (X := c.pt) (c.π.app i)).trans
      (by simp [Hom.opensRange_of_isIso]))
-- 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 : IsAffine.{u} c.pt
this_1 : ∀ (i : I), IsAffineHom (c.π.app i)
i : I
hi : IsQuasiAffine.{u} (D.obj i)
this_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)
this : ∀ (j : I), CompactSpace.{u} ↥((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j)
j : I
fij : j ⟶ i
hj : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map fij ⁻¹ᵁ Hom.opensRange (D.obj i).toSpecΓ = ⊤
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)
have this₁ : IsQuasiAffine.{u} (D.obj j)
Tactic: have := IsQuasiAffine.of_isAffineHom (D.map fij)
-- 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
⊢ ∃ (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)),
  ∃ (i_1 : I) (V : (D.obj i_1).Opens), IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Tactic: obtain ⟨i, U, hU', rfl⟩ := exists_preimage_eq D c hc U hU.isCompact
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), QuasiSeparatedSpace.{u} ↥(D.obj i)
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
have this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
Tactic: have (j : Over i) : CompactSpace ((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage _ U.2 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), QuasiSeparatedSpace.{u} ↥(D.obj i)
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
have this₁ : ∀ (j : Over i), QuasiSeparatedSpace.{u} ↥((opensDiagram D i U).obj j)
Tactic: have (j : Over i) : QuasiSeparatedSpace ((opensDiagram D i U).obj j) :=
    (isQuasiSeparated_iff_quasiSeparatedSpace _ (D.map _ ⁻¹ᵁ _).2).mp (.of_quasiSeparatedSpace _)
-- 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), QuasiSeparatedSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact (↑U : Set ↥(D.obj i))
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this_1 : ∀ (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
have this₁ : IsAffine.{u} (opensCone D c i U).pt
Tactic: have : IsAffine (opensCone D c i U).pt := 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)
i : I
U : (D.obj i).Opens
hU' : IsCompact (↑U : Set ↥(D.obj i))
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this_1 : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
this_2 : ∀ (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
have obtain : ∀ (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: obtain ⟨j, hj⟩ := Scheme.exists_isAffine_of_isLimit _ _ (isLimitOpensCone D c hc i U)
-- 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
⊢ ∃ (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)),
  ∃ (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