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
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 : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  Eq (α := (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier)
            (Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯)) :
          (a : (↑Γ((↑(D.map (𝟙 i) ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) → (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj i, U)) (Y := Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤))
                ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
            s :
          (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u)) :
      (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
    (0 : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
⊢ Eq (α := (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (D.map (Over.Hom.left f)) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
have hf' : Over.Hom.left f = j.hom
Tactic: have hf' : f.left = j.hom := by simpa using Over.w 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 : I), IsAffine.{u} (D.obj i)
s : (↑Γ(c.pt, ⊤) : Type u)
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
have dsimp : ∀ (i : Iᵒᵖ), IsAffine.{u} (D.obj (Opposite.unop i))
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 : I), IsAffine.{u} (D.obj i)
s : (↑Γ(c.pt, ⊤) : Type u)
⊢ ∃ (i : I) (t : (↑Γ(D.obj i, ⊤) : Type u)),
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        t =
      s
have this : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
Tactic: have : ∀ i, IsAffine (D.op.obj i).unop := by dsimp; infer_instance
-- 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 : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
⊢ ∃ (i : I) (t : (↑Γ(D.obj i, ⊤) : Type u)),
    s =
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        t
have this : CompactSpace.{u} ↥c.pt
Tactic: have := Scheme.compactSpace_of_isLimit _ _ 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
x : ↥c.pt
⊢ ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
    Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
    Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
have have : ∀ (i : I),
  ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
    Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
    Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) sorry :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
Tactic: have i := IsCofiltered.nonempty (C := I).some
-- 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
⊢ ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
    Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
    Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
have obtain : ∀ (U : TopologicalSpace.Opens ↥(D.obj i)) (hU : IsAffineOpen U)
  (hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))),
  ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
    Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
    Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) sorry :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
Tactic: obtain ⟨_, ⟨U, hU : IsAffineOpen U, rfl⟩, hxU, -⟩ :=
      (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open
        (Set.mem_univ ((c.π.app i).base 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
⊢ ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
    Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
    Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
have this₁ : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
Tactic: have (j : Over i) : IsAffine ((opensDiagram D i U).obj j) := hU.preimage (D.map _)
-- 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
t : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)
hj :
  Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensCone D c i U).π.app j)) :
          (a : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
        t :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))))
⊢ ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
    Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
    Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
have refine_1 : Membership.mem (α := ↥(D.obj j.left)) ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) ((c.π.app j.left) x : ↥(D.obj j.left))
Tactic: refine ⟨j.left, (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤, by simpa using hU.preimage (D.map _), ?_, t, ?_⟩
-- 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
t : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)
hj :
  Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensCone D c i U).π.app j)) :
          (a : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
        t :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))))
⊢ Membership.mem (α := ↥(D.obj j.left)) ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) ((c.π.app j.left) x : ↥(D.obj j.left))
have refine_1 : Membership.mem (α := ↥(D.obj i)) U ((c.π.app j.left ≫ D.map j.hom) x : ↥(D.obj i))
Tactic: suffices (c.π.app j.1 ≫ D.map j.hom).base x ∈ U by simpa [-Cone.w] using this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
t : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)
hj :
  Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensCone D c i U).π.app j)) :
          (a : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
        t :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))))
⊢ Membership.mem (α := ↥(D.obj i)) U ((c.π.app j.left ≫ D.map j.hom) x : ↥(D.obj i))
have refine_1 : Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))
Tactic: rwa [Cone.w]
-- 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 : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
t : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)
hj :
  Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensCone D c i U).π.app j)) :
          (a : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
        t :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))))
⊢ Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(D.obj j.left, (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)) (Y :=
            Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))
            (Scheme.Hom.app (c.π.app j.left) ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)) :
          (a : (↑Γ(D.obj j.left, (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u)) →
            (↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
        t :
      (↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))))
have H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
Tactic: have H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤ := by
        simp [← Scheme.Hom.comp_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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
⊢ ∃ (i : I) (t : (↑Γ(D.obj i, ⊤) : Type u)),
    s =
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        t
have this₁ : ∀ (x : ↥c.pt),
  ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
    Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
    Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) sorry :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
Tactic: have (x : c.pt) : ∃ (i : I) (U : (D.obj i).Opens) (hU : IsAffineOpen U)
      (hU : (c.π.app i).base x ∈ U) (t : Γ(D.obj i, U)), (c.π.app i).app U t = s |_ _ := by
    have i := IsCofiltered.nonempty (C := I).some
    obtain ⟨_, ⟨U, hU : IsAffineOpen U, rfl⟩, hxU, -⟩ :=
      (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open
        (Set.mem_univ ((c.π.app i).base x)) isOpen_univ
    have (j : Over i) : IsAffine ((opensDiagram D i U).obj j) := hU.preimage (D.map _)
    obtain ⟨j, t, hj⟩ := exists_appTop_π_eq_of_isAffine_of_isLimit _ _
      (isLimitOpensCone D c hc i U) (s |_ _)
    refine ⟨j.left, (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤, by simpa using hU.preimage (D.map _), ?_, t, ?_⟩
    · suffices (c.π.app j.1 ≫ D.map j.hom).base x ∈ U by simpa [-Cone.w] using this
      rwa [Cone.w]
    · have H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤ := by
        simp [← Scheme.Hom.comp_preimage]
      convert! congr(c.pt.presheaf.map (homOfLE H).op $hj)
      · convert! ConcreteCategory.comp_apply _ _ _
        congr
        simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
      · dsimp [TopCat.Presheaf.restrictOpen, TopCat.Presheaf.restrict]
        change _ = (c.pt.presheaf.map (homOfLE _).op ≫ c.pt.presheaf.map (homOfLE _).op) s
        rw [← Functor.map_comp]
        rfl