-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : LocallyOfFinitePresentation f
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_5 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
𝒰 :
  IsOpenCover (X := ↥c.pt)
    fun
      (V :
        { x :
          TopologicalSpace.Opens ↥c.pt ×
            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
              x.1 ∈ X.affineOpens ∧
                x.1 ≤
                  (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                    (↑x.2 : TopologicalSpace.Opens ↥S) } //
          Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt)) c.pt.affineOpens x.1 ∧
            x.1 ≤
              (Opens.comap (TopCat.Hom.hom a.base) : (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) ↦
    (↑V :
        TopologicalSpace.Opens ↥c.pt ×
          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
            x.1 ∈ X.affineOpens ∧
              x.1 ≤
                (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }).1
i : I
s :
  Finset
    { x :
      TopologicalSpace.Opens ↥c.pt ×
        { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
          x.1 ∈ X.affineOpens ∧
            x.1 ≤
              (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                (↑x.2 : TopologicalSpace.Opens ↥S) } //
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt)) c.pt.affineOpens x.1 ∧
        x.1 ≤
          (Opens.comap (TopCat.Hom.hom a.base) : (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
            (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 :
  ∀ (j : ↥s),
    IsAffineOpen (𝒱 j) ∧
      (↑(↑j :
                { x :
                  TopologicalSpace.Opens ↥c.pt ×
                    { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                      x.1 ∈ X.affineOpens ∧
                        x.1 ≤
                          (Opens.comap (TopCat.Hom.hom f.base) :
                              (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                            (↑x.2 : TopologicalSpace.Opens ↥S) } //
                  x.1 ∈ c.pt.affineOpens ∧
                    x.1 ≤
                      (Opens.comap (TopCat.Hom.hom a.base) :
                          (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                        (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
            TopologicalSpace.Opens ↥c.pt ×
              { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                x.1 ∈ X.affineOpens ∧
                  x.1 ≤
                    (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                      (↑x.2 : TopologicalSpace.Opens ↥S) }).1 =
        c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' :
  ∀ (j : ↥s),
    D.map fi'i ⁻¹ᵁ 𝒱 j ≤
      t.app i' ⁻¹ᵁ
        (↑(↑(↑(↑j :
                          { x :
                            TopologicalSpace.Opens ↥c.pt ×
                              { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                x.1 ∈ X.affineOpens ∧
                                  x.1 ≤
                                    (Opens.comap (TopCat.Hom.hom f.base) :
                                        (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                      (↑x.2 : TopologicalSpace.Opens ↥S) } //
                            x.1 ∈ c.pt.affineOpens ∧
                              x.1 ≤
                                (Opens.comap (TopCat.Hom.hom a.base) :
                                    (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                  (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                      TopologicalSpace.Opens ↥c.pt ×
                        { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                          x.1 ∈ X.affineOpens ∧
                            x.1 ≤
                              (Opens.comap (TopCat.Hom.hom f.base) :
                                  (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
          TopologicalSpace.Opens ↥S)
𝒱' : ↥s → (D.obj i').Opens := fun (x : ↥s) ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 :
  ∀ (j : ↥s),
    c.π.app i' ⁻¹ᵁ 𝒱' j =
      (↑(↑j :
              { x :
                TopologicalSpace.Opens ↥c.pt ×
                  { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                    x.1 ∈ X.affineOpens ∧
                      x.1 ≤
                        (Opens.comap (TopCat.Hom.hom f.base) :
                            (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                          (↑x.2 : TopologicalSpace.Opens ↥S) } //
                x.1 ∈ c.pt.affineOpens ∧
                  x.1 ≤
                    (Opens.comap (TopCat.Hom.hom a.base) :
                        (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                      (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
          TopologicalSpace.Opens ↥c.pt ×
            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
              x.1 ∈ X.affineOpens ∧
                x.1 ≤
                  (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                    (↑x.2 : TopologicalSpace.Opens ↥S) }).1
h : ∀ (j : ↥s) (k : Over i'), IsAffine.{u} ((opensDiagram D i' (𝒱' j)).obj k)
t𝒱 : (j : ↥s) →
  opensDiagram D i' (𝒱' j) ⟶
    Functor.obj (Functor.const (Over i'))
      (↑(↑(↑(↑(↑j :
                            { x :
                              TopologicalSpace.Opens ↥c.pt ×
                                { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                  x.1 ∈ X.affineOpens ∧
                                    x.1 ≤
                                      (Opens.comap (TopCat.Hom.hom f.base) :
                                          (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                        (↑x.2 : TopologicalSpace.Opens ↥S) } //
                              x.1 ∈ c.pt.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom a.base) :
                                      (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                    (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                        TopologicalSpace.Opens ↥c.pt ×
                          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                            x.1 ∈ X.affineOpens ∧
                              x.1 ≤
                                (Opens.comap (TopCat.Hom.hom f.base) :
                                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                  (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                  TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
            TopologicalSpace.Opens ↥S) :
        Scheme) :=
  fun (j : ↥s) ↦
    {
      app := fun (k : Over i') ↦
        Hom.resLE (t.app k.left)
          (↑(↑(↑(↑j :
                            { x :
                              TopologicalSpace.Opens ↥c.pt ×
                                { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                  x.1 ∈ X.affineOpens ∧
                                    x.1 ≤
                                      (Opens.comap (TopCat.Hom.hom f.base) :
                                          (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                        (↑x.2 : TopologicalSpace.Opens ↥S) } //
                              x.1 ∈ c.pt.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom a.base) :
                                      (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                    (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                        TopologicalSpace.Opens ↥c.pt ×
                          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                            x.1 ∈ X.affineOpens ∧
                              x.1 ≤
                                (Opens.comap (TopCat.Hom.hom f.base) :
                                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                  (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                  TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
            TopologicalSpace.Opens ↥S)
          (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯,
      naturality := ⋯ }
this :
  ∀ (j : ↥s),
    IsAffine.{u}
      (↑(↑(↑(↑j :
                        { x :
                          TopologicalSpace.Opens ↥c.pt ×
                            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                              x.1 ∈ X.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom f.base) :
                                      (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                    (↑x.2 : TopologicalSpace.Opens ↥S) } //
                          x.1 ∈ c.pt.affineOpens ∧
                            x.1 ≤
                              (Opens.comap (TopCat.Hom.hom a.base) :
                                  (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                    TopologicalSpace.Opens ↥c.pt ×
                      { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                        x.1 ∈ X.affineOpens ∧
                          x.1 ≤
                            (Opens.comap (TopCat.Hom.hom f.base) :
                                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                              (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
              TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 :
        Scheme)
j : ↥s
w :
  ∀ (k : Over i'),
    Eq (α :=
      Functor.obj
          (Functor.obj (Functor.const (Over i')) (Cone.pt (F := opensDiagram D i' (𝒱' j)) (opensCone D c i' (𝒱' j))))
          k ⟶
        Functor.obj
          (Functor.obj (Functor.const (Over i'))
            (↑(↑(↑(↑(↑j :
                                  { x :
                                    TopologicalSpace.Opens ↥c.pt ×
                                      { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                        x.1 ∈ X.affineOpens ∧
                                          x.1 ≤
                                            (Opens.comap (TopCat.Hom.hom f.base) :
                                                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                              (↑x.2 : TopologicalSpace.Opens ↥S) } //
                                    x.1 ∈ c.pt.affineOpens ∧
                                      x.1 ≤
                                        (Opens.comap (TopCat.Hom.hom a.base) :
                                            (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                          (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                              TopologicalSpace.Opens ↥c.pt ×
                                { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                  x.1 ∈ X.affineOpens ∧
                                    x.1 ≤
                                      (Opens.comap (TopCat.Hom.hom f.base) :
                                          (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                        (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                        TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
                  TopologicalSpace.Opens ↥S) :
              Scheme))
          k)
      (NatTrans.app (Cone.π (opensCone D c i' (𝒱' j)) ≫ t𝒱 j) k)
      (NatTrans.app
        (CategoryTheory.Functor.map (Functor.const (Over i'))
          (Hom.resLE a
              (↑(↑(↑j :
                            { x :
                              TopologicalSpace.Opens ↥c.pt ×
                                { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                  x.1 ∈ X.affineOpens ∧
                                    x.1 ≤
                                      (Opens.comap (TopCat.Hom.hom f.base) :
                                          (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                        (↑x.2 : TopologicalSpace.Opens ↥S) } //
                              x.1 ∈ c.pt.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom a.base) :
                                      (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                    (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                        TopologicalSpace.Opens ↥c.pt ×
                          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                            x.1 ∈ X.affineOpens ∧
                              x.1 ≤
                                (Opens.comap (TopCat.Hom.hom f.base) :
                                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                  (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                  TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1
              (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯ ≫
            Hom.resLE f
              (↑(↑(↑(↑j :
                                { x :
                                  TopologicalSpace.Opens ↥c.pt ×
                                    { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                      x.1 ∈ X.affineOpens ∧
                                        x.1 ≤
                                          (Opens.comap (TopCat.Hom.hom f.base) :
                                              (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                            (↑x.2 : TopologicalSpace.Opens ↥S) } //
                                  x.1 ∈ c.pt.affineOpens ∧
                                    x.1 ≤
                                      (Opens.comap (TopCat.Hom.hom a.base) :
                                          (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                        (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                            TopologicalSpace.Opens ↥c.pt ×
                              { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                x.1 ∈ X.affineOpens ∧
                                  x.1 ≤
                                    (Opens.comap (TopCat.Hom.hom f.base) :
                                        (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                      (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                      TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
                TopologicalSpace.Opens ↥S)
              (↑(↑(↑j :
                            { x :
                              TopologicalSpace.Opens ↥c.pt ×
                                { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                  x.1 ∈ X.affineOpens ∧
                                    x.1 ≤
                                      (Opens.comap (TopCat.Hom.hom f.base) :
                                          (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                        (↑x.2 : TopologicalSpace.Opens ↥S) } //
                              x.1 ∈ c.pt.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom a.base) :
                                      (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                    (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                        TopologicalSpace.Opens ↥c.pt ×
                          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                            x.1 ∈ X.affineOpens ∧
                              x.1 ≤
                                (Opens.comap (TopCat.Hom.hom f.base) :
                                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                  (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                  TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1
              ⋯))
        k)
⊢ Eq (α :=
    Quiver.Hom (V := Over i' ⥤ Scheme)
      (Functor.obj (Functor.const (Over i')) (Cone.pt (F := opensDiagram D i' (𝒱' j)) (opensCone D c i' (𝒱' j))))
      (Functor.obj (Functor.const (Over i'))
        (↑(↑(↑(↑(↑j :
                              { x :
                                TopologicalSpace.Opens ↥c.pt ×
                                  { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                    x.1 ∈ X.affineOpens ∧
                                      x.1 ≤
                                        (Opens.comap (TopCat.Hom.hom f.base) :
                                            (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                          (↑x.2 : TopologicalSpace.Opens ↥S) } //
                                x.1 ∈ c.pt.affineOpens ∧
                                  x.1 ≤
                                    (Opens.comap (TopCat.Hom.hom a.base) :
                                        (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                      (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                          TopologicalSpace.Opens ↥c.pt ×
                            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                              x.1 ∈ X.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom f.base) :
                                      (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                    (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                    TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
              TopologicalSpace.Opens ↥S) :
          Scheme)))
    (Cone.π (opensCone D c i' (𝒱' j)) ≫ t𝒱 j)
    (CategoryTheory.Functor.map (Functor.const (Over i'))
      (Hom.resLE a
          (↑(↑(↑j :
                        { x :
                          TopologicalSpace.Opens ↥c.pt ×
                            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                              x.1 ∈ X.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom f.base) :
                                      (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                    (↑x.2 : TopologicalSpace.Opens ↥S) } //
                          x.1 ∈ c.pt.affineOpens ∧
                            x.1 ≤
                              (Opens.comap (TopCat.Hom.hom a.base) :
                                  (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                    TopologicalSpace.Opens ↥c.pt ×
                      { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                        x.1 ∈ X.affineOpens ∧
                          x.1 ≤
                            (Opens.comap (TopCat.Hom.hom f.base) :
                                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                              (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
              TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1
          (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯ ≫
        Hom.resLE f
          (↑(↑(↑(↑j :
                            { x :
                              TopologicalSpace.Opens ↥c.pt ×
                                { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                                  x.1 ∈ X.affineOpens ∧
                                    x.1 ≤
                                      (Opens.comap (TopCat.Hom.hom f.base) :
                                          (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                        (↑x.2 : TopologicalSpace.Opens ↥S) } //
                              x.1 ∈ c.pt.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom a.base) :
                                      (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                    (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                        TopologicalSpace.Opens ↥c.pt ×
                          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                            x.1 ∈ X.affineOpens ∧
                              x.1 ≤
                                (Opens.comap (TopCat.Hom.hom f.base) :
                                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                  (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
                  TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
            TopologicalSpace.Opens ↥S)
          (↑(↑(↑j :
                        { x :
                          TopologicalSpace.Opens ↥c.pt ×
                            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                              x.1 ∈ X.affineOpens ∧
                                x.1 ≤
                                  (Opens.comap (TopCat.Hom.hom f.base) :
                                      (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                                    (↑x.2 : TopologicalSpace.Opens ↥S) } //
                          x.1 ∈ c.pt.affineOpens ∧
                            x.1 ≤
                              (Opens.comap (TopCat.Hom.hom a.base) :
                                  (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                                (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
                    TopologicalSpace.Opens ↥c.pt ×
                      { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                        x.1 ∈ X.affineOpens ∧
                          x.1 ≤
                            (Opens.comap (TopCat.Hom.hom f.base) :
                                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                              (↑x.2 : TopologicalSpace.Opens ↥S) }).2 :
              TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1
          ⋯))

Tactic:
ext k