Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this :
  (ConcreteCategory.hom (X.map α.hom))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map (Hom.right β₁).unop.hom.op))
      ((ConcreteCategory.hom (X.map α.hom))
        (sx.spineToSimplex
          { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
            arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
            arrow_src := ⋯, arrow_tgt := ⋯ })) =
    (ConcreteCategory.hom (s.π.app α₁)) x

Tactic:
rw [this, ← s.w β₁]

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this :
  (ConcreteCategory.hom (X.map α.hom))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map (Hom.right β₁).unop.hom.op)) ((ConcreteCategory.hom (s.π.app α)) x) =
    (ConcreteCategory.hom (s.π.app α ≫ (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).map β₁)) x