-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.cocone_ι_app : ∀ (R : Type) [inst : CommRing R] {X : LightCondMod R} {S T : LightProfinite}
  (π : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj S LightProfinite.NatUnionInfty)
  [inst_1 :
    CategoryTheory.Epi
      ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map (InternalProjectivityProof.cover✝ π))]
  (g : (lightProfiniteToLightCondSet.comp (LightCondensed.free R)).obj T ⟶ X)
  (r_inf :
    T ⟶
      InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
        (CategoryTheory.CategoryStruct.comp π
          (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
  (σ :
    S ⟶
      InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
        (CategoryTheory.CategoryStruct.comp π
          (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
  (hr :
    CategoryTheory.CategoryStruct.comp
        (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
          (CategoryTheory.CategoryStruct.comp π
            (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
        r_inf =
      CategoryTheory.CategoryStruct.id
        (InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
          (CategoryTheory.CategoryStruct.comp π
            (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty))))
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (InternalProjectivityProof.cocone✝ R π g r_inf σ hr).ι.app X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.Limits.WalkingParallelPair.rec
        (CategoryTheory.CategoryStruct.comp
              ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))) g -
            CategoryTheory.CategoryStruct.comp
              ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π)))
              (CategoryTheory.CategoryStruct.comp ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map r_inf))
                (CategoryTheory.CategoryStruct.comp
                  ((LightCondensed.free R).map
                    (lightProfiniteToLightCondSet.map
                      (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                        (CategoryTheory.CategoryStruct.comp π
                          (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))))
                  g)) +
          CategoryTheory.CategoryStruct.comp
            ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π)))
            (CategoryTheory.CategoryStruct.comp ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map r_inf))
              (CategoryTheory.CategoryStruct.comp
                ((LightCondensed.free R).map
                  (lightProfiniteToLightCondSet.map
                    (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                      (CategoryTheory.CategoryStruct.comp π
                        (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))))
                (CategoryTheory.CategoryStruct.comp ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map π))
                  (CategoryTheory.CategoryStruct.comp
                    ((LightCondensed.free R).map
                      (lightProfiniteToLightCondSet.map
                        (CategoryTheory.SemiCartesianMonoidalCategory.fst S LightProfinite.NatUnionInfty)))
                    (CategoryTheory.CategoryStruct.comp
                      ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map σ))
                      (CategoryTheory.CategoryStruct.comp
                        ((LightCondensed.free R).map
                          (lightProfiniteToLightCondSet.map
                            (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                              (CategoryTheory.CategoryStruct.comp π
                                (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))))
                        g)))))))
        (g -
            CategoryTheory.CategoryStruct.comp ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map r_inf))
              (CategoryTheory.CategoryStruct.comp
                ((LightCondensed.free R).map
                  (lightProfiniteToLightCondSet.map
                    (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                      (CategoryTheory.CategoryStruct.comp π
                        (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))))
                g) +
          CategoryTheory.CategoryStruct.comp ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map r_inf))
            (CategoryTheory.CategoryStruct.comp
              ((LightCondensed.free R).map
                (lightProfiniteToLightCondSet.map
                  (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                    (CategoryTheory.CategoryStruct.comp π
                      (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))))
              (CategoryTheory.CategoryStruct.comp ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map π))
                (CategoryTheory.CategoryStruct.comp
                  ((LightCondensed.free R).map
                    (lightProfiniteToLightCondSet.map
                      (CategoryTheory.SemiCartesianMonoidalCategory.fst S LightProfinite.NatUnionInfty)))
                  (CategoryTheory.CategoryStruct.comp ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map σ))
                    (CategoryTheory.CategoryStruct.comp
                      ((LightCondensed.free R).map
                        (lightProfiniteToLightCondSet.map
                          (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                            (CategoryTheory.CategoryStruct.comp π
                              (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))))
                      g))))))
        X_1)