-- 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) ⦋2⦌ _proof_4)))
    (y : Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))),
    f₁
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 _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 })))
            x) =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (δ₂ 2 _proof_2 _proof_5).op) :
            (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := _proof_2 })))
          y →
      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 })))
              x) =
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (δ₂ 0 _proof_2 _proof_5).op) :
              (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
                (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := _proof_2 })))
            y →
        f₁
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 _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 })))
              x) =
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (δ₂ 1 _proof_2 _proof_5).op) :
              (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
                (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := _proof_2 })))
            y
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
hn : HAdd.hAdd (α := ℕ) 0 1 < 2
refine_2 :
  ∀
    (x :
      X.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌ ⋯))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (σ 2 ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))) ⋯ ⋯)) ≫
            app f₀ f₁ hδ₁ hδ₀ hY
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2)
                  ⦋HAdd.hAdd (α := ℕ) 0 1 + 1⦌ ⋯))))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (app f₀ f₁ hδ₁ hδ₀ hY
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                  ⋯)) ≫
            Y.map (Quiver.Hom.op (σ 2 ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))) ⋯ ⋯))))
        x
⊢ naturalityProperty f₀ f₁ hδ₁ hδ₀ hY (Y :=
    ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌ ⋯)
    (σ 2 ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) ⋯ ⋯)

Tactic:
ext