awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
k : ℕ
hk :
  ∀ (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)))
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_11
α₀ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯)) ⋯
⊢ (α.hom ≫ CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Hom.tr (mkOfSucc 0) ⋯ ⋯).op).unop = α₂.hom.unop
have a : ∀ (x : Fin ((unop (obj (Functor.op (inclusion 2)) α₂.right)).len + 1)),
  (↑((Hom.toOrderHom (α.hom ≫ CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Hom.tr (mkOfSucc 0) sorry sorry).op).unop :
            (a : Fin ((unop ((inclusion 2).op.obj α₂.right)).len + 1)) → Fin ((unop (op ⦋n⦌)).len + 1))
          x) :
      ℕ) =
    (↑((Hom.toOrderHom α₂.hom.unop :
            (a : Fin ((unop ((inclusion 2).op.obj α₂.right)).len + 1)) → Fin ((unop (op ⦋n⦌)).len + 1))
          x) :
      ℕ)
Tactic: ext 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
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map φ.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₂ φ fac_aux₁._proof_1)) :
          (a :
              (fun (X : Type u) ↦ X)
                (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                  (strArrowMk₂ φ fac_aux₁._proof_1))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj (strArrowMk₂ φ fac_aux₁._proof_1)))
        x :
      (fun (X : Type u) ↦ X)
        (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
          (strArrowMk₂ φ fac_aux₁._proof_1)))
have obtain : ∀ (i j : Fin (n + 1)) (hij : i ≤ j),
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfLe i j 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 j 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 j hij) fac_aux₁._proof_1)))
Tactic: obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij :=
    ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide),
      Hom.ext_one_left _ _ rfl rfl⟩
Cleared hypotheses: φ
-- 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)
j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))
⊢ CategoryStruct.comp (Y :=
      Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
        (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌)))
      (↾fun (x : s.pt) ↦ lift sx s x :
        s.pt ⟶
          Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
            (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌)))
      (NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j :
        obj
            (obj
              (Functor.const
                (StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))))
              (Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
                (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))))
            j ⟶
          obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) j) =
    s.π.app j
have h : ∀ (x : s.pt),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
            (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌)))
          (↾fun (x : s.pt) ↦ lift sx s x :
            s.pt ⟶
              Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
                (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌)))
          (NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j :
            obj
                (obj
                  (Functor.const
                    (StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))))
                  (Cone.pt (J :=
                    StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
                    (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))))
                j ⟶
              obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) j)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app j)).toFun x
Tactic: ext 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 ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ (strArrowMk₂ f hi).hom ≫ CategoryTheory.Functor.map (Functor.op (inclusion 2)) (Hom.tr (⦋0⦌.const ⦋i⦌ k) ⋯ hi).op =
    StructuredArrow.hom
      (strArrowMk₂
        (⦋0⦌.const ⦋n⦌
          ((Hom.toOrderHom f :
              (a : Fin ((unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi }))).len + 1)) →
                Fin ((unop (op ⦋n⦌)).len + 1))
            k))
        lift._proof_1)
have simp : Eq (α := op ⦋n⦌ ⟶ op ⦋0⦌) (f.op ≫ Quiver.Hom.op (⦋0⦌.const ⦋i⦌ k))
  (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f : (a : Fin (i + 1)) → Fin (n + 1)) k)))
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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
⊢ m = ↾fun (x : s.pt) ↦ lift sx s x
have h : ∀ (x : s.pt),
  (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x
Tactic: ext 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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x
have h : Eq (α := X.Path n)
  ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n) ((ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x) : X.Path n)
  ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n)
      (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x) :
    X.Path n)
Tactic: apply sx.spineInjective (X := 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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
⊢ Eq (α := X.Path n)
    ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n) ((ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x) : X.Path n)
    ((sx.spineEquiv n : (a : X _⦋n⦌) → X.Path n)
        (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : s.pt) ↦ lift sx s x)) x) :
      X.Path n)
have h : X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x) =
  {
    vertex := fun (i : Fin (n + 1)) ↦
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (s.π.app
              (StructuredArrow.mk (Y :=
                op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ lift._proof_2))
                (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
          (a : s.pt) → X _⦋0⦌)
        x,
    arrow := fun (i : Fin n) ↦
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (s.π.app
              (StructuredArrow.mk (Y :=
                op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ lift._proof_4))
                (mkOfLe i.castSucc i.succ sorry).op)) :
          (a : s.pt) → X _⦋1⦌)
        x,
    arrow_src := sorry, arrow_tgt := sorry }
Tactic: simp only [spineEquiv, RightExtension.coneAt_pt, rightExtensionInclusion_left,
      TypeCat.Fun.toFun_apply, Equiv.coe_fn_mk, lift, Nat.reduceAdd, ObjectProperty.ι_obj,
      const_obj_obj, comp_obj, proj_obj, mk_right, op_obj, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      spine_spineToSimplex_apply]
-- 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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
⊢ X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x) =
    {
      vertex := fun (i : Fin (n + 1)) ↦
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (s.π.app
                (StructuredArrow.mk (Y :=
                  op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ lift._proof_2))
                  (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
            (a : s.pt) → X _⦋0⦌)
          x,
      arrow := fun (i : Fin n) ↦
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (s.π.app
                (StructuredArrow.mk (Y :=
                  op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ lift._proof_4))
                  (mkOfLe i.castSucc i.succ ⋯).op)) :
            (a : s.pt) → X _⦋1⦌)
          x,
      arrow_src := ⋯, arrow_tgt := ⋯ }
have h : ∀ (i : Fin (n + 1)),
  (X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x)).vertex i =
    Path.vertex
      {
        vertex := fun (i : Fin (n + 1)) ↦
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app
                  (StructuredArrow.mk (Y :=
                    op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        lift._proof_2))
                    (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
              (a : s.pt) → X _⦋0⦌)
            x,
        arrow := fun (i : Fin n) ↦
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app
                  (StructuredArrow.mk (Y :=
                    op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                        lift._proof_4))
                    (mkOfLe i.castSucc i.succ sorry).op)) :
              (a : s.pt) → X _⦋1⦌)
            x,
        arrow_src := sorry, arrow_tgt := sorry }
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
⊢ Eq (α := Set (X _⦋0⦌)) (X.degenerate 0) ∅
have h : ∀ (x : X _⦋0⦌), Membership.mem (γ := Set (X _⦋0⦌)) (X.degenerate 0) x ↔ Membership.mem (γ := Set (X _⦋0⦌)) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
x : X _⦋0⦌
⊢ Membership.mem (γ := Set (X _⦋0⦌)) (X.degenerate 0) x ↔ Membership.mem (γ := Set (X _⦋0⦌)) ∅ x
have h : x ∉ X.degenerate 0
Tactic: simp only [Set.mem_empty_iff_false, iff_false]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
        x
have mp : x ∈ X.degenerate n →
  ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
      x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
mp :
  x ∈ X.degenerate n →
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
        x
⊢ x ∈ X.degenerate n ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
        x
have mpr : (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
      x) →
  x ∈ X.degenerate n
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    x
⊢ ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
      x
have hy₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (CategoryStruct.comp (Y := op (image f)) (Quiver.Hom.op (image.ι f)) (Quiver.Hom.op (factorThruImage f)))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
    y =
  x
Tactic: rw [← image.fac f, op_comp] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (CategoryStruct.comp (Y := op (image f)) (Quiver.Hom.op (image.ι f)) (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    x
⊢ ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
      x
have this : (image f).len ≤ m
Tactic: have : _ ≤ m := SimplexCategory.len_le_of_mono (image.ι f)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ Membership.mem (α := X _⦋n⦌) (X.degenerate n) ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌) ↔
    Membership.mem (γ := Set (X.op _⦋n⦌)) (X.op.degenerate n) x
have simp : (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
      (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
      ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
  ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set (X.op _⦋n⦌))
      (Set.range (ι := X.op _⦋m⦌)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
      x
Tactic: simp only [mem_degenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
have refine : ∀ m < n,
  (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
Tactic: refine exists_congr (fun m ↦ exists_congr (fun _ ↦ ?_))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
h : m < n
⊢ (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
have mp : (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
      (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
      ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) →
  ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set (X.op _⦋n⦌))
      (Set.range (ι := X.op _⦋m⦌)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
      x
Tactic: constructor