-- 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 : 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) :
        (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 :
        (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) :
      (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 :
      (fun (X : Type u) ↦ X) (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) α₀))
h₂ :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Quiver.Hom.op (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i + k, ⋯⟩ : Fin (n + 1)) ⋯))) :
          (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex
          {
            vertex := fun (i : Fin (n + 1)) ↦
              (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (s.π.app
                      (StructuredArrow.mk (Y :=
                        op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            lift._proof_2))
                        (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
                  (a : s.pt) → X _⦋0⦌)
                x,
            arrow := fun (i : Fin n) ↦
              (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (s.π.app
                      (StructuredArrow.mk (Y :=
                        op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                            lift._proof_4))
                        (mkOfLe i.castSucc i.succ ⋯).op)) :
                  (a : s.pt) → X _⦋1⦌)
                x,
            arrow_src := ⋯, arrow_tgt := ⋯ }) :
      X _⦋1⦌)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3)) :
          (a : s.pt) → X _⦋1⦌)
        x :
      X _⦋1⦌)
t : Fin (HAdd.hAdd (α := ℕ) 1 1)
this : α.hom ≫ Quiver.Hom.op (mkOfSucc 0) = α₂.hom
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Quiver.Hom.op (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i + k, ⋯⟩ : Fin (n + 1)) ⋯))) :
          (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex
          {
            vertex := fun (i : Fin (n + 1)) ↦
              (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (s.π.app
                      (StructuredArrow.mk (Y :=
                        op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            lift._proof_2))
                        (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
                  (a : s.pt) → X _⦋0⦌)
                x,
            arrow := fun (i : Fin n) ↦
              (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (s.π.app
                      (StructuredArrow.mk (Y :=
                        op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                            lift._proof_4))
                        (mkOfLe i.castSucc i.succ ⋯).op)) :
                  (a : s.pt) → X _⦋1⦌)
                x,
            arrow_src := ⋯, arrow_tgt := ⋯ }) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋2⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_11)) :
              (a : s.pt) → X _⦋2⦌)
            x :
          X _⦋2⦌) :
      X _⦋1⦌)
have rw : Eq (α := X _⦋1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map β₂.right.unop.hom.op) :
        (a : X.obj (op (unop α.right).obj)) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app α) : (a : s.pt) → X.obj (op (unop α.right).obj)) x :
        X.obj (op ((unop α.right).obj (P := fun (a : SimplexCategory) ↦ a.len ≤ 2)))) :
    X _⦋1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋2⦌) → X _⦋1⦌)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (s.π.app (strArrowMk₂ (mkOfLeComp ⟨i, sorry⟩ ⟨i + k, sorry⟩ ⟨j, sorry⟩ sorry sorry) fac_aux₂._proof_11)) :
            (a : s.pt) → X _⦋2⦌)
          x :
        X _⦋2⦌) :
    X _⦋1⦌)
Tactic: rw [h₂, ← dsimp% [α₂] ConcreteCategory.congr_hom (s.w β₂) x]