-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
⊢ Continuous (X :=
    (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type) ⊕
      (↑((pullback (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) (X :=
                LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})) (Y := LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
                (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)).toTop
            (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type))
    (Y :=
    { x :
      (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type) ×
        (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type) //
      Eq (α :=
        (↑((tensorObj (𝒞 :=
                  CompHausLike.category fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                  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))
                π :
              (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type))
            x.1 :
          (↑((tensorObj (𝒞 :=
                    CompHausLike.category fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                    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))
                π :
              (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type))
            x.2 :
          (↑((tensorObj (𝒞 :=
                    CompHausLike.category fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                    S ℕ∪{∞}).toTop
                (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type)) })
    (Sum.elim
      (fun
          (t :
            (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type)) ↦
        Subtype.mk (p :=
          fun
            (xy :
              (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type) ×
                (↑(T.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) ×
              Option ℕ)
            ((π.hom.hom' : (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type)) xy.1 :
              (↑((tensorObj (𝒞 :=
                        CompHausLike.category fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                        S ℕ∪{∞}).toTop
                    (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type))
            ((π.hom.hom' : (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type)) xy.2 :
              (↑((tensorObj (𝒞 :=
                        CompHausLike.category fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                        S ℕ∪{∞}).toTop
                    (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type)))
          (t, t) ⋯)
      fun
        (xy :
          { xy :
            (↑((LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type) ×
              (↑((LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).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) ×
                Option ℕ)
              ((π.hom.hom' : (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type))
                  ((TopCat.Hom.hom' (InducedCategory.Hom.hom (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) :
                        (a : (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type)) → (↑T.toTop : Type))
                      xy.1 :
                    (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type)) :
                (↑((tensorObj (𝒞 :=
                          CompHausLike.category fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                          S ℕ∪{∞}).toTop
                      (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
              ((π.hom.hom' : (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type))
                  ((TopCat.Hom.hom' (InducedCategory.Hom.hom (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) :
                        (a : (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type)) → (↑T.toTop : Type))
                      xy.2 :
                    (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type)) :
                (↑((tensorObj (𝒞 :=
                          CompHausLike.category fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                          S ℕ∪{∞}).toTop
                      (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type)) }) ↦
      Subtype.mk (p :=
        fun
          (xy :
            (↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type) ×
              (↑(T.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) ×
            Option ℕ)
          ((π.hom.hom' : (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type)) xy.1 :
            (↑((tensorObj (𝒞 :=
                      CompHausLike.category fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                      S ℕ∪{∞}).toTop
                  (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type))
          ((π.hom.hom' : (a : (↑T.toTop : Type)) → (↑(S ⊗ ℕ∪{∞}).toTop : Type)) xy.2 :
            (↑((tensorObj (𝒞 :=
                      CompHausLike.category fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                      S ℕ∪{∞}).toTop
                  (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type)))
        ((TopCat.Hom.hom' (InducedCategory.Hom.hom (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) :
              (a : (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type)) → (↑T.toTop : Type))
            (↑xy :
                (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type) ×
                  (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type)).1,
          (TopCat.Hom.hom' (InducedCategory.Hom.hom (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) :
              (a : (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type)) → (↑T.toTop : Type))
            (↑xy :
                (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type) ×
                  (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type)).2)
        ⋯)

Tactic:
fun_prop