-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
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_2 _proof_5).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
            (fun (X : Type u) ↦ X) (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)))) =
    Path.arrow (m := 2)
      ((hY.spineEquiv 2 f₂._proof_1 : (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.Path 2)
        ((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))))
      1
⊢ Eq.{u + 1} (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))
    (Path.arrow (m := 2)
      ((hY.spineEquiv 2 f₂._proof_1 : (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.Path 2)
        (f₂ f₀ f₁ hδ₁ hδ₀ hY
          ((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)))
      1)
    (Path.arrow (m := 2)
      ((hY.spineEquiv 2 f₂._proof_1 : (a : Y.obj (op { obj := ⦋2⦌, property := f₂._proof_1 })) → Y.Path 2)
        ((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))))
      1)

Tactic:
rw [spineEquiv_f₂_arrow_one]

Premises used: SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one