-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
a :
  Eq (α := Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (mkOfSucc k).op) : (a : Y _⦋n + 1⦌) → Y _⦋1⦌)
        (sy.spineToSimplex (f.map σ)) :
      Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌) ≫ Y.map (mkOfSucc k).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        (sx.spineToSimplex f) :
      (fun (X : Type u) ↦ X) (Y _⦋1⦌))
a₁ :
  Eq (α := Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (mkOfSucc k).op) : (a : Y _⦋n + 1⦌) → Y _⦋1⦌)
        (sy.spineToSimplex (f.map σ)) :
      Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op ≫ σ.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        (sx.spineToSimplex f) :
      (fun (X : Type u) ↦ X) (Y _⦋1⦌))
a₂ :
  Eq (α := Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (mkOfSucc k).op) : (a : Y _⦋n + 1⦌) → Y _⦋1⦌)
        (sy.spineToSimplex (f.map σ)) :
      Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (X _⦋1⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋1⦌))
a₃ :
  (f.map σ).arrow k =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (sx.spineToSimplex f) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
a₄ :
  (f.map σ).arrow k =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      (f.arrow k)
a₅ a₆ :
  Eq (α := Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        (f.arrow k) :
      (fun (X : Type u) ↦ X) (Y _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        (f.arrow k) :
      (fun (X : Type u) ↦ X) (Y _⦋1⦌))
⊢ Eq (α := Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (mkOfSucc k).op) : (a : Y _⦋n + 1⦌) → Y _⦋1⦌)
        (sy.spineToSimplex (f.map σ)) :
      Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (mkOfSucc k).op) : (a : Y _⦋n + 1⦌) → Y _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌)) : (a : X _⦋n + 1⦌) → Y _⦋n + 1⦌)
            (sx.spineToSimplex f) :
          Y _⦋n + 1⦌) :
      Y _⦋1⦌)

Tactic:
rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality, types_comp_apply,
    spineToSimplex_arrow, spineToSimplex_arrow, Path.map_arrow]

Premises used: SSet.Path.map_arrow, CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, SSet.StrictSegal.spineToSimplex_arrow, CategoryTheory.NatTrans.app, CategoryTheory.types_comp_apply