-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst : Epi π
this :
  CompactSpace
    (↑(S'
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  T) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (S ⊗ ℕ∪{∞}))) :
      Type)
S'π : (n :
    (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)) →
  LightProfinite.of
      (↑(S'
            (⇑(ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type),
                    (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type)))
                  (CC :=
                  fun
                    (X :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type))
                  π) :
              (a :
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                      (↑X.toTop : Type))
                    T) →
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (S ⊗ ℕ∪{∞}))) :
        Type) ⟶
    LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun
      (n :
        (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type)) ↦
    {
      hom :=
        TopCat.ofHom
          {
            toFun :=
              fun
                (x :
                  (↑(S'
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π) :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                T) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (S ⊗ ℕ∪{∞}))) :
                    Type)) ↦
              (↑x :
                  (x : OnePoint ℕ) →
                    (↑(Prod.snd ∘
                            (⇑(ConcreteCategory.hom π) :
                              (a :
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    T) →
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (S ⊗ ℕ∪{∞})) ⁻¹'
                          {x}) :
                      Type))
                n,
            continuous_toFun := ⋯ } }
y' : LightProfinite.of
    (↑(S'
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  T) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (S ⊗ ℕ∪{∞}))) :
      Type) ⟶
  S :=
  ConcreteCategory.ofHom (FC :=
    fun
      (x1 x2 :
        CompHausLike fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type),
      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)))
    (CC :=
    fun
      (X :
        CompHausLike fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type))
    {
      toFun :=
        y
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  T) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (S ⊗ ℕ∪{∞})),
      continuous_toFun := ⋯ }
π' : pullback (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
    (y' ▷ ℕ∪{∞}) ⟶
  tensorObj (𝒞 :=
    CompHausLike.category fun (X : TopCat.{0}) ↦
      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
    (LightProfinite.of
      (↑(S'
            (⇑(ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type),
                    (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type)))
                  (CC :=
                  fun
                    (X :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type))
                  π) :
              (a :
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                      (↑X.toTop : Type))
                    T) →
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (S ⊗ ℕ∪{∞}))) :
        Type))
    ℕ∪{∞} :=
  pullback.snd (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
    π (y' ▷ ℕ∪{∞})
n :
  (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
    Type)
h_fst :
  ∀
    (x :
      (↑((LightProfinite.of
                (↑(S'
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π) :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              T) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (S ⊗ ℕ∪{∞}))) :
                  Type)).toTop
            (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)),
    Eq (α :=
      (↑(S.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type))
      ((ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type),
                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type))
              (((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞}) :
            (a :
                (↑(LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type)).toTop :
                  Type)) →
              (↑S.toTop : Type))
          x :
        (↑(S.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type))
      ((ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type),
                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type))
              ((lift
                    (𝟙
                      (LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom (FC :=
                                    fun
                                      (x1 x2 :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type),
                                      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type)))
                                    (CC :=
                                    fun
                                      (X :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type))
                                    π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type)))
                    (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                      (LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom (FC :=
                                    fun
                                      (x1 x2 :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type),
                                      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type)))
                                    (CC :=
                                    fun
                                      (X :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type))
                                    π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type))
                      n) ≫
                  y' ▷ ℕ∪{∞}) ≫
                fst S ℕ∪{∞}) :
            (a :
                (↑(LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type)).toTop :
                  Type)) →
              (↑S.toTop : Type))
          x :
        (↑(S.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type))
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞} =
    (lift
          (𝟙
            (LightProfinite.of
              (↑(S'
                    (⇑(ConcreteCategory.hom (FC :=
                          fun
                            (x1 x2 :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type),
                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type)))
                          (CC :=
                          fun
                            (X :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type))
                          π) :
                      (a :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            T) →
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          (S ⊗ ℕ∪{∞}))) :
                Type)))
          (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            (LightProfinite.of
              (↑(S'
                    (⇑(ConcreteCategory.hom (FC :=
                          fun
                            (x1 x2 :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type),
                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type)))
                          (CC :=
                          fun
                            (X :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type))
                          π) :
                      (a :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            T) →
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          (S ⊗ ℕ∪{∞}))) :
                Type))
            n) ≫
        y' ▷ ℕ∪{∞}) ≫
      fst S ℕ∪{∞}

Tactic:
ext x