awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) y : ↥(D.obj i))
h₂ :
  Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁ ∈ (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₄ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₃ :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
have e₁ : Eq (α := ↥(D.obj k.left))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
          (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
        (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
      (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₃ :
        ↥(D.map k.hom ⁻¹ᵁ U)) :
    ↥(D.obj k.left))
  ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
Tactic: obtain rfl : y = (D.map f.left).base x := congr($e)
Cleared hypotheses: y, h₁, h₂, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₂ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
      ↥(D.map k.hom ⁻¹ᵁ U))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
have h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) x : ↥(D.obj i))
Tactic: rw [← Scheme.Hom.comp_apply] at h₁
Cleared hypotheses: h₂, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁_1 : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) x : ↥(D.obj i))
h₂ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
      ↥(D.map k.hom ⁻¹ᵁ U))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
have rwa : ∀ (h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f ≫ k.hom)) x : ↥(D.obj i)))
  (h₂ :
    Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
      (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
        ↥(D.map k.hom ⁻¹ᵁ U)))
  (e :
    Eq (α := ↥(D.obj k.left))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
            (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
          (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
            ↥(D.map k.hom ⁻¹ᵁ U)) :
        ↥(D.obj k.left))
      ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))),
  x ∈ D.map j.hom ⁻¹ᵁ U
Tactic: rwa [← D.map_comp, Over.w f] at h₁
Cleared hypotheses: h₁, h₂, e
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V
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 (f := (D.map j.hom)) _ U.2 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
⊢ Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
have rw : LE.le (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) ⊤ ((c.π.app i ⁻¹ᵁ U).ι ⁻¹ᵁ c.π.app i ⁻¹ᵁ V)
Tactic: rw [Scheme.Hom.comp_preimage, ← top_le_iff]
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V
have H₁ : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
Tactic: have H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤ := by
    rw [Scheme.Hom.comp_preimage, ← top_le_iff]
    exact .trans (by simp) (Scheme.Hom.preimage_mono _ H)
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V
have obtain : ∀ (j : Over i) (fji : j ⟶ Over.mk (𝟙 i))
  (hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq sorry) ≫ U.ι) ⁻¹ᵁ V = ⊤),
  ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V
Tactic: obtain ⟨j, fji, hj⟩ := exists_map_eq_top _ _ (isLimitOpensCone D c hc i U) (i := .mk (𝟙 i))
    (((Scheme.isoOfEq _ (by simp)).hom ≫ U.ι) ⁻¹ᵁ V)
    (by simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base])
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V = ⊤
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V
have refine : D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ V
Tactic: refine ⟨j.left, j.hom, ?_⟩
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V = ⊤
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ V
have hj₁ : Eq (α := (↑(D.map j.hom ⁻¹ᵁ U) : Scheme).Opens) ((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left fji) ⁻¹ᵁ V) ⊤
Tactic: replace hj : (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map fji.left ⁻¹ᵁ V = ⊤ := by
    simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base] using hj
Cleared hypotheses: hj
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
have obtain : ∀ (j₁ : I) (fj₁i : j₁ ⟶ i) (e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V),
  ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
Tactic: obtain ⟨j₁, fj₁i, e₁⟩ := exists_map_preimage_le_map_preimage D c hc hU H.le
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
have obtain : ∀ (j₂ : I) (fj₂i : j₂ ⟶ i) (e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U),
  ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
Tactic: obtain ⟨j₂, fj₂i, e₂⟩ := exists_map_preimage_le_map_preimage D c hc hV H.ge
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
have obtain : ∀ (k : I) (fkj₁ : k ⟶ j₁) (fkj₂ : k ⟶ j₂) (e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i),
  ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
Tactic: obtain ⟨k, fkj₁, fkj₂, e⟩ := IsCofiltered.cospan fj₁i fj₂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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
have refine_1 : D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V
Tactic: refine ⟨k, fkj₁ ≫ fj₁i, le_antisymm ?_ ?_⟩
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
refine_1 : D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
have refine_2 : D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U
Tactic: refine ⟨k, fkj₁ ≫ fj₁i, le_antisymm ?_ ?_⟩
-- 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U
have refine_2 : D.map (fkj₂ ≫ fj₂i) ⁻¹ᵁ V ≤ D.map (fkj₂ ≫ fj₂i) ⁻¹ᵁ U
Tactic: rw [e]
-- 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)
⊢ TopologicalSpace.Opens.IsBasis.{u} (α := ↥c.pt)
    {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
have refine : ∀ {U : TopologicalSpace.Opens ↥c.pt} {x : ↥c.pt} (hxU : x ∈ U),
  ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
Tactic: refine TopologicalSpace.Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_
-- 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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
have obtain : ∀ (i : I),
  ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
Tactic: obtain ⟨i⟩ := IsCofiltered.nonempty (C := 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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
have obtain : ∀ (V : TopologicalSpace.Opens ↥(D.obj i)) (hV : IsAffineOpen V)
  (hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))),
  ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
Tactic: obtain ⟨_, ⟨V, hV : IsAffineOpen V, rfl⟩, hxV, -⟩ :=
    (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (c.π.app i x)) isOpen_univ
-- 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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
have this : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
Tactic: have (j : _) : IsAffine ((opensDiagram D i V).op.obj j).unop := hV.preimage _
-- 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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
have this₁ : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i V).obj j)
Tactic: have (j : _) : IsAffine ((opensDiagram D i V).obj j) := hV.preimage _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this_1 : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i V).obj j)
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
have obtain : ∀ (r : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u))
  (hrU : (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r ≤ U)
  (hxr :
    (↑(Subtype.mk (p := fun (x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)) ↦ x ∈ U) x hxU) :
        ↥(((Functor.const I).obj c.pt).obj i)) ∈
      (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r),
  ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
Tactic: obtain ⟨r, hrU, hxr⟩ := IsAffineOpen.exists_basicOpen_le
    (Scheme.isAffine_of_isLimit _ (isLimitOpensCone D c hc i V)) (V := U) ⟨x, hxU⟩ hxV
-- 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)
U : c.pt.Opens
hU : IsCompact (↑U : Set ↥c.pt)
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = U
have obtain : ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
  (hs :
    s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
  (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)),
  ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
Tactic: obtain ⟨s, hs, hsf, rfl⟩ := (isBasis_preimage_isAffineOpen D c hc).exists_finite_of_isCompact hU
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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact (↑(sSup s) : Set ↥c.pt)
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
have this : Finite.{u + 1} (↑s : Type u)
Tactic: have : Finite s := hsf