awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
f : X ⟶ Y
⊢ ((id x).map f).edge =
    edge (x₀ :=
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })))
        x)
      (id
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) →
              (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })))
          x))

Tactic:
simp [NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
x y : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
f g : Edge x y
edge : f.edge = g.edge
⊢ f = g

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
x y : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
f g : Edge x y
⊢ f.edge = g.edge

Tactic:
subsingleton
-- 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))
⊢ ∃ (x₀ :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (x₁ :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (x₂ :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) (h : e₀₁.CompStruct e₁₂ e₀₂), h.simplex = s

Tactic:
⟨X.map (Hom.tr (SimplexCategory.const _ _ 0)).op s,
    X.map (Hom.tr (SimplexCategory.const _ _ 1)).op s,
    X.map (Hom.tr (SimplexCategory.const _ _ 2)).op s,
    .mk _ ?_ ?_, .mk _ ?_ ?_, .mk _ ?_ ?_, .mk s rfl rfl rfl, rfl⟩

Premises used: SimplexCategory.Truncated.Hom.tr, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, SSet.Truncated.Edge.mk, SimplexCategory.const, Exists.intro, OfNat.ofNat, SSet.Truncated.Edge.CompStruct.mk, DFunLike.coe, rfl
-- 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_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 ≫ δ₂ 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⦌ 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 (δ₂ 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⦌ 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_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 ≫ δ₂ 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⦌ 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 ≫ δ₂ 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⦌ 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_1 : δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 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 ≫ δ₂ 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⦌ 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 ≫ δ₂ 2 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_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) ⋯ ⋯).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 (δ₂ 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⦌ ⋯))))

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_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) ⋯ ⋯).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 ≫ δ₂ 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⦌ ⋯))))

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_2 : δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 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 := ⋯ })))

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 ≫ δ₂ 2 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯

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_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) ⋯ ⋯).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 (δ₂ 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⦌ ⋯))))

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_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) ⋯ ⋯).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 ≫ δ₂ 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⦌ ⋯))))

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_3 : δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 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 := ⋯ })))

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 ≫ δ₂ 0 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯

Tactic:
decide