awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
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) ⋯ ⋯).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⦌ ⋯))))
⊢ 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⦌ ⋯))))

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
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) ⋯ ⋯).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 := ⋯ })))
⊢ 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⦌ ⋯))))

Tactic:
apply congr_fun

Premises used: congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
refine_4 : δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 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 ≫ δ₂ 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 := ⋯ })))

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
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) ⋯ ⋯).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⦌ ⋯))))
⊢ 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⦌ ⋯))))

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
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) ⋯ ⋯).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 := ⋯ })))
⊢ 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⦌ ⋯))))

Tactic:
apply congr_fun

Premises used: congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
refine_5 : δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯
⊢ 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 := ⋯ })))

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
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) ⋯ ⋯).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⦌ ⋯))))
⊢ 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⦌ ⋯))))

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
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) ⋯ ⋯).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 := ⋯ })))
⊢ 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⦌ ⋯))))

Tactic:
apply congr_fun

Premises used: congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
refine_6 : δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 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 ≫ δ₂ 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 := ⋯ })))

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
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
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
⊢ (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

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_zero]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
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 δ₂_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:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
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
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋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
⊢ (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

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_zero]

Premises used: CategoryTheory.op_comp, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero, CategoryTheory.Functor.map_comp_apply