-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X Y : Truncated 2
f₀ :
  X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1)) →
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
f₁ :
  X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)) →
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))
hδ₁ :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))),
    f₀
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 _proof_1 _proof_3).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := _proof_1 })))
          x) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (δ₂ 1 _proof_1 _proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0⦌, property := _proof_1 })))
        (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))),
    f₀
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _proof_1 _proof_3).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := _proof_1 })))
          x) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (δ₂ 0 _proof_1 _proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0⦌, property := _proof_1 })))
        (f₁ x)
hσ :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))),
    f₁
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 0 _proof_3 _proof_1).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := _proof_3 })))
          x) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_3 _proof_1).op) :
          (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0 + 1⦌, property := _proof_3 })))
        (f₀ x)
hY : Y.StrictSegal
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))
a :
  f₁
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((σ₂ 0 _proof_5 _proof_2).op ≫ (δ₂ 2 _proof_2 _proof_5).op)) :
          (a : X.obj (op { obj := ⦋1⦌, property := _proof_2 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
        x) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.map (Quiver.Hom.op (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_1))) :
        (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_5 _proof_2).op) :
            (a : Y.obj (op { obj := ⦋1⦌, property := _proof_2 })) → Y.obj (op { obj := ⦋2⦌, property := _proof_5 }))
          (f₁ x) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5)))
a₁ :
  f₁
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 _proof_2 _proof_5 ≫ σ₂ 0 _proof_5 _proof_2).op) :
          (a : X.obj (op { obj := ⦋1⦌, property := _proof_2 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
        x) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.map (Quiver.Hom.op (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_1))) :
        (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_5 _proof_2).op) :
            (a : Y.obj (op { obj := ⦋1⦌, property := _proof_2 })) → Y.obj (op { obj := ⦋2⦌, property := _proof_5 }))
          (f₁ x) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5)))
a₂ :
  f₁
      ((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 (op { obj := ⦋1⦌, property := _proof_2 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
        x) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.map (Quiver.Hom.op (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_1))) :
        (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_5 _proof_2).op) :
            (a : Y.obj (op { obj := ⦋1⦌, property := _proof_2 })) → Y.obj (op { obj := ⦋2⦌, property := _proof_5 }))
          (f₁ x) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5)))
a₃ :
  f₁
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              ((δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op ≫
                (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4).op)) :
          (a : X.obj (op { obj := ⦋1⦌, property := _proof_2 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
        x) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.map (Quiver.Hom.op (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_1))) :
        (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_5 _proof_2).op) :
            (a : Y.obj (op { obj := ⦋1⦌, property := _proof_2 })) → Y.obj (op { obj := ⦋2⦌, property := _proof_5 }))
          (f₁ x) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5)))
a₄ :
  f₁
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4).op) :
          (a : X.obj (op { obj := ⦋0⦌, property := δ₂_zero_comp_σ₂_one._proof_4 })) →
            X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op) :
              (a : X.obj (op { obj := ⦋1⦌, property := _proof_2 })) →
                X.obj (op { obj := ⦋0⦌, property := δ₂_zero_comp_σ₂_one._proof_4 }))
            x :
          X.obj
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                δ₂_zero_comp_σ₂_one._proof_4)))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.map (Quiver.Hom.op (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_1))) :
        (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_5 _proof_2).op) :
            (a : Y.obj (op { obj := ⦋1⦌, property := _proof_2 })) → Y.obj (op { obj := ⦋2⦌, property := _proof_5 }))
          (f₁ x) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5)))
⊢ f₁
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 _proof_2 _proof_5).op) :
          (a : X.obj (op { obj := ⦋2⦌, property := _proof_5 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 0 _proof_5 _proof_2).op) :
              (a : X.obj (op { obj := ⦋1⦌, property := _proof_2 })) → X.obj (op { obj := ⦋2⦌, property := _proof_5 }))
            x :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5)))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.map (Quiver.Hom.op (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ f₂._proof_1))) :
        (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_5 _proof_2).op) :
            (a : Y.obj (op { obj := ⦋1⦌, property := _proof_2 })) → Y.obj (op { obj := ⦋2⦌, property := _proof_5 }))
          (f₁ x) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5)))
have a₅ : Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_3 _proof_1).op) :
        (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
          (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0 + 1⦌, property := _proof_3 })))
      (f₀
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map (δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op) :
            (a : X.obj (op { obj := ⦋1⦌, property := _proof_2 })) →
              X.obj (op { obj := ⦋0⦌, property := δ₂_zero_comp_σ₂_one._proof_4 }))
          x)) :
    (fun (X : Type u) ↦ X)
      (Y.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
            _proof_3))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.map (Quiver.Hom.op (Hom.tr (SimplexCategory.mkOfSucc 0) sorry f₂._proof_1))) :
        (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.obj (op { obj := ⦋1⦌, property := sorry }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (σ₂ 0 _proof_5 _proof_2).op) :
            (a : Y.obj (op { obj := ⦋1⦌, property := _proof_2 })) → Y.obj (op { obj := ⦋2⦌, property := _proof_5 }))
          (f₁ x) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_5))) :
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ sorry)))
Tactic: rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_zero, op_comp,
      Functor.map_comp_apply, hσ, SimplexCategory.mkOfSucc_zero_eq_δ,
      ← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_zero,
      op_comp, Functor.map_comp_apply, hδ₁]