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 π') ⋯))
this :
  LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' =
    LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞)
⊢ (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

Tactic:
reassoc_of% this,

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 π') ⋯))
this :
  LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' =
    LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞)
⊢ (lightProfiniteToLightCondSet ⋙ free R).map
        (r_inf ≫
          LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
            π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞) ≫ y' ▷ ℕ∪{∞}) ≫
      f =
    (lightProfiniteToLightCondSet ⋙ free R).map
        (r_inf ≫
          LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
            π' ≫
              fst S' ℕ∪{∞} ≫
                split.section_ ≫
                  LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
                    π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞) ≫ y' ▷ ℕ∪{∞}) ≫
      f