awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
φ : strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3 ⟶ strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1 :=
  homMk (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯)) ⋯
⊢ Eq (α :=
    obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
      (op
        (obj (incl 1 1 ⋯)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌
            Truncated.Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (obj (truncation 1) X)
              (Quiver.Hom.op
                (ObjectProperty.homMk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) (SimplexCategory.δ 0)))) :
          (a :
              ((truncation 1).obj X).obj (op ((incl 1 1 ⋯).obj { obj := ⦋1⦌, property := Truncated.Path₁._proof_5 }))) →
            ((truncation 1).obj X).obj (op ((incl 1 1 ⋯).obj { obj := ⦋0⦌, property := Truncated.Path₁._proof_1 })))
        ((@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 :
          X _⦋1⦌) :
      obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
        (op
          (obj (incl 1 1 ⋯)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌
              Truncated.Path₁._proof_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.succ)))) :
          (a : s.pt) → X _⦋0⦌)
        x :
      X _⦋0⦌)

Tactic:
ConcreteCategory.congr_hom (s.w φ) x

Premises used: Quiver.Hom.op, CategoryTheory.Limits.Cone.w, CategoryTheory.ObjectProperty.homMk, CategoryTheory.ConcreteCategory.congr_hom
-- 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
φ : strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3 ⟶ strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) lift._proof_1 :=
  homMk (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯)) ⋯
⊢ Eq (α :=
    obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
      (op
        (obj (incl 1 1 ⋯)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌
            Truncated.Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (obj (truncation 1) X)
              (Quiver.Hom.op
                (ObjectProperty.homMk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) (SimplexCategory.δ 0)))) :
          (a :
              ((truncation 1).obj X).obj (op ((incl 1 1 ⋯).obj { obj := ⦋1⦌, property := Truncated.Path₁._proof_5 }))) →
            ((truncation 1).obj X).obj (op ((incl 1 1 ⋯).obj { obj := ⦋0⦌, property := Truncated.Path₁._proof_1 })))
        ((@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 :
          X _⦋1⦌) :
      obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
        (op
          (obj (incl 1 1 ⋯)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌
              Truncated.Path₁._proof_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.succ)))) :
          (a : s.pt) → X _⦋0⦌)
        x :
      X _⦋0⦌)

Tactic:
exact ConcreteCategory.congr_hom (s.w φ) x

Premises used: CategoryTheory.Limits.Cone.w, CategoryTheory.ConcreteCategory.congr_hom
-- 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 < n
dsimp :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc (⟨i, hi⟩ : Fin n)).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 _ types TypeCat.Fun _ _ _ _ _
            (s.π.app (strArrowMk₂ (mkOfSucc (⟨i, hi⟩ : Fin n)) fac_aux₁._proof_1)) :
          (a : s.pt) → X _⦋1⦌)
        x :
      X _⦋1⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc (⟨i, hi⟩ : Fin n)).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₂ (mkOfSucc (⟨i, hi⟩ : Fin n)) fac_aux₁._proof_1)) :
          (a :
              (fun (X : Type u) ↦ X)
                (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                  (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) fac_aux₁._proof_1)))
        x :
      (fun (X : Type u) ↦ X)
        (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
          (strArrowMk₂ (mkOfSucc (⟨i, hi⟩ : Fin n)) fac_aux₁._proof_1)))

Tactic:
dsimp [lift]

Premises used: SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift
-- 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 < n
rw :
  Eq.{u + 1} (α := X _⦋1⦌)
    (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, hi⟩ : Fin n))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (s.π.app (strArrowMk₂ (mkOfSucc (⟨i, hi⟩ : Fin n)) fac_aux₁._proof_1)) :
        (a : s.pt) → X _⦋1⦌)
      x)
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc (⟨i, hi⟩ : Fin n)).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 _ types TypeCat.Fun _ _ _ _ _
            (s.π.app (strArrowMk₂ (mkOfSucc (⟨i, hi⟩ : Fin n)) fac_aux₁._proof_1)) :
          (a : s.pt) → X _⦋1⦌)
        x :
      X _⦋1⦌)

Tactic:
rw [spineToSimplex_arrow]

Premises used: SSet.StrictSegal.spineToSimplex_arrow
-- 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 < n
⊢ Eq.{u + 1} (α := X _⦋1⦌)
    (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, hi⟩ : Fin n))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (s.π.app (strArrowMk₂ (mkOfSucc (⟨i, hi⟩ : Fin n)) fac_aux₁._proof_1)) :
        (a : s.pt) → X _⦋1⦌)
      x)

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 j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ i < n + 1

Tactic:
lia
-- 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 j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ j < n + 1

Tactic:
lia
-- 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 j : ℕ
hij : i ≤ j
hj : j ≤ n
obtain :
  ∀ (k : ℕ) (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)))
⊢ 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)))

Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest hij

Premises used: Nat.le.dest
-- 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 j : ℕ
hij : i ≤ j
hj : j ≤ n
k : ℕ
hk : i + k = j
revert :
  ∀ (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)))
⊢ 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)))

Tactic:
revert i j
-- 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 j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + 0 = j
⊢ i = j

Tactic:
hik
-- 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 j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + 0 = j
zero :
  ∀ (hij : i ≤ i) (hj : i ≤ n),
    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)))
⊢ 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)))

Tactic:
obtain rfl : i = j := hik

Premises used: 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
⊢ (⟨i, ⋯⟩ : Fin (n + 1)) ≤ ⟨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
⊢ mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)

Tactic:
have : mkOfLe ⟨i, Nat.lt_add_one_of_le hj⟩ ⟨i, Nat.lt_add_one_of_le hj⟩ (by rfl) =
        ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩ := Hom.ext_one_left _ _