-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
X : LightCondMod R
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst_1 :
  Epi (C := LightCondMod R) (X :=
    obj (lightProfiniteToLightCondSet ⋙ free R)
      (CompHausLike.of
        (fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        ((↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type) ⊕
          (↑((CompHausLike.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))))
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π))
g : obj (lightProfiniteToLightCondSet ⋙ free R) T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
apply :
  ∀ (j : Discrete WalkingPair),
    Eq (α :=
      obj
          (pair T
              (CompHausLike.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 ℕ∪{∞}) ≫ π)) ⋙
            lightProfiniteToLightCondSet ⋙ free R)
          j ⟶
        X)
      (CategoryStruct.comp (Y :=
        obj
          (obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F :=
              pair T
                  (CompHausLike.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 ℕ∪{∞}) ≫ π)) ⋙
                lightProfiniteToLightCondSet ⋙ free R)
              (mapCocone (lightProfiniteToLightCondSet ⋙ free R)
                (coproductCocone (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) T
                  (CompHausLike.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 ℕ∪{∞}) ≫ π))))))
          j)
        (NatTrans.app
          (Cocone.ι
            (mapCocone (lightProfiniteToLightCondSet ⋙ free R)
              (coproductCocone (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) T
                (CompHausLike.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 ℕ∪{∞}) ≫ π)))))
          j)
        (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π) ≫
          CategoryTheory.Functor.map
              (parallelPair (X :=
                  lightProfiniteToLightCondSet.obj
                    (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
                  (lightProfiniteToLightCondSet.map
                    (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
                  (lightProfiniteToLightCondSet.map
                    (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
                free R)
              WalkingParallelPairHom.left ≫
            (g -
                CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
                    (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                  g +
              CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
                  (r_inf ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                      π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                g)))
      (CategoryStruct.comp (Y :=
        obj
          (obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F :=
              pair T
                  (CompHausLike.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 ℕ∪{∞}) ≫ π)) ⋙
                lightProfiniteToLightCondSet ⋙ free R)
              (mapCocone (lightProfiniteToLightCondSet ⋙ free R)
                (coproductCocone (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) T
                  (CompHausLike.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 ℕ∪{∞}) ≫ π))))))
          j)
        (NatTrans.app
          (Cocone.ι
            (mapCocone (lightProfiniteToLightCondSet ⋙ free R)
              (coproductCocone (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) T
                (CompHausLike.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 ℕ∪{∞}) ≫ π)))))
          j)
        (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π) ≫
          CategoryTheory.Functor.map
              (parallelPair (X :=
                  lightProfiniteToLightCondSet.obj
                    (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
                  (lightProfiniteToLightCondSet.map
                    (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
                  (lightProfiniteToLightCondSet.map
                    (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
                free R)
              WalkingParallelPairHom.right ≫
            (g -
                CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
                    (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                  g +
              CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
                  (r_inf ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                      π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                g)))
⊢ Eq (α :=
    obj (lightProfiniteToLightCondSet ⋙ free R)
        (CompHausLike.of
          (fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          ((↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type) ⊕
            (↑((CompHausLike.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))) ⟶
      X)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π) ≫
      CategoryTheory.Functor.map
          (parallelPair (X :=
              lightProfiniteToLightCondSet.obj
                (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
              (lightProfiniteToLightCondSet.map
                (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
              (lightProfiniteToLightCondSet.map
                (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
            free R)
          WalkingParallelPairHom.left ≫
        (g -
            CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
                (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
              g +
          CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
              (r_inf ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                  π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
            g))
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π) ≫
      CategoryTheory.Functor.map
          (parallelPair (X :=
              lightProfiniteToLightCondSet.obj
                (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
              (lightProfiniteToLightCondSet.map
                (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
              (lightProfiniteToLightCondSet.map
                (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
            free R)
          WalkingParallelPairHom.right ≫
        (g -
            CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
                (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
              g +
          CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
              (r_inf ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                  π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
            g))

Tactic:
apply (isColimitOfPreserves (lightProfiniteToLightCondSet ⋙ free R)
      (coproductIsColimit _ _)).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Functor.comp, CompHausLike.coproductIsColimit, lightProfiniteToLightCondSet, LightCondensed.free, CategoryTheory.Limits.isColimitOfPreserves