awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
rw₃ :
  Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₄ :
  Subset (α := Set ↥Y) (Set.range (ι := ↥(Hom.image f)) ⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₅ :
  (↑(Hom.ker f).support : Set ↥Y) ⊆
    closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))
rw₆ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₇ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.range (ι := ↥X) (Function.comp (β := ↥(Hom.image f)) ⇑(Hom.imageι f) ⇑(Hom.toImage f))))
rw₈ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure
      (Set.range (ι := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              ((Hom.toImage f).base ≫ (Hom.imageι f).base)) :
          (a : ↥X) → ↥Y)))
rw₉ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f ≫ Hom.imageι f)))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₁₀ : Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) (closure (Set.range (ι := ↥X) ⇑f))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
⊢ app (toImage f) (imageι f ⁻¹ᵁ (↑U : Y.Opens)) =
    ((ker f).subschemeObjIso U).hom ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯)
have this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
Tactic: have := ConcreteCategory.epi_of_surjective _ (f.ker.subschemeι_app_surjective U)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
⊢ app (toImage f) (imageι f ⁻¹ᵁ (↑U : Y.Opens)) =
    ((ker f).subschemeObjIso U).hom ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯)
have rw : app f (↑U : Y.Opens) =
  ((CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫ ((ker f).subschemeObjIso U).inv) ≫
      ((ker f).subschemeObjIso U).hom ≫
        CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) sorry)) ≫
    X.presheaf.map (inv (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [← cancel_epi (f.ker.subschemeι.app U), ← Scheme.Hom.comp_app,
    Scheme.Hom.congr_app f.toImage_imageι, f.ker.subschemeι_app,
    ← IsIso.eq_comp_inv, ← Functor.map_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
⊢ app f (↑U : Y.Opens) =
    ((CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫ ((ker f).subschemeObjIso U).inv) ≫
        ((ker f).subschemeObjIso U).hom ≫
          CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯)) ≫
      X.presheaf.map (inv (Quiver.Hom.op (eqToHom ⋯)))
have simp : app f (↑U : Y.Opens) =
  CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫
    CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) sorry) ≫
      X.presheaf.map (eqToHom sorry)
Tactic: simp only [Hom.comp_base, Opens.map_comp_obj, Category.assoc,
    Iso.inv_hom_id_assoc, eqToHom_op, inv_eqToHom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
⊢ app f (↑U : Y.Opens) =
    CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯) ≫
        X.presheaf.map (eqToHom ⋯)
have rw : app f (↑U : Y.Opens) =
  app f (↑U : Y.Opens) ≫ 𝟙 Γ(X, (Opens.map (toImage f).base).obj ((Opens.map (imageι f).base).obj (↑U : Y.Opens)))
Tactic: rw [← reassoc_of% CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk, CommRingCat.ofHom_hom,
    eqToHom_refl, CategoryTheory.Functor.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
⊢ Function.Injective (α := (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) (β :=
    (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)))
          (app (toImage f) (imageι f ⁻¹ᵁ (↑U : Y.Opens)))) :
      (a : (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
        (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
have simp : Function.Injective (α := (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) (β :=
  (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  (Function.comp (β := (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U)
    (⇑(Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) sorry) :
      (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U) →
        (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (⇑(CommRingCat.Hom.hom ((ker f).subschemeObjIso U).hom) :
      (a : (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U))
Tactic: simp only [f.toImage_app U, CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
x : ↥(image f)
⊢ Function.Injective (α := (↑(Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat x) (image f).presheaf) : Type u))
    (β :=
    (↑(Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat x)
          (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toImage f).base) X.presheaf)) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat x) (image f).presheaf)
          (CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor CommRingCat x) (toImage f).c)) :
      (a : (↑((TopCat.Presheaf.stalkFunctor CommRingCat x).obj (image f).presheaf) : Type u)) →
        (↑((TopCat.Presheaf.stalkFunctor CommRingCat x).obj
              ((TopCat.Presheaf.pushforward CommRingCat (toImage f).base).obj X.presheaf)) :
          Type u))
have hα : ∀ (U : TopologicalSpace.Opens ↥(image f)),
  Membership.mem (γ := Set (TopologicalSpace.Opens ↥(image f)))
      {x : TopologicalSpace.Opens ↥(image f) |
        ∃ U ∈ Y.affineOpens,
          { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := sorry : TopologicalSpace.Opens ↥(image f) } = x}
      U →
    Function.Injective (α := (↑((image f).presheaf.obj (Opposite.op U)) : Type u)) (β :=
      (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toImage f).base) X.presheaf).obj (Opposite.op U)) :
        Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := (image f).presheaf.obj (Opposite.op U)) ((toImage f).c.app (Opposite.op U))) :
        (a : (↑((image f).presheaf.obj (Opposite.op U)) : Type u)) →
          (↑(((TopCat.Presheaf.pushforward CommRingCat (toImage f).base).obj X.presheaf).obj (Opposite.op U)) : Type u))
Tactic: apply TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis
    (hB := (Y.isBasis_affineOpens.of_isInducing f.imageι.isEmbedding.isInducing))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y_1 : Scheme
f : X ⟶ Y_1
U : (↑Y_1.affineOpens : Type u)
Y : Scheme
x x_1 : (Over Y)ᵒᵖ
x_2 : x ⟶ x_1
⊢ Eq (α :=
    Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1) ⟶
      Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x))
    (Quiver.Hom.unop
        ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x_2 ≫
          Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x_1).hom) ⋯)) :
      Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1) ⟶
        Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x))
    (Quiver.Hom.unop
        (Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x).hom) ⋯) ≫
          CategoryTheory.Functor.map (𝟭 (Over Y)ᵒᵖ) x_2) :
      Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1) ⟶
        Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x))
have h : Eq (α :=
  (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
    (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
  (Over.Hom.left
      (Quiver.Hom.unop
        ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x_2 ≫
          Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x_1).hom) sorry))) :
    (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
      (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
  (Over.Hom.left
      (Quiver.Hom.unop
        (Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x).hom) sorry) ≫
          CategoryTheory.Functor.map (𝟭 (Over Y)ᵒᵖ) x_2)) :
    (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
      (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y_1 : Scheme
f : X ⟶ Y_1
U : (↑Y_1.affineOpens : Type u)
Y : Scheme
I : Y.IdealSheafData
⊢ Quiver.Hom.unop
      ((subschemeFunctor Y).rightOp.map
          ({ app := fun (I : Y.IdealSheafData) ↦ eqToHom ⋯, naturality := ⋯ :
                NatTrans (𝟭 Y.IdealSheafData) ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor) }.app
            I) ≫
        NatTrans.app
          { app := fun (f : (Over Y)ᵒᵖ) ↦ Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯),
            naturality := ⋯ }
          ((subschemeFunctor Y).rightOp.obj I)) =
    Quiver.Hom.unop (𝟙 ((subschemeFunctor Y).rightOp.obj I))
have h : Over.Hom.left
    (Quiver.Hom.unop
      ((subschemeFunctor Y).rightOp.map
          ({ app := fun (I : Y.IdealSheafData) ↦ eqToHom sorry, naturality := sorry :
                NatTrans (𝟭 Y.IdealSheafData) ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor) }.app
            I) ≫
        NatTrans.app
          { app := fun (f : (Over Y)ᵒᵖ) ↦ Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop f).hom) sorry),
            naturality := sorry }
          ((subschemeFunctor Y).rightOp.obj I))) =
  Over.Hom.left (Quiver.Hom.unop (𝟙 ((subschemeFunctor Y).rightOp.obj I)))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥X
⊢ IsOpenImmersion f
have hf : Topology.IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
Tactic: apply +allowSynthFailures IsOpenImmersion.of_isIso_stalkMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥X
hf : Topology.IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsOpenImmersion f
have inst : ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Tactic: apply +allowSynthFailures IsOpenImmersion.of_isIso_stalkMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
⊢ IsIso f
have this : IsEmpty.{u_1 + 1} ↥X
Tactic: haveI : IsEmpty X := f.base.hom.1.isEmpty
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
this : IsEmpty.{u_1 + 1} ↥X
⊢ Epi f.base
have rw : Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
Tactic: rw [TopCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
this : IsEmpty.{u_1 + 1} ↥X
⊢ IsIso f
have this₁ : Epi f.base
Tactic: have : Epi f.base := by
    rw [TopCat.epi_iff_surjective]; rintro (x : Y)
    exact isEmptyElim x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X : Scheme
inst : IsEmpty.{u_1 + 1} ↥X
U : X.Opens
⊢ Subsingleton.{u_1 + 1} (↑Γ(X, U) : Type u_1)
have obtain : Subsingleton.{u_1 + 1} (↑Γ(X, ⊥) : Type u_1)
Tactic: obtain rfl : U = ⊥ := Subsingleton.elim _ _
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
h : Nonempty.{u + 1} ↥X
⊢ IsAffine X
have inr : ∀ (x : ↥X), IsAffine X
Tactic: obtain ⟨x⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
⊢ IsAffine X
have inr : ∀ (U : Opens ↥X) (hU : IsAffine.{u} (↑U : Scheme)) (hxU : x ∈ (↑U : Set ↥X)), IsAffine X
Tactic: obtain ⟨_, ⟨U, hU : IsAffine _, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (a := x) (by trivial) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine.{u} (↑U : Scheme)
hxU : x ∈ (↑U : Set ↥X)
⊢ U = ⊤
have h : ∀ (y : ↥X), y ∈ (↑U : Set ↥X) ↔ y ∈ (↑⊤ : Set ↥X)
Tactic: ext y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine.{u} (↑U : Scheme)
hxU : x ∈ (↑U : Set ↥X)
⊢ IsAffine X
have hU₁ : IsAffine.{u} (↑⊤ : Scheme)
Tactic: obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]
Cleared hypotheses: U, hU, hxU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine.{u} (↑U : Scheme)
hxU : x ∈ (↑U : Set ↥X)
hU₁ : IsAffine.{u} (↑⊤ : Scheme)
⊢ IsAffine X
have hxU₁ : x ∈ (↑⊤ : Set ↥X)
Tactic: obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]
Cleared hypotheses: U, hU, hxU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
⊢ IsAffine X
have x : IsEmpty.{u + 1} ↥X ∨ Nonempty.{u + 1} ↥X
Tactic: cases isEmpty_or_nonempty X with
  | inl h => infer_instance
  | inr h =>
  obtain ⟨x⟩ := h
  obtain ⟨_, ⟨U, hU : IsAffine _, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (a := x) (by trivial) isOpen_univ
  obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]
  exact .of_isIso (Scheme.topIso X).inv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ↔
    Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y)
have refine_1 : (∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(Functor.obj (Discrete.functor g) k)),
    (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
      (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y) →
  Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y)
Tactic: refine (Scheme.IsLocallyDirected.ι_eq_ι_iff _).trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
refine_1 :
  (∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(Functor.obj (Discrete.functor g) k)),
      (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
        (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y) →
    Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y)
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ↔
    Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y)
have refine_2 : Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y) →
  ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(Functor.obj (Discrete.functor g) k)),
    (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
      (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y
Tactic: refine (Scheme.IsLocallyDirected.ι_eq_ι_iff _).trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y) →
    ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(Functor.obj (Discrete.functor g) k)),
      (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
        (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y
have refine_2 : i = j ∧ x ≍ y →
  ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(g k.as)),
    (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
      (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y
Tactic: simp only [Discrete.functor_obj_eq_as, Sigma.mk.injEq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i : σ
x y : ↥(g i)
e : x ≍ y
⊢ ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := i }) (x_1 : ↥(g k.as)),
    (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
      (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y
have refine_2 : ∀ (e : x ≍ x),
  ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := i }) (x_1 : ↥(g k.as)),
    (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
      (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = x
Tactic: obtain rfl := (heq_eq_eq x y).mp e
Cleared hypotheses: y, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(∐ g)
hx : x ∈ U
⊢ Membership.mem (γ := Opens ↥(∐ g)) ⊥ x
have obtain : ∀ (x : ↥(g i)) (hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))),
  Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))
Tactic: obtain ⟨x, rfl⟩ := hU hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
⊢ Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))
have obtain : ∀ (y : ↥(g j)) (hy : Eq (α := ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))),
  Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))
Tactic: obtain ⟨y, hy⟩ := hU' hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
y : ↥(g j)
hy : Eq (α := ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))
⊢ Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))
have h₁ : i ≠ i
Tactic: obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy
Cleared hypotheses: j, h, hU', y, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
y : ↥(g j)
hy : Eq (α := ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))
h₁ : i ≠ i
hU'₁ : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
⊢ Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))
have hy₁ : Eq (α := ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))
Tactic: obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy
Cleared hypotheses: j, h, hU', y, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
⊢ IsEmpty.{u + 1} ↥Z
have refine : ∀ (z : ↥Z), False
Tactic: refine ⟨fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ False
have x : ↥(∐ g)
Tactic: fapply eq_bot_iff.mp <| disjoint_iff.mp <| disjoint_opensRange_sigmaι g i j hij
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
x : ↥(∐ g)
⊢ False
have a₁ : Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g))
  (Scheme.Hom.opensRange (Sigma.ι g i) ⊓ Scheme.Hom.opensRange (Sigma.ι g j)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))
Tactic: fapply eq_bot_iff.mp <| disjoint_iff.mp <| disjoint_opensRange_sigmaι g i j hij
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g j) (b z : ↥(g j)) : ↥(∐ g)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))
have rw : Eq (α := ↥(∐ g)) ((b ≫ Sigma.ι g j) z : ↥(∐ g)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))
Tactic: rw [← Scheme.Hom.comp_apply, h.w]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
rw : Eq (α := ↥(∐ g)) ((b ≫ Sigma.ι g j) z : ↥(∐ g)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g j) (b z : ↥(g j)) : ↥(∐ g)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))
have rw₁ : Eq (α := ↥(∐ g)) ((b ≫ Sigma.ι g j) z : ↥(∐ g)) ((b ≫ Sigma.ι g j) z : ↥(∐ g))
Tactic: rw [← Scheme.Hom.comp_apply, h.w]