-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
R : Type
inst : CommRing R
X : LightCondMod R
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst_1 :
  Epi (C := LightCondMod R) (X :=
    obj (lightProfiniteToLightCondSet ⋙ free R)
      (CompHausLike.of
        (fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        ((↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type) ⊕
          (↑((CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) (X :=
                    LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})) (Y := LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)).toTop
                (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type))))
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π))
g : obj (lightProfiniteToLightCondSet ⋙ free R) 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 ℕ∪{∞}))
⊢ Cocone (C := LightCondMod R)
    (parallelPair (X :=
        lightProfiniteToLightCondSet.obj
          (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
        (lightProfiniteToLightCondSet.map
          (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
        (lightProfiniteToLightCondSet.map
          (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
      free R)
have refine : Eq (α :=
  obj
      (parallelPair (X :=
          lightProfiniteToLightCondSet.obj
            (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
        free R)
      WalkingParallelPair.zero ⟶
    X)
  (CategoryTheory.Functor.map
      (parallelPair (X :=
          lightProfiniteToLightCondSet.obj
            (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
        free R)
      WalkingParallelPairHom.left ≫
    (g -
        CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
            (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
          g +
      CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
              π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
        g))
  (CategoryTheory.Functor.map
      (parallelPair (X :=
          lightProfiniteToLightCondSet.obj
            (CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π))
          (lightProfiniteToLightCondSet.map
            (CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π π)) ⋙
        free R)
      WalkingParallelPairHom.right ≫
    (g -
        CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
            (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
          g +
      CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R)
          (r_inf ≫
            LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
              π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
        g))
Tactic: refine Cocone.ofCofork (Cofork.ofπ (g -
    (lightProfiniteToLightCondSet ⋙ free R).map
      (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd _ _)) ≫ g +
    (lightProfiniteToLightCondSet ⋙ free R).map
      (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd _ _) ≫ π ≫ fst _ _ ≫ σ ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd _ _)) ≫ g) ?_)