awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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))
h :
  IsAffineOpen (D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))) ∧
    x ∈ D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))
⊢ 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

Tactic:
rw [← Scheme.preimage_basicOpen_top, ← Scheme.preimage_basicOpen_top]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen_top
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 (D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))) ∧
    x ∈ D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))

Tactic:
⟨((hf _).preimage _).preimage _, hy⟩

Premises used: And.intro, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 (D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))) ∧
    x ∈ D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))

Tactic:
exact ⟨((hf _).preimage _).preimage _, hy⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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), IsAffineHom (c.π.app i)

Tactic:
have := isAffineHom_π_app _ _ hc
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
obtain : ∀ (i : I) (hi : IsQuasiAffine.{u} (D.obj i)), ∃ (i : I), IsAffine.{u} (D.obj i)
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)

Tactic:
obtain ⟨i, hi⟩ := Scheme.exists_isQuasiAffine_of_isLimit D c hc

Premises used: AlgebraicGeometry.Scheme.exists_isQuasiAffine_of_isLimit
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
dsimp : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Spec.map (Hom.appTop (D.map f)))
⊢ ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 (Spec.map (Hom.appTop (D.map f)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)

Tactic:
have : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f) := by
    dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
dsimp : CompactSpace.{u} ↥(Spec Γ(D.obj j, ⊤))
⊢ CompactSpace.{u} ↥((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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} ↥(Spec Γ(D.obj j, ⊤))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)

Tactic:
have (j : _) : CompactSpace ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j) := by dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
⊢ Eq.{u + 1} (α := (Spec Γ(c.pt, ⊤)).Opens) (Hom.opensRange c.pt.toSpecΓ) ⊤

Tactic:
simp [Hom.opensRange_of_isIso]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
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)
⊢ ∃ (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]))

Premises used: CategoryTheory.Limits.Cone.π, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.Scheme.Γ, CategoryTheory.Functor.comp, AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.Scheme.toSpecΓ, CategoryTheory.Functor.rightOp, AlgebraicGeometry.exists_map_eq_top, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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Γ = ⊤
⊢ IsQuasiAffine.{u} (D.obj j)

Tactic:
have := IsQuasiAffine.of_isAffineHom (D.map fij)
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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_3 : ∀ (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Γ = ⊤
this : IsQuasiAffine.{u} (D.obj j)
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)

Tactic:
⟨j, ⟨isIso_of_isOpenImmersion_of_opensRange_eq_top _
    ((preimage_opensRange_toSpecΓ (D.map fij)).symm.trans hj)⟩⟩

Premises used: AlgebraicGeometry.IsAffine.mk, CategoryTheory.Functor.map, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, Exists.intro, Eq.symm, AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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_3 : ∀ (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Γ = ⊤
this : IsQuasiAffine.{u} (D.obj j)
⊢ ∃ (i : I), IsAffine.{u} (D.obj i)

Tactic:
exact ⟨j, ⟨isIso_of_isOpenImmersion_of_opensRange_eq_top _
    ((preimage_opensRange_toSpecΓ (D.map fij)).symm.trans hj)⟩⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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

Tactic:
obtain ⟨i, U, hU', rfl⟩ := exists_preimage_eq D c hc U hU.isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.exists_preimage_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
⊢ ∀ (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')
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
⊢ ∀ (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 _)
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
⊢ IsAffine.{u} (opensCone D c i U).pt

Tactic:
have : IsAffine (opensCone D c i U).pt := hU
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
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
⊢ ∃ (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)

Premises used: AlgebraicGeometry.Scheme.exists_isAffine_of_isLimit, AlgebraicGeometry.isLimitOpensCone
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
j : Over i
hj : IsAffine.{u} ((opensDiagram D i U).obj j)
⊢ c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ U

Tactic:
simp [← Scheme.Hom.comp_preimage]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
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:
exact ⟨_, _, hj, by simp [← Scheme.Hom.comp_preimage]⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
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
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsAffineOpen V ∧ c.π.app i ⁻¹ᵁ V = 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]⟩

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.exists_preimage_eq, rfl