-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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)
n :
  (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
    Type)
⊢ Continuous (Y :=
    (↑(Set.preimage (β :=
          (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))
            ℕ∪{∞})
          (⇑(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))
                (π ≫ snd S ℕ∪{∞})) :
            (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))
                ℕ∪{∞})
          {n}) :
      Type))
    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
have refine : Continuous (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))
  (Subtype.val (p :=
    fun
      (x :
        (x : OnePoint ℕ) →
          (↑(Set.preimage (β := OnePoint ℕ)
                (Function.comp (β :=
                  (↑(S.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type) ×
                    OnePoint ℕ)
                  Prod.snd
                  (⇑(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 ⊗ ℕ∪{∞})))
                {x}) :
            Type)) ↦
    Membership.mem (γ :=
      Set
        ((x : OnePoint ℕ) →
          (↑(Set.preimage (β := OnePoint ℕ)
                (Function.comp (β :=
                  (↑(S.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type) ×
                    OnePoint ℕ)
                  Prod.snd
                  (⇑(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 ⊗ ℕ∪{∞})))
                {x}) :
            Type)))
      (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 ⊗ ℕ∪{∞})))
      x))
Tactic: refine (continuous_apply _).comp ?_