-- 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 ℕ∪{∞}))
this :
  cover π =
    (↑(BinaryCofan.IsColimit.desc'
          (coproductIsColimit (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 ℕ∪{∞}) ≫ π)))
          (CompHausLike.pullback.lift (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π (𝟙 T) (𝟙 T) ⋯)
          (CompHausLike.pullback.lift (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π
            (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
              LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
            (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
              LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
            ⋯)) :
      (coproductCocone T
            (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
              (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π))).pt ⟶
        CompHausLike.pullback π π)
right :
  HSub.hSub (α :=
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X)
        (CategoryTheory.Functor.map (free R)
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g)
        (CategoryTheory.Functor.map (free R)
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g) +
      CategoryTheory.Functor.map (free R)
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
              LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                r_inf ≫
                  LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                    π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
        g =
    HSub.hSub (α :=
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X)
        (CategoryTheory.Functor.map (free R)
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g)
        (CategoryTheory.Functor.map (free R)
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g) +
      CategoryTheory.Functor.map (free R)
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
              LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                r_inf ≫
                  LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                    π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
        g
⊢ HAdd.hAdd (β :=
      obj (free R)
          (lightProfiniteToLightCondSet.obj
            (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 ℕ∪{∞}) ≫ π))) ⟶
        X)
      (HSub.hSub (α :=
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X)
        (β :=
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X)
        (CategoryTheory.Functor.map (free R)
              (CategoryStruct.comp (Y :=
                lightProfiniteToLightCondSet.obj
                  (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
                (lightProfiniteToLightCondSet.map
                  (NatTrans.app
                      (Cocone.ι
                        (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 ℕ∪{∞}) ≫ π))))
                      { as := WalkingPair.right : Discrete WalkingPair } ≫
                    cover π))
                (lightProfiniteToLightCondSet.map
                  (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))) ≫
            g :
          obj (free R)
              (lightProfiniteToLightCondSet.obj
                (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 ℕ∪{∞}) ≫ π))) ⟶
            X)
        (CategoryTheory.Functor.map (free R)
              (lightProfiniteToLightCondSet.map
                  (NatTrans.app
                      (Cocone.ι
                        (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 ℕ∪{∞}) ≫ π))))
                      { as := WalkingPair.right : Discrete WalkingPair } ≫
                    cover π ≫
                      CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π) ≫
                lightProfiniteToLightCondSet.map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
            g :
          obj (free R)
              (lightProfiniteToLightCondSet.obj
                (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 ℕ∪{∞}) ≫ π))) ⟶
            X))
      (CategoryTheory.Functor.map (free R)
            (lightProfiniteToLightCondSet.map
                (NatTrans.app
                    (Cocone.ι
                      (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 ℕ∪{∞}) ≫ π))))
                    { as := WalkingPair.right : Discrete WalkingPair } ≫
                  cover π ≫
                    CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π) ≫
              lightProfiniteToLightCondSet.map
                (r_inf ≫
                  LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                    π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g :
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X) =
    HAdd.hAdd (β :=
      obj (free R)
          (lightProfiniteToLightCondSet.obj
            (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 ℕ∪{∞}) ≫ π))) ⟶
        X)
      (HSub.hSub (α :=
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X)
        (β :=
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X)
        (CategoryTheory.Functor.map (free R)
              (CategoryStruct.comp (Y :=
                lightProfiniteToLightCondSet.obj
                  (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
                (lightProfiniteToLightCondSet.map
                  (NatTrans.app
                      (Cocone.ι
                        (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 ℕ∪{∞}) ≫ π))))
                      { as := WalkingPair.right : Discrete WalkingPair } ≫
                    cover π))
                (lightProfiniteToLightCondSet.map
                  (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))) ≫
            g :
          obj (free R)
              (lightProfiniteToLightCondSet.obj
                (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 ℕ∪{∞}) ≫ π))) ⟶
            X)
        (CategoryTheory.Functor.map (free R)
              (lightProfiniteToLightCondSet.map
                  (NatTrans.app
                      (Cocone.ι
                        (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 ℕ∪{∞}) ≫ π))))
                      { as := WalkingPair.right : Discrete WalkingPair } ≫
                    cover π ≫
                      CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π) ≫
                lightProfiniteToLightCondSet.map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
            g :
          obj (free R)
              (lightProfiniteToLightCondSet.obj
                (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 ℕ∪{∞}) ≫ π))) ⟶
            X))
      (CategoryTheory.Functor.map (free R)
            (lightProfiniteToLightCondSet.map
                (NatTrans.app
                    (Cocone.ι
                      (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 ℕ∪{∞}) ≫ π))))
                    { as := WalkingPair.right } ≫
                  cover π ≫
                    CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π) ≫
              lightProfiniteToLightCondSet.map
                (r_inf ≫
                  LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                    π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g :
        obj (free R)
            (lightProfiniteToLightCondSet.obj
              (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 ℕ∪{∞}) ≫ π))) ⟶
          X)

Tactic:
simp only [this, pair_obj_left, const_obj_obj, pair_obj_right, BinaryCofan.IsColimit.desc'_coe,
      IsColimit.fac, BinaryCofan.mk_pt, BinaryCofan.mk_inr, ← Functor.map_comp,
      pullback.lift_fst, IsColimit.fac_assoc, assoc,
      pullback.lift_snd]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe, CompHausLike.pullback.lift_fst, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.IsColimit.fac_assoc, CompHausLike.pullback.lift_snd