awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
i : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin (i + 1)
simp :
  Eq (α := op ⦋n⦌ ⟶ op ⦋0⦌) (f.op ≫ Quiver.Hom.op (⦋0⦌.const ⦋i⦌ k))
    (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f : (a : Fin (i + 1)) → Fin (n + 1)) k)))
⊢ (strArrowMk₂ f hi).hom ≫ CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Hom.tr (⦋0⦌.const ⦋i⦌ k) ⋯ hi).op =
    StructuredArrow.hom
      (strArrowMk₂
        (⦋0⦌.const ⦋n⦌
          ((Hom.toOrderHom f :
              (a : Fin ((unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi }))).len + 1)) →
                Fin ((unop (op ⦋n⦌)).len + 1))
            k))
        lift._proof_1)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
i : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Eq (α := op ⦋n⦌ ⟶ op ⦋0⦌) (f.op ≫ Quiver.Hom.op (⦋0⦌.const ⦋i⦌ k))
    (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f : (a : Fin (i + 1)) → Fin (n + 1)) k)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
i : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin (i + 1)
α : strArrowMk₂ f hi ⟶
  strArrowMk₂
    (⦋0⦌.const ⦋n⦌
      ((Hom.toOrderHom f :
          (a : Fin ((unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi }))).len + 1)) →
            Fin ((unop (op ⦋n⦌)).len + 1))
        k))
    lift._proof_1 :=
  homMk (Hom.tr (⦋0⦌.const ⦋i⦌ k) ⋯ hi).op ⋯
⊢ Eq.{u + 1} (α := X _⦋0⦌)
    (Path.vertex (n := n)
      {
        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 := ⋯ }
      ((Hom.toOrderHom f : (a : Fin (⦋i⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋i⦌ k))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋i⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app
                  (StructuredArrow.mk (Y :=
                    op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi)) f.op)) :
              TypeCat.Fun s.pt (X _⦋i⦌)) :
            (a : s.pt) → X _⦋i⦌)
          x :
        X _⦋i⦌))

Tactic:
ConcreteCategory.congr_hom (s.w α).symm x

Premises used: Quiver.Hom.op, SimplexCategory.const, CategoryTheory.Limits.Cone.w, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
i : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin (i + 1)
α : strArrowMk₂ f hi ⟶
  strArrowMk₂
    (⦋0⦌.const ⦋n⦌
      ((Hom.toOrderHom f :
          (a : Fin ((unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi }))).len + 1)) →
            Fin ((unop (op ⦋n⦌)).len + 1))
        k))
    lift._proof_1 :=
  homMk (Hom.tr (⦋0⦌.const ⦋i⦌ k) ⋯ hi).op ⋯
⊢ Eq.{u + 1} (α := X _⦋0⦌)
    (Path.vertex (n := n)
      {
        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 := ⋯ }
      ((Hom.toOrderHom f : (a : Fin (⦋i⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋i⦌ k))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋i⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app
                  (StructuredArrow.mk (Y :=
                    op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi)) f.op)) :
              TypeCat.Fun s.pt (X _⦋i⦌)) :
            (a : s.pt) → X _⦋i⦌)
          x :
        X _⦋i⦌))

Tactic:
exact ConcreteCategory.congr_hom (s.w α).symm x

Premises used: CategoryTheory.Limits.Cone.w, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
i : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin i
⊢ (strArrowMk₂ f ⋯).hom ≫ CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Hom.tr (mkOfSucc k) ⋯ hi).op =
    (strArrowMk₂ (mkOfSucc k ≫ f) lift._proof_3).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
i : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin i
α : strArrowMk₂ f ⋯ ⟶ strArrowMk₂ (mkOfSucc k ≫ f) lift._proof_3 := homMk (Hom.tr (mkOfSucc k) ⋯ hi).op ⋯
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (op f ≫ (mkOfSucc k).op)) : (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 (mkOfSucc k).op) : (a : X _⦋i⦌) → X _⦋1⦌)
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (s.π.app (StructuredArrow.mk (op f))) :
                TypeCat.Fun s.pt (X _⦋i⦌)) :
              (a : s.pt) → X _⦋i⦌)
            x :
          X _⦋i⦌) :
      X _⦋1⦌)

Tactic:
(isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans
        (ConcreteCategory.congr_hom (s.w α).symm x)

Premises used: SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
i : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin i
α : strArrowMk₂ f ⋯ ⟶ strArrowMk₂ (mkOfSucc k ≫ f) lift._proof_3 := homMk (Hom.tr (mkOfSucc k) ⋯ hi).op ⋯
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (op f ≫ (mkOfSucc k).op)) : (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 (mkOfSucc k).op) : (a : X _⦋i⦌) → X _⦋1⦌)
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (s.π.app (StructuredArrow.mk (op f))) :
                TypeCat.Fun s.pt (X _⦋i⦌)) :
              (a : s.pt) → X _⦋i⦌)
            x :
          X _⦋i⦌) :
      X _⦋1⦌)

Tactic:
exact (isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans
        (ConcreteCategory.congr_hom (s.w α).symm x)

Premises used: SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, CategoryTheory.Limits.Cone.w, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
h :
  ∀ (x : s.pt),
    (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x
⊢ m = ↾fun (x : s.pt) ↦ lift sx s x

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
h :
  Eq (α := X.Path n)
    ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n) ((ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x) : X.Path n)
    ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n)
        (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x) :
      X.Path n)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x

Tactic:
apply sx.spineInjective (X := X)

Premises used: SSet.StrictSegal.spineInjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
h :
  X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x) =
    {
      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 := ⋯ }
⊢ Eq (α := X.Path n)
    ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n) ((ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x) : X.Path n)
    ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n)
        (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x) :
      X.Path n)

Tactic:
simp only [spineEquiv, RightExtension.coneAt_pt, rightExtensionInclusion_left,
      TypeCat.Fun.toFun_apply, Equiv.coe_fn_mk, lift, Nat.reduceAdd, ObjectProperty.ι_obj,
      const_obj_obj, comp_obj, proj_obj, mk_right, op_obj, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      spine_spineToSimplex_apply]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.RightExtension.coneAt_pt, SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift, TypeCat.Fun.coe_mk, TypeCat.hom_ofHom, Nat.reduceAdd, CategoryTheory.ObjectProperty.ι_obj, TypeCat.Fun.toFun_apply, SSet.Truncated.rightExtensionInclusion_left, CategoryTheory.StructuredArrow.mk_right, SSet.StrictSegal.spine_spineToSimplex_apply, Equiv.coe_fn_mk, CategoryTheory.Functor.const_obj_obj, CategoryTheory.StructuredArrow.proj_obj, CategoryTheory.Functor.op_obj, SSet.StrictSegal.spineEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
i : Fin (n + 1)
⊢ (X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x)).vertex i =
    Path.vertex
      {
        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 := ⋯ }
      i

Tactic:
ConcreteCategory.congr_hom (hm (StructuredArrow.mk
        (Y := op ⦋0⦌₂) (⦋0⦌.const ⦋n⦌ i).op)) x

Premises used: Quiver.Hom.op, SimplexCategory.const, SimplexCategory.mk, CategoryTheory.StructuredArrow.mk, CategoryTheory.ConcreteCategory.congr_hom, OfNat.ofNat, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
i : Fin (n + 1)
⊢ (X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x)).vertex i =
    Path.vertex
      {
        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 := ⋯ }
      i

Tactic:
exact ConcreteCategory.congr_hom (hm (StructuredArrow.mk
        (Y := op ⦋0⦌₂) (⦋0⦌.const ⦋n⦌ i).op)) x

Premises used: Quiver.Hom.op, SimplexCategory.const, SimplexCategory.mk, CategoryTheory.StructuredArrow.mk, CategoryTheory.ConcreteCategory.congr_hom, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x)).arrow i =
    Path.arrow
      {
        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 := ⋯ }
      i

Tactic:
ConcreteCategory.congr_hom (hm (.mk (Y := op ⦋1⦌₂)
        (.op (mkOfLe _ _ (Fin.castSucc_le_succ i))))) x

Premises used: Fin.castSucc_le_succ, Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.mkOfLe, SimplexCategory.mkOfSucc, CategoryTheory.StructuredArrow.mk, CategoryTheory.ConcreteCategory.congr_hom, SimplexCategory.Hom.mk