awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (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₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₁ :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    Path.arrow
        (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
          (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
        i =
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow i
⊢ spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))) =
    spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (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₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h₁ :
  Path.arrow
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))
h₃ :
  Path.arrow
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩) =
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))
⊢ Path.arrow
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
      i =
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow i

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (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₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C))
            (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 2) ⋯ _proof_4))) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_4 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))) =
    ComposableArrows.mk₁ (F.map (homMk e₀₁))

Tactic:
apply nerve.δ₂_mk₂_eq

Premises used: CategoryTheory.nerve.δ₂_mk₂_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (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₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C))
            (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 0) ⋯ _proof_4))) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_4 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))) =
    ComposableArrows.mk₁ (F.map (homMk e₁₂))

Tactic:
apply nerve.δ₀_mk₂_eq

Premises used: CategoryTheory.nerve.δ₀_mk₂_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
⊢ F.mapArrow.obj (Arrow.mk (homMk (Edge.id x))) =
    (ComposableArrows.arrowEquiv : (a : ComposableArrows C 1) → Arrow C)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (σ₂ 0 _proof_3 _proof_1).op) :
          (a : (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := _proof_3 })))
        ((fun
              (x :
                X.obj
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) ↦
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) (F.obj (mk x)) : ComposableArrows C 0))
          x))

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
F : X.HomotopyCategory ⥤ C
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((homToNerveMk F).app
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 })))
        x :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))
    ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) (F.obj (mk x)) : ComposableArrows C 0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
F : X.HomotopyCategory ⥤ C
f : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((homToNerveMk F).app
            (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := _proof_2 }))) →
          (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 })))
      f =
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f)))

Tactic:
rfl

Premises used: rfl, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
F : X.HomotopyCategory ⥤ C
x y : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
e : Edge x y
⊢ ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))

Tactic:
ComposableArrows.arrowEquiv.injective
    (congr_arg F.mapArrow.obj (congr_arrowMk_homMk (Edge.mk' e.edge) e rfl))

Premises used: SSet.Truncated.Edge.edge, CategoryTheory.ComposableArrows.arrowEquiv, SSet.Truncated.Edge.mk', congr_arg, SSet.Truncated.HomotopyCategory.congr_arrowMk_homMk, Equiv.injective, CategoryTheory.Functor.mapArrow, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
F : X.HomotopyCategory ⥤ C
x y : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
e : Edge x y
⊢ ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))

Tactic:
exact ComposableArrows.arrowEquiv.injective
    (congr_arg F.mapArrow.obj (congr_arrowMk_homMk (Edge.mk' e.edge) e rfl))

Premises used: CategoryTheory.ComposableArrows.arrowEquiv, Equiv.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ (descOfTruncation (homToNerveMk F)).obj (mk x) = F.obj (mk x)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
f : Edge x y
dsimp :
  (descOfTruncation (homToNerveMk F)).map (homMk f) =
    𝟙
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) (F.obj (mk x)) : ComposableArrows C 0)) ≫
      F.map (homMk f) ≫ 𝟙 (F.obj (mk y))
⊢ (descOfTruncation (homToNerveMk F)).map (homMk f) = eqToHom ⋯ ≫ F.map (homMk f) ≫ eqToHom ⋯

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
f : Edge x y
simp :
  (nerve.homEquiv :
        (a :
            SSet.Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk x)))
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk y)))) →
          (nerveEquiv : (a : ComposableArrows C 0) → C)
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk x))) ⟶
            (nerveEquiv : (a : ComposableArrows C 0) → C)
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk y))))
      (f.map (homToNerveMk F)) =
    F.map (homMk f)
⊢ (descOfTruncation (homToNerveMk F)).map (homMk f) =
    𝟙
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) (F.obj (mk x)) : ComposableArrows C 0)) ≫
      F.map (homMk f) ≫ 𝟙 (F.obj (mk y))

Tactic:
simp only [Category.comp_id, Category.id_comp, descOfTruncation_map_homMk,
        homToNerveMk_app_zero]

Premises used: CategoryTheory.Category.comp_id, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
f : Edge x y
⊢ (nerve.homEquiv :
        (a :
            SSet.Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk x)))
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk y)))) →
          (nerveEquiv : (a : ComposableArrows C 0) → C)
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk x))) ⟶
            (nerveEquiv : (a : ComposableArrows C 0) → C)
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk y))))
      (f.map (homToNerveMk F)) =
    F.map (homMk f)

Tactic:
exact nerve.homEquiv.symm.injective (Edge.ext (by cat_disch))

Premises used: SSet.Truncated.Edge.ext, CategoryTheory.nerve.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : X ⟶ Functor.obj (truncation 2) (nerve C)
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
refine_1 :
  Eq.{u + 1} (α := C)
    (Functor.obj (C := Fin 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2)
                      ⦋HAdd.hAdd (α := ℕ) 0 1⦌ Edge._proof_3))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))
            f.edge :
          Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                Edge._proof_3))))
      0)
    (ComposableArrows.left (n := 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge))
⊢ Eq.{u + 1} (α := C)
    (Functor.obj (C := Fin 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : X.obj (op { obj := ⦋0⦌, property := _proof_1 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        x₀)
      0)
    (ComposableArrows.left (n := 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge))

Tactic:
simp only [← f.src_eq, NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, SSet.Truncated.Edge.src_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : X ⟶ Functor.obj (truncation 2) (nerve C)
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
⊢ Eq.{u + 1} (α := C)
    (Functor.obj (C := Fin 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2)
                      ⦋HAdd.hAdd (α := ℕ) 0 1⦌ Edge._proof_3))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))
            f.edge :
          Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                Edge._proof_3))))
      0)
    (ComposableArrows.left (n := 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : X ⟶ Functor.obj (truncation 2) (nerve C)
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
refine_2 :
  Eq.{u + 1} (α := C)
    (Functor.obj (C := Fin 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2)
                      ⦋HAdd.hAdd (α := ℕ) 0 1⦌ Edge._proof_3))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))
            f.edge :
          Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                Edge._proof_3))))
      0)
    (Functor.obj (C := Fin 2)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge)
      1)
⊢ Eq.{u + 1} (α := C)
    (Functor.obj (C := Fin 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : X.obj (op { obj := ⦋0⦌, property := _proof_1 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        x₁)
      0)
    (Functor.obj (C := Fin 2)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge)
      1)

Tactic:
simp only [← f.tgt_eq, NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, SSet.Truncated.Edge.tgt_eq