-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x_1 : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) (hk : i + k = j),
    Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨j, ⋯⟩ : Fin (n + 1)) hij).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (lift sx s x_1) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (s.π.app (strArrowMk₂ (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨j, ⋯⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)) :
            (a :
                (fun (X : Type u) ↦ X)
                  (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                    (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) →
              (fun (X : Type u) ↦ X)
                ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                  (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1)))
          x_1 :
        (fun (X : Type u) ↦ X)
          (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
            (strArrowMk₂ (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨j, ⋯⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)))
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_11
α₀ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯)) ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ :
  Eq (α := (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₀.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α₀.hom) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.obj ((inclusion 2).op.obj α₀.right)))
        (lift sx s x_1) :
      (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₀.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app α₀) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj α₀)) →
            (fun (X : Type u) ↦ X) ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj α₀))
        x_1 :
      (fun (X : Type u) ↦ X) (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) α₀))
h₂ :
  Eq (α := (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₂.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α₂.hom) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.obj ((inclusion 2).op.obj α₂.right)))
        (lift sx s x_1) :
      (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₂.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app α₂) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj α₂)) →
            (fun (X : Type u) ↦ X) ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj α₂))
        x_1 :
      (fun (X : Type u) ↦ X) (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) α₂))
t : Fin (HAdd.hAdd (α := ℕ) 1 1)
x : Fin ((unop (op ⦋1⦌)).len + 1)
⊢ (↑((Hom.toOrderHom (α.hom ≫ Quiver.Hom.op (mkOfSucc 1)).unop :
            (a : Fin ((unop (op ⦋1⦌)).len + 1)) → Fin ((unop (op ⦋n⦌)).len + 1))
          x) :
      ℕ) =
    (↑((Hom.toOrderHom α₀.hom.unop : (a : Fin ((unop (op ⦋1⦌)).len + 1)) → Fin ((unop (op ⦋n⦌)).len + 1)) x) : ℕ)
have a : (↑((Hom.toOrderHom (α.hom ≫ Quiver.Hom.op (mkOfSucc 1)).unop :
          (a : Fin ((unop (op ⦋1⦌)).len + 1)) → Fin ((unop (op ⦋n⦌)).len + 1))
        ((fun (i : Fin ((unop (op ⦋1⦌)).len + 1)) ↦ i) (⟨0, sorry⟩ : Fin ((unop (op ⦋1⦌)).len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom α₀.hom.unop : (a : Fin ((unop (op ⦋1⦌)).len + 1)) → Fin ((unop (op ⦋n⦌)).len + 1))
        ((fun (i : Fin ((unop (op ⦋1⦌)).len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x