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 ℕ∪{∞}))
⊢ ((lightProfiniteToLightCondSet ⋙ free R).mapCocone
              (coproductCocone T
                (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))).ι.app
        { as := WalkingPair.left } ≫
      (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
        { as := WalkingPair.left } ≫
      (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)

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 ℕ∪{∞}))
⊢ ((lightProfiniteToLightCondSet ⋙ free R).mapCocone
              (coproductCocone T
                (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))).ι.app
        { as := WalkingPair.right } ≫
      (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
        { as := WalkingPair.right } ≫
      (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:
· simp [← map_comp_assoc, -Functor.map_comp]
    rfl

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 ℕ∪{∞}))
⊢ ((lightProfiniteToLightCondSet ⋙ free R).mapCocone
              (coproductCocone T
                (CompHausLike.pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                  (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))).ι.app
        { as := WalkingPair.right } ≫
      (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
        { as := WalkingPair.right } ≫
      (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)