Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
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 : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (free R).map (lightProfiniteToLightCondSet.map π') ≫
      (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f =
    (free R).map (lightProfiniteToLightCondSet.map g') ≫ (free R).map (lightProfiniteToLightCondSet.map π) ≫ f -
        (free R).map (lightProfiniteToLightCondSet.map r_inf) ≫
          (free R).map (lightProfiniteToLightCondSet.map (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))) ≫
            (free R).map (lightProfiniteToLightCondSet.map g') ≫ (free R).map (lightProfiniteToLightCondSet.map π) ≫ f +
      (free R).map (lightProfiniteToLightCondSet.map r_inf) ≫
        (free R).map (lightProfiniteToLightCondSet.map (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))) ≫
          (free R).map (lightProfiniteToLightCondSet.map π') ≫
            (free R).map (lightProfiniteToLightCondSet.map (fst S' ℕ∪{∞})) ≫
              (free R).map (lightProfiniteToLightCondSet.map split.section_) ≫
                (free R).map (lightProfiniteToLightCondSet.map (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))) ≫
                  (free R).map (lightProfiniteToLightCondSet.map g') ≫
                    (free R).map (lightProfiniteToLightCondSet.map π) ≫ f

Tactic:
simp only [← Functor.map_comp, ← Functor.comp_map, ← assoc, ← comp]

Goal state after:
case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
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 : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map (π' ≫ y' ▷ ℕ∪{∞}) ≫ f =
    (lightProfiniteToLightCondSet ⋙ free R).map (π' ≫ y' ▷ ℕ∪{∞}) ≫ f -
        (lightProfiniteToLightCondSet ⋙ free R).map
            (((r_inf ≫ LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞})) ≫ π') ≫ y' ▷ ℕ∪{∞}) ≫
          f +
      (lightProfiniteToLightCondSet ⋙ free R).map
          (((((((r_inf ≫ LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞})) ≫ π') ≫ fst S' ℕ∪{∞}) ≫ split.section_) ≫
                LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞})) ≫
              π') ≫
            y' ▷ ℕ∪{∞}) ≫
        f