awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ Eq (α :=
    (x :
        X.obj
          (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))) →
      X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) :
      (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
        X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) :
      (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := ⋯ }))) →
        (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := ⋯ })))
have refine_5 : δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 0) sorry sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 Edge._proof_1 _proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
            (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })))
        ((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 })))
            s :
          (fun (X : Type u) ↦ X)
            (X.obj
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ Edge._proof_2)))) :
      (fun (X : Type u) ↦ X)
        (X.obj
          (Opposite.op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := ⋯ })))
        s :
      (fun (X : Type u) ↦ X)
        (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))))
have refine_6 : Eq (α :=
  (fun (X : Type u) ↦ X)
    (X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op) :
        (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
          X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
      s :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) sorry sorry).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := sorry })))
      s :
    (fun (X : Type u) ↦ X)
      (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ sorry))))
Tactic: rw [← Functor.map_comp_apply, ← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op) :
          (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
            X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
        s :
      X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := ⋯ })))
        s :
      (fun (X : Type u) ↦ X)
        (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))))
have refine_6 : Eq (α :=
  (x :
      X.obj
        (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))) →
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) :
    (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
      X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) sorry sorry).op)) :
    (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := sorry }))) →
      (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := sorry })))
Tactic: apply congr_fun
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ Eq (α :=
    (x :
        X.obj
          (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))) →
      X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) :
      (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
        X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) :
      (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := ⋯ }))) →
        (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := ⋯ })))
have refine_6 : δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 2) sorry sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
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 (δ₂ 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 (σ₂ 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)))) =
    (id x).edge
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
              δ₂ 1 δ₂_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 x).edge
Tactic: rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
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 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
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (Quiver.Hom.op (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ sorry)))) :
      (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: rw [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
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 (δ₂ 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
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (Quiver.Hom.op (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ sorry)))) :
      (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: rw [← Functor.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
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 (δ₂ 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
have 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
Tactic: rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_one]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
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 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
have 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
Tactic: rw [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_one]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
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 (δ₂ 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
have 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⦌
                sorry)))) :
      (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: rw [← Functor.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_one]
-- 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 : s.pt
i : Fin n
⊢ ((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
have 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 sorry) lift._proof_3).hom ≫
                  CategoryTheory.Functor.map (Functor.op (inclusion 2))
                    (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) sorry sorry))).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: ext x
-- 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.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) :
      ℕ)
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.δ 1) sorry sorry))).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,
              sorry⟩ :
            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,
            sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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 : s.pt
i : Fin n
⊢ ((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
have 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 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))
          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: ext x