-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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))
    (coverToFun
      (⇑(TopCat.Hom.hom' (InducedCategory.Hom.hom (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})))) :
        (a : (↑(LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})).toTop : Type)) → (↑T.toTop : Type))
      π.hom.hom'.1)
have dsimp : 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) sorry)
    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)
      sorry)
Tactic: dsimp [coverToFun]