-- 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
⊢ HEq (ComposableArrows.hom (F.map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }).edge)
    (ComposableArrows.hom (F.map g).edge)

Tactic:
obtain ⟨g, rfl, rfl⟩ := g

Result:
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)

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

Tactic:
rw [g.tgt_eq]

Result:
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 Y).obj 0 = ComposableArrows.right (F.map g).edge

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

Tactic:
exact ComposableArrows.ext₀ 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 ((oneTruncation₂.map (toNerve₂.mk' F hyp)).map g) (F.map g)

Tactic:
simp [oneTruncation₂]

Result:
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)

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
⊢ 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)

Tactic:
simp [OneTruncation₂.nerveHomEquiv]

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 (ComposableArrows.hom (F.map { edge := g.edge, src_eq := ⋯, tgt_eq := ⋯ }).edge)
    (ComposableArrows.hom (F.map g).edge)

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

Tactic:
exact ComposableArrows.ext₀ 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₂ φ)
⊢ oneTruncation₂.map (toNerve₂.mk' F hyp) = F

Tactic:
refine ReflPrefunctor.ext (fun _ ↦ ComposableArrows.ext₀ rfl)
  (fun X Y g ↦ eq_of_heq (heq_eqRec_iff_heq.2 <| heq_eqRec_iff_heq.2 ?_))

Result:
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 ((oneTruncation₂.map (toNerve₂.mk' F hyp)).map g) (F.map g)