awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
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)
⊢ (↑((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) :
      ℕ)
have a : (↑((Hom.toOrderHom
            ((strArrowMk₂ (mkOfLe i.castSucc i.succ sorry) lift._proof_3).hom ≫
                CategoryTheory.Functor.map (Functor.op (inclusion 2))
                  (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) sorry sorry))).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, sorry⟩ :
            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, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ 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)))
have 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 sorry).op)) :
                (a : s.pt) → X _⦋1⦌)
              x,
          arrow_src := sorry, arrow_tgt := sorry }) :
    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: dsimp [lift]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ 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⦌)
have 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 sorry).op)) :
            (a : s.pt) → X _⦋1⦌)
          x,
      arrow_src := sorry, arrow_tgt := sorry }
    (⟨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: rw [spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
i j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ 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)))
have obtain : ∀ (k : ℕ) (hk : i + k = j),
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfLe (⟨i, sorry⟩ : Fin (n + 1)) (⟨j, sorry⟩ : 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, sorry⟩ : Fin (n + 1)) (⟨j, sorry⟩ : 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, sorry⟩ ⟨j, sorry⟩ hij) fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (strArrowMk₂ (mkOfLe ⟨i, sorry⟩ ⟨j, sorry⟩ 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, sorry⟩ : Fin (n + 1)) (⟨j, sorry⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)))
Tactic: obtain ⟨k, hk⟩ := Nat.le.dest hij
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
i j : ℕ
hij : i ≤ j
hj : j ≤ n
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)))
have 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, sorry⟩ : Fin (n + 1)) (⟨j, sorry⟩ : 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, sorry⟩ : Fin (n + 1)) (⟨j, sorry⟩ : 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, sorry⟩ ⟨j, sorry⟩ hij) fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (strArrowMk₂ (mkOfLe ⟨i, sorry⟩ ⟨j, sorry⟩ 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, sorry⟩ : Fin (n + 1)) (⟨j, sorry⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)))
Tactic: revert i j
Cleared hypotheses: i, j, hij, hj, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + 0 = 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)))
have zero : ∀ (hij : i ≤ i) (hj : i ≤ n),
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfLe (⟨i, sorry⟩ : Fin (n + 1)) (⟨i, sorry⟩ : 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, sorry⟩ : Fin (n + 1)) (⟨i, sorry⟩ : 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, sorry⟩ ⟨i, sorry⟩ hij) fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (strArrowMk₂ (mkOfLe ⟨i, sorry⟩ ⟨i, sorry⟩ 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, sorry⟩ : Fin (n + 1)) (⟨i, sorry⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)))
Tactic: obtain rfl : i = j := hik
Cleared hypotheses: j, hij, hj, hik
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (hypothesis)
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
⊢ 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)))
have this : mkOfLe (⟨i, sorry⟩ : Fin (n + 1)) (⟨i, sorry⟩ : Fin (n + 1)) sorry =
  CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, sorry⟩)
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 _ _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
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 (α := (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)))
have 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, sorry⟩ : 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, sorry⟩ : 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, sorry⟩) 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, sorry⟩) 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, sorry⟩ : Fin (⦋n⦌.len + 1))))
          fac_aux₁._proof_1)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
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).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
have simp : Eq (α := op ⦋n⦌ ⟶ op ⦋1⦌)
  (CategoryStruct.comp (Y := op ⦋0⦌) (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ⟨i, sorry⟩)) (Quiver.Hom.op (⦋1⦌.const ⦋0⦌ 0)))
  (Quiver.Hom.op (⦋1⦌.const ⦋n⦌ ⟨i, sorry⟩))
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
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 ⋯
| ((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)))
have dsimp : ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋n⦌ ⟨i, sorry⟩) fac_aux₁._proof_1)) :
      (a : s.pt) → X _⦋1⦌)
    x :
  X _⦋1⦌)
Tactic: dsimp