Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case left
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 ℕ∪{∞}))
⊢ (free R).map
            (lightProfiniteToLightCondSet.map
                ((coproductCocone T
                          (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                            (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π))).ι.app
                    { as := WalkingPair.left } ≫
                  cover π) ≫
              lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π)) ≫
          g -
        (free R).map
            (lightProfiniteToLightCondSet.map
                ((coproductCocone T
                          (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                            (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π))).ι.app
                    { as := WalkingPair.left } ≫
                  cover π ≫ CompHausLike.pullback.fst π π) ≫
              lightProfiniteToLightCondSet.map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g +
      (free R).map
          (lightProfiniteToLightCondSet.map
              ((coproductCocone T
                        (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π))).ι.app
                  { as := WalkingPair.left } ≫
                cover π ≫ CompHausLike.pullback.fst π π) ≫
            lightProfiniteToLightCondSet.map
              (r_inf ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                  π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
        g =
    (free R).map
            (lightProfiniteToLightCondSet.map
                ((coproductCocone T
                          (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                            (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π))).ι.app
                    { as := WalkingPair.left } ≫
                  cover π) ≫
              lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ≫
          g -
        (free R).map
            (lightProfiniteToLightCondSet.map
                ((coproductCocone T
                          (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                            (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π))).ι.app
                    { as := WalkingPair.left } ≫
                  cover π ≫ CompHausLike.pullback.snd π π) ≫
              lightProfiniteToLightCondSet.map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
          g +
      (free R).map
          (lightProfiniteToLightCondSet.map
              ((coproductCocone T
                        (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π))).ι.app
                  { as := WalkingPair.left } ≫
                cover π ≫ CompHausLike.pullback.snd π π) ≫
            lightProfiniteToLightCondSet.map
              (r_inf ≫
                LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                  π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}))) ≫
        g

Tactic:
rfl

Goal state after: