-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' :
  ¬Nonempty
      (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)
h :
  IsEmpty
    (tensorObj (𝒞 := types)
      (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)
      (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type))
h₁ :
  ∀
    (x :
      (↑(T'.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)),
    Eq (α :=
      (↑(T'.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))
              (Y := T')
              (π' ≫
                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 :=
                      fun
                        (x :
                          (↑((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)) ↦
                      h.elim (p :=
                        fun
                          (x :
                            (↑((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'.toTop (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                          Type))
                        x,
                    continuous_toFun := ⋯ }) :
            (a : (↑T'.toTop : Type)) → (↑T'.toTop : Type))
          x :
        (↑(T'.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))
              (𝟙 T') :
            (a : (↑T'.toTop : Type)) → (↑T'.toTop : Type))
          x :
        (↑(T'.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type))
⊢ π' ≫
      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 :=
            fun
              (x :
                (↑((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)) ↦
            h.elim (p :=
              fun
                (x :
                  (↑((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'.toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type))
              x,
          continuous_toFun := ⋯ } =
    𝟙 T'

Tactic:
ext x