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 (α :=
    (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 (δ₂ 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 })))
            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⦌ 1) ⋯ ⋯).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_2 : 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 ≫ δ₂ 2 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⦌ 1) 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 ≫ δ₂ 2 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⦌ 1) ⋯ ⋯).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_2 : 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 ≫ δ₂ 2 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⦌ 1) 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 ≫ δ₂ 2 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⦌ 1) ⋯ ⋯).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_2 : δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 1) 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 (δ₂ 1 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 (δ₂ 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 })))
            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⦌ 1) ⋯ ⋯).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_3 : 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 (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 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⦌ 1) 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 (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 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⦌ 1) ⋯ ⋯).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_3 : 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 ≫ δ₂ 0 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⦌ 1) 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 (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 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⦌ 1) ⋯ ⋯).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_3 : δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 1) 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 (δ₂ 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 })))
            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_4 : 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 ≫ δ₂ 0 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 ≫ δ₂ 0 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_4 : 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 ≫ δ₂ 0 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 ≫ δ₂ 0 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_4 : δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 0 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 : 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 (δ₂ 1 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⦌ 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 := ⋯ })))
        s :
      (fun (X : Type u) ↦ X)
        (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))))
have refine_5 : 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 (δ₂ 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 }))
      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⦌ 0) 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 (δ₂ 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 }))
        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⦌ 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 := ⋯ })))
        s :
      (fun (X : Type u) ↦ X)
        (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))))
have refine_5 : 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) 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