-- 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
i : (x : ↥c.pt) → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), Membership.mem (α := ↥(D.obj (i x))) (U x) ((c.π.app (i x)) x : ↥(D.obj (i x)))
t : (x : ↥c.pt) → (↑Γ(D.obj (i x), U x) : Type u)
ht :
  ∀ (x : ↥c.pt),
    Eq (α := (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x)) (Scheme.Hom.app (c.π.app (i x)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
          (t x) :
        (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app (i x) ⁻¹ᵁ U x) ⋯ :
        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 x) ⁻¹ᵁ U x))))
j : (x y : ↥c.pt) → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    Eq (α :=
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        ((D.obj (j x y)).presheaf.obj (Opposite.op (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj (i x), U x)) (Scheme.Hom.app (D.map (fjx x y)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(D.obj (j x y), D.map (fjx x y) ⁻¹ᵁ U x) : Type u))
          (t x))
        (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y) ⋯)
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj (i y), U y)) (Scheme.Hom.app (D.map (fjy x y)) (U y)) :
            (a : (↑Γ(D.obj (i y), U y) : Type u)) → (↑Γ(D.obj (j x y), D.map (fjy x y) ⁻¹ᵁ U y) : Type u))
          (t y))
        (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y) ⋯)
σ : Finset ↥c.pt
hσ : Eq.{u + 1} (α := Set ↥c.pt) (⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U x).carrier) ⊤
σi : (x : ↥c.pt) → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi :
  ∀ (x : ↥c.pt),
    Membership.mem (γ := Set ↥c.pt)
      (TopologicalSpace.Opens.carrier (c.π.app (i (σi x)) ⁻¹ᵁ U (σi x)) :
        Set ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) (i (σi x))))
      x
S : Finset I := Finset.image i σ ∪ Finset.image₂ j σ σ
hiS : ∀ {x : ↥c.pt} (hx : x ∈ σ), i x ∈ S
hjS : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), j x y ∈ S
k : I
fk : {X : I} → X ∈ S → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ S) (mY : Y ∈ S) {f : X ⟶ Y},
    Membership.mem (γ := Finset ((X : I) ×' (Y : I) ×' (_ : X ∈ S) ×' (_ : Y ∈ S) ×' (X ⟶ Y)))
        (Finset.image₂
            (fun (x y : ↥σ) ↦
              PSigma.mk (β := fun (X : I) ↦ (Y : I) ×' (_ : X ∈ S) ×' (_ : Y ∈ S) ×' (X ⟶ Y))
                (j (↑x : ↥c.pt) (↑y : ↥c.pt))
                (PSigma.mk (β := fun (Y : I) ↦
                  (_ : j (↑x : ↥c.pt) (↑y : ↥c.pt) ∈ S) ×' (_ : Y ∈ S) ×' (j (↑x : ↥c.pt) (↑y : ↥c.pt) ⟶ Y))
                  (i (↑x : ↥c.pt))
                  (PSigma.mk (β := fun (x_1 : j (↑x : ↥c.pt) (↑y : ↥c.pt) ∈ S) ↦
                    (_ : i (↑x : ↥c.pt) ∈ S) ×' (j (↑x : ↥c.pt) (↑y : ↥c.pt) ⟶ i (↑x : ↥c.pt))) ⋯
                    (PSigma.mk (β := fun (x_1 : i (↑x : ↥c.pt) ∈ S) ↦ j (↑x : ↥c.pt) (↑y : ↥c.pt) ⟶ i (↑x : ↥c.pt)) ⋯
                      (fjx (↑x : ↥c.pt) (↑y : ↥c.pt))))))
            σ.attach σ.attach ∪
          Finset.image₂
            (fun (x y : ↥σ) ↦
              PSigma.mk (β := fun (X : I) ↦ (Y : I) ×' (_ : X ∈ S) ×' (_ : Y ∈ S) ×' (X ⟶ Y))
                (j (↑x : ↥c.pt) (↑y : ↥c.pt))
                (PSigma.mk (β := fun (Y : I) ↦
                  (_ : j (↑x : ↥c.pt) (↑y : ↥c.pt) ∈ S) ×' (_ : Y ∈ S) ×' (j (↑x : ↥c.pt) (↑y : ↥c.pt) ⟶ Y))
                  (i (↑y : ↥c.pt))
                  (PSigma.mk (β := fun (x_1 : j (↑x : ↥c.pt) (↑y : ↥c.pt) ∈ S) ↦
                    (_ : i (↑y : ↥c.pt) ∈ S) ×' (j (↑x : ↥c.pt) (↑y : ↥c.pt) ⟶ i (↑y : ↥c.pt))) ⋯
                    (PSigma.mk (β := fun (x_1 : i (↑y : ↥c.pt) ∈ S) ↦ j (↑x : ↥c.pt) (↑y : ↥c.pt) ⟶ i (↑y : ↥c.pt)) ⋯
                      (fjy (↑x : ↥c.pt) (↑y : ↥c.pt))))))
            σ.attach σ.attach)
        (PSigma.mk (β := fun (X : I) ↦ (Y : I) ×' (_ : X ∈ S) ×' (_ : Y ∈ S) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : I) ↦ (_ : X ∈ S) ×' (_ : Y ∈ S) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ S) ↦ (_ : Y ∈ S) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ S) ↦ X ⟶ Y) mY f)))) →
      fk mX ≫ f = fk mY
hk₁ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjx x y = fk ⋯
hk₂ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjy x y = fk ⋯
k' : I
fk'k : k' ⟶ k
hk' : D.map fk'k ⁻¹ᵁ ⨆ (x : ↥c.pt), ⨆ (hx : x ∈ σ), D.map (fk ⋯) ⁻¹ᵁ U x = ⊤
this :
  ∀
    (x :
      (i_1 : ↥σ) →
        ((D.obj k').presheaf ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
          (Opposite.op (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑i_1 : ↥c.pt)))),
    Presieve.Arrows.Compatible
        ((D.obj k').presheaf ⋙
          forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
        (B := ⊤) (fun (x : ↥σ) ↦ homOfLE ⋯) x →
      ∃! t :
        (fun (X : Type u) ↦ X)
          (((D.obj k').presheaf ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier)).obj
            (Opposite.op ⊤)),
        ∀ (i_1 : ↥σ),
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (((D.obj k').presheaf ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).map
                    (Quiver.Hom.op (homOfLE ⋯))) :
                (a : (fun (X : Type u) ↦ X) (((D.obj k').presheaf ⋙ forget CommRingCat).obj (Opposite.op ⊤))) →
                  (fun (X : Type u) ↦ X)
                    (((D.obj k').presheaf ⋙ forget CommRingCat).obj
                      (Opposite.op (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑i_1 : ↥c.pt)))))
              t =
            x i_1
t₀ :
  ((D.obj k').presheaf ⋙
        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)).obj
    (Opposite.op ⊤)
ht₀ :
  ∀ (i_1 : ↥σ),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (((D.obj k').presheaf ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
          (Opposite.op (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑i_1 : ↥c.pt)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (((D.obj k').presheaf ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier)).map
                (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (fun (X : Type u) ↦ X) (((D.obj k').presheaf ⋙ forget CommRingCat).obj (Opposite.op ⊤))) →
              (fun (X : Type u) ↦ X)
                (((D.obj k').presheaf ⋙ forget CommRingCat).obj
                  (Opposite.op (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑i_1 : ↥c.pt)))))
          t₀ :
        (fun (X : Type u) ↦ X)
          (((D.obj k').presheaf ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier)).obj
            (Opposite.op (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑i_1 : ↥c.pt)))))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj (i (↑i_1 : ↥c.pt)), U (↑i_1 : ↥c.pt)))
              (Scheme.Hom.app (D.map (fk'k ≫ fk ⋯)) (U (↑i_1 : ↥c.pt))) :
            (a : (↑Γ(D.obj (i (↑i_1 : ↥c.pt)), U (↑i_1 : ↥c.pt)) : Type u)) →
              (↑Γ(D.obj k', D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑i_1 : ↥c.pt)) : Type u))
          (t (↑i_1 : ↥c.pt)) :
        (↑Γ(D.obj k', D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑i_1 : ↥c.pt)) : Type u))
y : ↥c.pt
hy : Membership.mem (γ := TopologicalSpace.Opens ↥c.pt) ⊤ y
H : c.π.app (i (σi y)) ⁻¹ᵁ U (σi y) ≤ c.π.app k' ⁻¹ᵁ D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y)
⊢ Eq (α := (↑(c.pt.presheaf.obj (Opposite.op (c.π.app (i (σi y)) ⁻¹ᵁ U (σi y)))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤)) (Y :=
            c.pt.presheaf.obj (Opposite.op (c.π.app (i (σi y)) ⁻¹ᵁ U (σi y))))
            (c.pt.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑(c.pt.presheaf.obj (Opposite.op (c.π.app (i (σi y)) ⁻¹ᵁ U (σi y)))) : Type u))
        s :
      (↑(c.pt.presheaf.obj (Opposite.op (c.π.app (i (σi y)) ⁻¹ᵁ U (σi y)))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (c.pt.presheaf.map (homOfLE H).op) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op (c.π.app k' ⁻¹ᵁ D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y)))) : Type u)) →
            (↑(c.pt.presheaf.obj (Opposite.op (c.π.app (i (σi y)) ⁻¹ᵁ U (σi y)))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj k', D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y)))
                (Scheme.Hom.app (c.π.app k') (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y))) :
              (a : (↑Γ(D.obj k', D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y)) : Type u)) →
                (↑Γ(((Functor.const I).obj c.pt).obj k', c.π.app k' ⁻¹ᵁ D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y)) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X :=
                    Γ(D.obj (i (↑⟨σi y, ⋯⟩ : ↥c.pt)),
                      U (↑(Subtype.mk (p := fun (x : ↥c.pt) ↦ x ∈ σ) (σi y) ⋯) : ↥c.pt)))
                    (Scheme.Hom.app (D.map (fk'k ≫ fk ⋯))
                      (U (↑(Subtype.mk (p := fun (x : ↥c.pt) ↦ x ∈ σ) (σi y) ⋯) : ↥c.pt))) :
                  (a : (↑Γ(D.obj (i (↑⟨σi y, ⋯⟩ : ↥c.pt)), U (↑⟨σi y, ⋯⟩ : ↥c.pt)) : Type u)) →
                    (↑Γ(D.obj k', D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑⟨σi y, ⋯⟩ : ↥c.pt)) : Type u))
                (t (↑(Subtype.mk (p := fun (x : ↥c.pt) ↦ x ∈ σ) (σi y) ⋯) : ↥c.pt)) :
              (↑Γ(D.obj k', D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (↑(Subtype.mk (p := fun (x : ↥c.pt) ↦ x ∈ σ) (σi y) ⋯) : ↥c.pt)) :
                Type u)) :
          (↑Γ(((Functor.const I).obj c.pt).obj k', c.π.app k' ⁻¹ᵁ D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y)) : Type u)) :
      (↑(c.pt.presheaf.obj (Opposite.op (c.π.app (i (σi y)) ⁻¹ᵁ U (σi y)))) : Type u))

Tactic:
(ht (σi y)).symm.trans ?_

Premises used: TopCat.Presheaf.restrict, Eq.symm, Eq.trans