Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case right
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 ℕ∪{∞}))
this :
  cover π =
    ↑(BinaryCofan.IsColimit.desc'
        (coproductIsColimit T
          (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
            (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))
        (CompHausLike.pullback.lift π π (𝟙 T) (𝟙 T) ⋯)
        (CompHausLike.pullback.lift π π
          (CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
              (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
          (CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
              (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
          ⋯))
⊢ (free R).map
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g -
        (free R).map
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g +
      (free R).map
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.fst (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 =
    (free R).map
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g -
        (free R).map
            (lightProfiniteToLightCondSet.map
              (CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g +
      (free R).map
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.snd (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

Tactic:
simp only [← assoc, hr, id_comp, sub_self, zero_add]

Goal state after:
case right
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 ℕ∪{∞}))
this :
  cover π =
    ↑(BinaryCofan.IsColimit.desc'
        (coproductIsColimit T
          (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
            (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))
        (CompHausLike.pullback.lift π π (𝟙 T) (𝟙 T) ⋯)
        (CompHausLike.pullback.lift π π
          (CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
              (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
          (CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
              (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))
          ⋯))
⊢ (free R).map
        (lightProfiniteToLightCondSet.map
          (((((CompHausLike.pullback.fst (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                      (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                  π) ≫
                fst S ℕ∪{∞}) ≫
              σ) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
      g =
    (free R).map
        (lightProfiniteToLightCondSet.map
          (((((CompHausLike.pullback.snd (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                      (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
                    LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
                  π) ≫
                fst S ℕ∪{∞}) ≫
              σ) ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
      g