-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
theorem oneTruncation₂_toNerve₂Mk' : oneTruncation₂.map (toNerve₂.mk' F hyp) = F

Proof state:
case refine_3.edge.w
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ ((F.obj (X✝.map (δ₂ 1 ⋯ ⋯).op g.edge)).nerveHomEquiv (F.obj (X✝.map (δ₂ 0 ⋯ ⋯).op g.edge)))
      (F.map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }) =
    eqToHom ⋯ ≫ ComposableArrows.hom (F.map g).edge ≫ eqToHom ⋯

Tactic:
refine (conj_eqToHom_iff_heq' _ _ _ _).2 ?_

Result:
case refine_3.edge.w
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ HEq
    (((F.obj (X✝.map (δ₂ 1 ⋯ ⋯).op g.edge)).nerveHomEquiv (F.obj (X✝.map (δ₂ 0 ⋯ ⋯).op g.edge)))
      (F.map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }))
    (ComposableArrows.hom (F.map g).edge)

Proof state:
case refine_3.edge
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ ComposableArrows.mk₁
      ((F ≫ OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C)).map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }) =
    (F.map g).edge

Tactic:
fapply ComposableArrows.ext₁ <;> simp [ReflQuiv.comp_eq_comp]

Result:
case refine_3.edge.left
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ (F.obj (X✝.map (δ₂ 1 ⋯ ⋯).op g.edge)).obj 0 = ComposableArrows.left (F.map g).edge

case refine_3.edge.right
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ (F.obj (X✝.map (δ₂ 0 ⋯ ⋯).op g.edge)).obj 0 = ComposableArrows.right (F.map g).edge

case refine_3.edge.w
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ ((F.obj (X✝.map (δ₂ 1 ⋯ ⋯).op g.edge)).nerveHomEquiv (F.obj (X✝.map (δ₂ 0 ⋯ ⋯).op g.edge)))
      (F.map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }) =
    eqToHom ⋯ ≫ ComposableArrows.hom (F.map g).edge ≫ eqToHom ⋯

Proof state:
case refine_3
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ Quiver.homOfEq
      {
        edge :=
          ComposableArrows.mk₁
            ((F ≫ OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C)).map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }),
        src_eq := ⋯, tgt_eq := ⋯ }
      ⋯ ⋯ =
    F.map g

Tactic:
apply OneTruncation₂.Hom.ext

Result:
case refine_3.edge
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ (Quiver.homOfEq
        {
          edge :=
            ComposableArrows.mk₁
              ((F ≫ OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C)).map
                { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }),
          src_eq := ⋯, tgt_eq := ⋯ }
        ⋯ ⋯).edge =
    (F.map g).edge

Proof state:
case refine_3.edge
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ (Quiver.homOfEq
        {
          edge :=
            ComposableArrows.mk₁
              ((F ≫ OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C)).map
                { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }),
          src_eq := ⋯, tgt_eq := ⋯ }
        ⋯ ⋯).edge =
    (F.map g).edge

Tactic:
simp only [oneTruncation₂_obj, ReflQuiv.of_val, OneTruncation₂.homOfEq_edge]

Result:
case refine_3.edge
C : Type u
inst✝ : SmallCategory C
X✝ : SSet.Truncated 2
F : oneTruncation₂.obj X✝ ⟶ oneTruncation₂.obj (nerveFunctor₂.obj (Cat.of C))
hyp :
  ∀ (φ : X✝.obj (op { obj := [2], property := ⋯ })),
    (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev02₂ φ) =
      (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev01₂ φ) ≫
        (F ≫ (OneTruncation₂.ofNerve₂.natIso.app (Cat.of C)).hom).map (ev12₂ φ)
X Y : ↑(oneTruncation₂.obj X✝)
g : X ⟶ Y
⊢ ComposableArrows.mk₁
      ((F ≫ OneTruncation₂.ofNerve₂.natIso.hom.app (Cat.of C)).map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }) =
    (F.map g).edge