-- Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean
lemma fac_aux₂ {n : ℕ}
    (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
    (x : s.pt) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) :
    X.map (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij).op (lift s x) =
      s.π.app (strArrowMk₂ (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij)) x

Proof state:
case a.h
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x
h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x
⊢ ∀ (i : Fin (1 + 1)), ((spineEquiv 2) (X.map α.hom (lift s x))).arrow i = ((spineEquiv 2) (s.π.app α x)).arrow i

Tactic:
intro t

Result:
case a.h
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x
h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x
t : Fin (1 + 1)
⊢ ((spineEquiv 2) (X.map α.hom (lift s x))).arrow t = ((spineEquiv 2) (s.π.app α x)).arrow t

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x
h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x
t : Fin (1 + 1)
this : α.hom ≫ (mkOfSucc 0).op = α₂.hom
⊢ X.map (α.hom ≫ (mkOfSucc 0).op) (lift s x) = X.map (mkOfSucc 0).op (s.π.app α x)

Tactic:
rw [this, h₂, ← congr_fun (s.w β₂) x]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x
h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x
t : Fin (1 + 1)
this : α.hom ≫ (mkOfSucc 0).op = α₂.hom
⊢ (s.π.app α ≫ (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X).map β₂) x =
    X.map (mkOfSucc 0).op (s.π.app α x)

Proof state:
case intro.succ
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
⊢ X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x

Tactic:
have h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x := by
  subst hik
  exact fac_aux₁ _ _ _ _ hj

Result:
case intro.succ
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x
⊢ X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x