-- 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))
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).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⦌ ⋯))))
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).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⦌ ⋯))))
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).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⦌ ⋯))))
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).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⦌ ⋯))))
⊢ ∃ (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
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).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) 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: refine ⟨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⟩