awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    e.edge

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    e.edge
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_2 _proof_2).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 0 _proof_2 Edge._proof_2).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })))
          e.edge :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 1 1⦌
                _proof_2)))) =
    e.edge

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_zero]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                  δ₂_zero_comp_σ₂_one._proof_1)))) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    e.edge
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 Edge._proof_2 _proof_2).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 1 _proof_2 Edge._proof_2).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })))
          e.edge :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 1 1⦌
                _proof_2)))) =
    e.edge

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_one]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, SimplexCategory.Truncated.δ₂_two_comp_σ₂_one
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                  δ₂_zero_comp_σ₂_one._proof_1)))) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    e.edge

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
                δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    (id y).edge
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 Edge._proof_2 _proof_2).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 1 _proof_2 Edge._proof_2).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })))
          e.edge :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 1 1⦌
                _proof_2)))) =
    (id y).edge

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_one]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
                δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    (id y).edge

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                  ⋯)))) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    e.edge
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_2 _proof_2).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 1 _proof_2 Edge._proof_2).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })))
          e.edge :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 1 1⦌
                _proof_2)))) =
    e.edge

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_one]

Premises used: CategoryTheory.op_comp, SimplexCategory.Truncated.δ₂_one_comp_σ₂_one, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x y :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e : Edge x y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                  ⋯)))) :
        (a : X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })) →
          X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 }))
      e.edge =
    e.edge

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X_1 : SSet
sx_1 : X_1.StrictSegal
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 : Fin n
a :
  ∀
    (x :
      Fin
        ((unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len + 1)),
    (↑((Hom.toOrderHom
                ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                    CategoryTheory.Functor.map (Functor.op (inclusion 2))
                      (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯))).unop :
              (a :
                  Fin
                    ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                      1)) →
                Fin ((unop (op ⦋n⦌)).len + 1))
            x) :
        ℕ) =
      (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).hom.unop :
              (a :
                  Fin
                    ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                      1)) →
                Fin ((unop (op ⦋n⦌)).len + 1))
            x) :
        ℕ)
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
        CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯))).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).hom.unop

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X_1 : SSet
sx_1 : X_1.StrictSegal
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
i : Fin n
x : Fin ((unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len + 1)
a :
  (↑((Hom.toOrderHom
              ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                  CategoryTheory.Functor.map (Functor.op (inclusion 2))
                    (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯))).unop :
            (a :
                Fin
                  ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                    1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                      1)) ↦
              i)
            (⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len,
                ⋯⟩ :
              Fin
                ((unop
                      (obj (Functor.op (inclusion 2))
                        (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                  1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).hom.unop :
            (a :
                Fin
                  ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                    1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                      1)) ↦
              i)
            ⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len,
              ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom
              ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                  CategoryTheory.Functor.map (Functor.op (inclusion 2))
                    (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯))).unop :
            (a :
                Fin
                  ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                    1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          x) :
      ℕ) =
    (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).hom.unop :
            (a :
                Fin
                  ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                    1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          x) :
      ℕ)

Tactic:
fin_cases x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X_1 : SSet
sx_1 : X_1.StrictSegal
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 : Fin n
⊢ (↑((Hom.toOrderHom
              ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                  CategoryTheory.Functor.map (Functor.op (inclusion 2))
                    (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯))).unop :
            (a :
                Fin
                  ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                    1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                      1)) ↦
              i)
            (⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len,
                ⋯⟩ :
              Fin
                ((unop
                      (obj (Functor.op (inclusion 2))
                        (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                  1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).hom.unop :
            (a :
                Fin
                  ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                    1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len +
                      1)) ↦
              i)
            ⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1).right)).len,
              ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X_1 : SSet
sx_1 : X_1.StrictSegal
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 : Fin n
a :
  ∀
    (x :
      Fin ((unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)),
    (↑((Hom.toOrderHom
                ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                    CategoryTheory.Functor.map (Functor.op (inclusion 2))
                      (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯))).unop :
              (a :
                  Fin
                    ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
                Fin ((unop (op ⦋n⦌)).len + 1))
            x) :
        ℕ) =
      (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).hom.unop :
              (a :
                  Fin
                    ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
                Fin ((unop (op ⦋n⦌)).len + 1))
            x) :
        ℕ)
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
        CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯))).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).hom.unop

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X_1 : SSet
sx_1 : X_1.StrictSegal
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
i : Fin n
x : Fin ((unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)
a :
  (↑((Hom.toOrderHom
              ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                  CategoryTheory.Functor.map (Functor.op (inclusion 2))
                    (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯))).unop :
            (a : Fin ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len +
                      1)) ↦
              i)
            (⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len, ⋯⟩ :
              Fin
                ((unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len +
                  1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).hom.unop :
            (a : Fin ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len +
                      1)) ↦
              i)
            ⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len,
              ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom
              ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                  CategoryTheory.Functor.map (Functor.op (inclusion 2))
                    (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯))).unop :
            (a : Fin ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          x) :
      ℕ) =
    (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).hom.unop :
            (a : Fin ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          x) :
      ℕ)

Tactic:
fin_cases x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X_1 : SSet
sx_1 : X_1.StrictSegal
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 : Fin n
⊢ (↑((Hom.toOrderHom
              ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3).hom ≫
                  CategoryTheory.Functor.map (Functor.op (inclusion 2))
                    (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯))).unop :
            (a : Fin ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len +
                      1)) ↦
              i)
            (⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len, ⋯⟩ :
              Fin
                ((unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len +
                  1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).hom.unop :
            (a : Fin ((unop ((inclusion 2).op.obj (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len + 1)) →
              Fin ((unop (op ⦋n⦌)).len + 1))
          ((fun
                (i :
                  Fin
                    ((unop
                          (obj (Functor.op (inclusion 2))
                            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len +
                      1)) ↦
              i)
            ⟨(unop (obj (Functor.op (inclusion 2)) (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1).right)).len,
              ⋯⟩)) :
      ℕ)

Tactic:
rfl