Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj 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 ℕ∪{∞}))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map (cover π) ≫
      (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
                (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
              free R).map
          WalkingParallelPairHom.left ≫
        (g - (lightProfiniteToLightCondSet ⋙ free R).map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫ g +
          (lightProfiniteToLightCondSet ⋙ free R).map
              (r_inf ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                  π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
            g) =
    (lightProfiniteToLightCondSet ⋙ free R).map (cover π) ≫
      (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
                (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
              free R).map
          WalkingParallelPairHom.right ≫
        (g - (lightProfiniteToLightCondSet ⋙ free R).map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫ g +
          (lightProfiniteToLightCondSet ⋙ free R).map
              (r_inf ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                  π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
            g)

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

Goal state after:
R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj 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 ℕ∪{∞}))
⊢ ∀ (j : Discrete WalkingPair),
    ((lightProfiniteToLightCondSet ⋙ free R).mapCocone
                (coproductCocone T
                  (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))).ι.app
          j ≫
        (lightProfiniteToLightCondSet ⋙ free R).map (cover π) ≫
          (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
                    (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
                  free R).map
              WalkingParallelPairHom.left ≫
            (g -
                (lightProfiniteToLightCondSet ⋙ free R).map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫ g +
              (lightProfiniteToLightCondSet ⋙ free R).map
                  (r_inf ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                      π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                g) =
      ((lightProfiniteToLightCondSet ⋙ free R).mapCocone
                (coproductCocone T
                  (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))).ι.app
          j ≫
        (lightProfiniteToLightCondSet ⋙ free R).map (cover π) ≫
          (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
                    (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
                  free R).map
              WalkingParallelPairHom.right ≫
            (g -
                (lightProfiniteToLightCondSet ⋙ free R).map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫ g +
              (lightProfiniteToLightCondSet ⋙ free R).map
                  (r_inf ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                      π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                g)