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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
zero :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1)))))) :
          (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₂
                (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
                fac_aux₁._proof_1)) :
          (a :
              (fun (X : Type u) ↦ X)
                (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                  (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1)))
        x :
      (fun (X : Type u) ↦ X)
        (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
          (strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
            fac_aux₁._proof_1)))
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : 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)) (⟨i, ⋯⟩ : 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, ⋯⟩ ⟨i, ⋯⟩ hij) fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ 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)) (⟨i, ⋯⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)))

Tactic:
rw [this]
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
simp :
  Eq (α := op ⦋n⦌ ⟶ op ⦋1⦌)
    (CategoryStruct.comp (Y := op ⦋0⦌) (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0)))
    (Quiver.Hom.op (⦋1⦌.const ⦋n⦌ ⟨i, ⋯⟩))
⊢ (strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1).hom ≫
      CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op =
    (strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
⊢ Eq (α := op ⦋n⦌ ⟶ op ⦋1⦌)
    (CategoryStruct.comp (Y := op ⦋0⦌) (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0)))
    (Quiver.Hom.op (⦋1⦌.const ⦋n⦌ ⟨i, ⋯⟩))

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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
dsimp :
  ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1)) :
        (a : s.pt) → X _⦋1⦌)
      x :
    X _⦋1⦌)
| ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (s.π.app
            (strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
              fac_aux₁._proof_1)) :
        (a :
            (fun (X : Type u) ↦ X)
              (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) →
          (fun (X : Type u) ↦ X)
            ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
              (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1)))
      x :
    (fun (X : Type u) ↦ X)
      (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
        (strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
          fac_aux₁._proof_1)))

Tactic:
dsimp
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
rw :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
            (a : s.pt) → X _⦋0⦌)
          x :
        X _⦋0⦌) :
    X _⦋1⦌)
| ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1)) :
        (a : s.pt) → X _⦋1⦌)
      x :
    X _⦋1⦌)

Tactic:
rw [dsimp% s.π.naturality_apply α x]

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality_apply
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
rw :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
            (a : s.pt) → X _⦋0⦌)
          x :
        X _⦋0⦌) :
    X _⦋1⦌)
| ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (s.π.app
            (strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
              fac_aux₁._proof_1)) :
        (a :
            (fun (X : Type u) ↦ X)
              (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) →
          (fun (X : Type u) ↦ X)
            ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
              (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1)))
      x :
    (fun (X : Type u) ↦ X)
      (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
        (strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
          fac_aux₁._proof_1)))

Tactic:
dsimp; rw [dsimp% s.π.naturality_apply α x]

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality_apply
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
zero :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1)))))) :
          (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) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
              (a : s.pt) → X _⦋0⦌)
            x :
          X _⦋0⦌) :
      X _⦋1⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1)))))) :
          (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₂
                (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
                fac_aux₁._proof_1)) :
          (a :
              (fun (X : Type u) ↦ X)
                (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                  (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1)))
        x :
      (fun (X : Type u) ↦ X)
        (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
          (strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))))
            fac_aux₁._proof_1)))

Tactic:
conv_rhs => dsimp; rw [dsimp% s.π.naturality_apply α x]

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality_apply
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
zero :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := X _⦋0⦌) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1)))))
              (X.map (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0)))) :
          (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) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
              (a : s.pt) → X _⦋0⦌)
            x :
          X _⦋0⦌) :
      X _⦋1⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1)))))) :
          (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) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
              (a : s.pt) → X _⦋0⦌)
            x :
          X _⦋0⦌) :
      X _⦋1⦌)

Tactic:
rw [op_comp, Functor.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
zero :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0))) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (n + 1))))) :
              (a : X _⦋n⦌) → X _⦋0⦌)
            (lift sx s x) :
          X _⦋0⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
              (a : s.pt) → X _⦋0⦌)
            x :
          X _⦋0⦌) :
      X _⦋1⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := X _⦋0⦌) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1)))))
              (X.map (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0)))) :
          (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) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
              (a : s.pt) → X _⦋0⦌)
            x :
          X _⦋0⦌) :
      X _⦋1⦌)

Tactic:
simp only [types_comp_apply]

Premises used: CategoryTheory.types_comp_apply
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0))) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (n + 1))))) :
              (a : X _⦋n⦌) → X _⦋0⦌)
            (lift sx s x) :
          X _⦋0⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
              (a : s.pt) → X _⦋0⦌)
            x :
          X _⦋0⦌) :
      X _⦋1⦌)

Tactic:
congrArg (X.map (⦋1⦌.const ⦋0⦌ 0).op) ?_

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, SimplexCategory.const, SimplexCategory.mk, OfNat.ofNat, DFunLike.coe, 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
zero :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (n + 1))))) :
          (a : X _⦋n⦌) → X _⦋0⦌)
        (lift sx s x) :
      X _⦋0⦌)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
          (a : s.pt) → X _⦋0⦌)
        x :
      X _⦋0⦌)
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0))) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (n + 1))))) :
              (a : X _⦋n⦌) → X _⦋0⦌)
            (lift sx s x) :
          X _⦋0⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α.right.unop.hom.op) : (a : X _⦋0⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
              (a : s.pt) → X _⦋0⦌)
            x :
          X _⦋0⦌) :
      X _⦋1⦌)

Tactic:
refine congrArg (X.map (⦋1⦌.const ⦋0⦌ 0).op) ?_

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, SimplexCategory.const, SimplexCategory.mk, OfNat.ofNat, DFunLike.coe
-- 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 : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
zero :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (n + 1))))) :
          (a : X _⦋n⦌) → X _⦋0⦌)
        (lift sx s x) :
      X _⦋0⦌)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (s.π.app
              (StructuredArrow.mk (Y :=
                op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ lift._proof_1))
                (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)))) :
          (a : s.pt) → X _⦋0⦌)
        x :
      X _⦋0⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (n + 1))))) :
          (a : X _⦋n⦌) → X _⦋0⦌)
        (lift sx s x) :
      X _⦋0⦌)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1)) :
          (a : s.pt) → X _⦋0⦌)
        x :
      X _⦋0⦌)

Tactic:
unfold strArrowMk₂

Premises used: SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂