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)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s t : (↑Γ(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))
    ((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))
⊢ 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 - t) :
      (↑Γ(((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))

Tactic:
simpa +instances [map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero
-- 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)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s t : (↑Γ(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))
    ((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))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map 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 f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(D.obj j, D.map 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 f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          t :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))

Tactic:
simpa [sub_eq_zero] using exists_app_map_eq_zero_of_isLimit _ _ hc hU (s - t)
    (by simpa +instances [map_sub, sub_eq_zero])

Premises used: sub_eq_zero, HSub.hSub, AlgebraicGeometry.exists_app_map_eq_zero_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 : I), IsAffine.{u} (D.obj i)
s : (↑Γ(c.pt, ⊤) : Type u)
dsimp : ∀ (i : Iᵒᵖ), IsAffine.{u} (D.obj (Opposite.unop i))
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))

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 : I), IsAffine.{u} (D.obj i)
s : (↑Γ(c.pt, ⊤) : Type u)
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (D.obj (Opposite.unop i))

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 : I), IsAffine.{u} (D.obj i)
s : (↑Γ(c.pt, ⊤) : Type u)
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))

Tactic:
have : ∀ i, IsAffine (D.op.obj i).unop := 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 : I), IsAffine.{u} (D.obj i)
s : (↑Γ(c.pt, ⊤) : Type u)
this : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
⊢ ∃ (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

Tactic:
⟨_, (Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (Scheme.Γ ⋙ forget _) hc.op) s).choose_spec⟩

Premises used: Exists.choose_spec, CategoryTheory.Limits.IsLimit.op, AlgebraicGeometry.Scheme.Γ, CategoryTheory.Functor.comp, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, Exists.intro, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves
-- 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 : I), IsAffine.{u} (D.obj i)
s : (↑Γ(c.pt, ⊤) : Type u)
this : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
⊢ ∃ (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

Tactic:
exact ⟨_, (Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (Scheme.Γ ⋙ forget _) hc.op) s).choose_spec⟩
-- 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
⊢ CompactSpace.{u} ↥c.pt

Tactic:
have := Scheme.compactSpace_of_isLimit _ _ 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)
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
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) ⋯ :
          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))))
⊢ ∃ (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))))

Tactic:
have i := IsCofiltered.nonempty (C := I).some
-- 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)
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
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) ⋯ :
          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))))
⊢ ∃ (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))))

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

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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)
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))
⊢ ∀ (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 _)
-- 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)
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 ⊤))))))
⊢ IsAffineOpen ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)

Tactic:
simpa using hU.preimage (D.map _)

Premises used: CategoryTheory.Functor.map, 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)
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_2 : ∀ (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 ⊤))))))
this : Membership.mem (α := ↥(D.obj i)) U ((c.π.app j.left ≫ D.map j.hom) x : ↥(D.obj i))
⊢ Membership.mem (α := ↥(D.obj j.left)) ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) ((c.π.app j.left) x : ↥(D.obj j.left))

Tactic:
simpa [-Cone.w] using this

Premises used: CategoryTheory.Limits.Cone.w
-- 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)
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 ⊤))))))
refine_1 : Membership.mem (α := ↥(D.obj i)) U ((c.π.app j.left ≫ D.map j.hom) x : ↥(D.obj i))
⊢ Membership.mem (α := ↥(D.obj j.left)) ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) ((c.π.app j.left) x : ↥(D.obj j.left))

Tactic:
suffices (c.π.app j.1 ≫ D.map j.hom).base x ∈ U by simpa [-Cone.w] using this
-- 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)
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 ⊤))))))
refine_1 refine_1₁ refine_1₂ refine_1₃ : Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))
⊢ Membership.mem (α := ↥(D.obj i)) U ((c.π.app j.left ≫ D.map j.hom) x : ↥(D.obj i))

Tactic:
rwa [Cone.w]

Premises used: CategoryTheory.Limits.Cone.w
-- 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)
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 ⊤))))))
⊢ 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)
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 ⊤))))))
⊢ 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]