-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
/-- For any `σ : X ⟶ Y` between `StrictSegal` simplicial sets, `spineToSimplex`
commutes with `Path.map`. -/
lemma spineToSimplex_map {X Y : SSet.{u}} [StrictSegal X] [StrictSegal Y]
    {n : ℕ} (f : Path X (n + 1)) (σ : X ⟶ Y) :
    spineToSimplex (f.map σ) = σ.app _ (spineToSimplex f)

Proof state:
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ spineToSimplex (f.map σ) = σ.app (Opposite.op ⦋n + 1⦌) (spineToSimplex f)

Tactic:
apply spineInjective

Result:
case a
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ (spineEquiv (n + 1)) (spineToSimplex (f.map σ)) =
    (spineEquiv (n + 1)) (σ.app (Opposite.op ⦋n + 1⦌) (spineToSimplex f))

Proof state:
case a
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ (spineEquiv (n + 1)) (spineToSimplex (f.map σ)) =
    (spineEquiv (n + 1)) (σ.app (Opposite.op ⦋n + 1⦌) (spineToSimplex f))

Tactic:
ext k

Result:
case a.h
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ ((spineEquiv (n + 1)) (spineToSimplex (f.map σ))).arrow k =
    ((spineEquiv (n + 1)) (σ.app (Opposite.op ⦋n + 1⦌) (spineToSimplex f))).arrow k

Proof state:
case a.h
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ Y.map (mkOfSucc k).op
      (spineToSimplex
        { vertex := fun i => σ.app (Opposite.op ⦋0⦌) (f.vertex i),
          arrow := fun i => σ.app (Opposite.op ⦋1⦌) (f.arrow i), arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (X.map (mkOfSucc k).op ≫ σ.app (Opposite.op ⦋1⦌)) (spineToSimplex f)

Tactic:
simp only [types_comp_apply, spineToSimplex_arrow]

Result:
no goals

Proof state:
case a.h
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ ((spineEquiv (n + 1)) (spineToSimplex (f.map σ))).arrow k =
    ((spineEquiv (n + 1)) (σ.app (Opposite.op ⦋n + 1⦌) (spineToSimplex f))).arrow k

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk, Path.map, spine_arrow]

Result:
case a.h
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ Y.map (mkOfSucc k).op
      (spineToSimplex
        { vertex := fun i => σ.app (Opposite.op ⦋0⦌) (f.vertex i),
          arrow := fun i => σ.app (Opposite.op ⦋1⦌) (f.arrow i), arrow_src := ⋯, arrow_tgt := ⋯ }) =
    Y.map (mkOfSucc k).op (σ.app (Opposite.op ⦋n + 1⦌) (spineToSimplex f))

Proof state:
case a.h
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ Y.map (mkOfSucc k).op
      (spineToSimplex
        { vertex := fun i => σ.app (Opposite.op ⦋0⦌) (f.vertex i),
          arrow := fun i => σ.app (Opposite.op ⦋1⦌) (f.arrow i), arrow_src := ⋯, arrow_tgt := ⋯ }) =
    Y.map (mkOfSucc k).op (σ.app (Opposite.op ⦋n + 1⦌) (spineToSimplex f))

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

Result:
case a.h
X Y : SSet
inst✝¹ : X.StrictSegal
inst✝ : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ Y.map (mkOfSucc k).op
      (spineToSimplex
        { vertex := fun i => σ.app (Opposite.op ⦋0⦌) (f.vertex i),
          arrow := fun i => σ.app (Opposite.op ⦋1⦌) (f.arrow i), arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (X.map (mkOfSucc k).op ≫ σ.app (Opposite.op ⦋1⦌)) (spineToSimplex f)