-- 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 intro.zero
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ ⟶ strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ :=
  homMk (⦋1⦌.const ⦋0⦌ 0).op ⋯
nat :
  s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x =
    X.map ((Truncated.inclusion 2).map α.right.unop).op (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x)
⊢ X.map (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op (lift s x) = s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x

Tactic:
unfold strArrowMk₂

Result:
case intro.zero
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ ⟶ strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ :=
  homMk (⦋1⦌.const ⦋0⦌ 0).op ⋯
nat :
  s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x =
    X.map ((Truncated.inclusion 2).map α.right.unop).op (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x)
⊢ X.map (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op (lift s x) = s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op) x

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, ⋯⟩ ⋯) ⋯
⊢ i < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case intro.zero
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ ⟶ strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ :=
  homMk (⦋1⦌.const ⦋0⦌ 0).op ⋯
nat :
  (((Functor.const (StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op)).obj s.pt).map α ≫
        s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯))
      x =
    (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) ≫
        (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X).map α)
      x
⊢ X.map (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op (lift s x) =
    s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x

Tactic:
dsimp only [Fin.val_zero, Nat.add_zero, id_eq, Int.reduceNeg, Int.Nat.cast_ofNat_Int,
  Int.reduceAdd, Fin.eta, comp_obj, StructuredArrow.proj_obj, op_obj, const_obj_obj,
  const_obj_map, types_comp_apply, types_id_apply, Functor.comp_map, StructuredArrow.proj_map,
  op_map] at nat

Result:
case intro.zero
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ ⟶ strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯ :=
  homMk (⦋1⦌.const ⦋0⦌ 0).op ⋯
nat :
  s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x =
    X.map ((Truncated.inclusion 2).map α.right.unop).op (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x)
⊢ X.map (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op (lift s x) =
    s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) ⋯) x

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
⊢ ⟨i + k, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]

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
⊢ i + k ≤ j

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
i j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x

Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest hij

Result:
case intro
X : SSet
inst✝ : X.StrictSegal
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
k : ℕ
hk : i + k = j
⊢ X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x

Proof state:
case intro
X : SSet
inst✝ : X.StrictSegal
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
k : ℕ
hk : i + k = j
⊢ X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x

Tactic:
revert i j

Result:
case intro
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
⊢ ∀ (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