-- 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π'_1 : 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)
this_1 : Mono (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})) (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this_2 :
  Nonempty
    (↑((LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this_3 : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet
    (pullback.cone (P := fun (X : TopCat.{0}) ↦
      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π' π')
    (pullback.isLimit (P := fun (X : TopCat.{0}) ↦
      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π' π')
hc :
  Limits.IsColimit (C := LightCondMod R) (F := Limits.parallelPair hπ'.left hπ'.right ⋙ free R)
    (mapCocone (free R) (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
this :
  Eq (α :=
    LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}) ⟶
      tensorObj (𝒞 :=
        CompHausLike.category fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        S' ℕ∪{∞})
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π')
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
      π' ≫
        fst S' ℕ∪{∞} ≫
          lift (𝟙 S')
            (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) S' ∞))
pos :
  Eq (α := obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫
            LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
              π' ≫
                fst S' ℕ∪{∞} ≫
                  lift (𝟙 S')
                      (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) S' ∞) ≫
                    y' ▷ ℕ∪{∞}) ≫
        f :
      obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫
            LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
              π' ≫
                fst S' ℕ∪{∞} ≫
                  split.section_ ≫
                    LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
                      π' ≫
                        fst S' ℕ∪{∞} ≫
                          lift (𝟙 S')
                              (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) S' ∞) ≫
                            y' ▷ ℕ∪{∞}) ≫
        f :
      obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
pos₁ pos₂ :
  Eq (α := obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫
            LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
              π' ≫
                fst S' ℕ∪{∞} ≫
                  lift (𝟙 S')
                      (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) S' ∞) ≫
                    y' ▷ ℕ∪{∞}) ≫
        f :
      obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫
            LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
              π' ≫
                fst S' ℕ∪{∞} ≫
                  lift (𝟙 S')
                      (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) S' ∞) ≫
                    y' ▷ ℕ∪{∞}) ≫
        f :
      obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
⊢ Eq (α := obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫ LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ y' ▷ ℕ∪{∞}) ≫
        f :
      obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫
            LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
              π' ≫ fst S' ℕ∪{∞} ≫ split.section_ ≫ LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ y' ▷ ℕ∪{∞}) ≫
        f :
      obj (free R) (lightProfiniteToLightCondSet.obj T') ⟶ Y)

Tactic:
rw [reassoc_of% this, reassoc_of% split.id]

Premises used: CategoryTheory.SplitEpi.id