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

Proof state:
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

Tactic:
rw [g.src_eq]

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).obj 0 = ComposableArrows.left (F.map g).edge

Proof state:
case refine_3.edge.w.mk
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₂ φ)
g : X.obj (op { obj := [1], property := ⋯ })
⊢ HEq
    (ComposableArrows.hom
      (F.map { edge := { edge := g, src_eq := ⋯, tgt_eq := ⋯ }.edge, src_eq := ⋯, tgt_eq := ⋯ }).edge)
    (ComposableArrows.hom (F.map { edge := g, src_eq := ⋯, tgt_eq := ⋯ }).edge)

Tactic:
rfl

Result:
no goals

Proof state:
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
    {
      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:
refine Quiver.heq_of_homOfEq_ext ?_ ?_ (f' := F.map g) ?_

Result:
case refine_1
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)).obj X) = F.obj X

case refine_2
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)).obj Y) = F.obj Y

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 := ⋯ }
      ?refine_1 ?refine_2 =
    F.map g