-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
@[reassoc]
lemma nerve₂Adj.unit.naturality {X Y : SSet.Truncated.{u} 2} (f : X ⟶ Y) :
    f ≫ unit.app Y = unit.app X ≫ nerveFunctor₂.map (hoFunctor₂.map f) :=
  toNerve₂.ext _ _ (by
    have := (OneTruncation₂.ofNerve₂.natIso).inv.naturality (hoFunctor₂.map f)
    dsimp at this ⊢
    rw [Functor.map_comp, Functor.map_comp, nerve₂Adj.unit.map_app_eq,
      nerve₂Adj.unit.map_app_eq, ← ReflQuiv.comp_eq_comp (Y := ReflQuiv.of _),
      ← ReflQuiv.comp_eq_comp (Y := ReflQuiv.of _), assoc, ← this]
    rfl)

Proof state:
X Y : SSet.Truncated 2
f : X ⟶ Y
this :
  ReflQuiv.forget.map (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj X) ≫ (nerveFunctor₂ ⋙ oneTruncation₂).map (hoFunctor₂.map f)
⊢ oneTruncation₂.map (f ≫ app Y) = oneTruncation₂.map (app X ≫ nerveFunctor₂.map (hoFunctor₂.map f))

Tactic:
dsimp at this ⊢

Result:
X Y : SSet.Truncated 2
f : X ⟶ Y
this :
  toReflPrefunctor (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj X) ≫
      oneTruncation₂.map (nerveFunctor₂.map (hoFunctor₂.map f))
⊢ oneTruncation₂.map (f ≫ app Y) = oneTruncation₂.map (app X ≫ nerveFunctor₂.map (hoFunctor₂.map f))

Proof state:
X Y : SSet.Truncated 2
f : X ⟶ Y
this :
  toReflPrefunctor (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj X) ≫
      oneTruncation₂.map (nerveFunctor₂.map (hoFunctor₂.map f))
⊢ oneTruncation₂.map f ≫
      (ReflQuiv.adj.unit.app (oneTruncation₂.obj Y) ⋙rq (HomotopyCategory.quotientFunctor Y).toReflPrefunctor) ≫
        OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    (ReflQuiv.adj.unit.app (oneTruncation₂.obj X) ⋙rq (HomotopyCategory.quotientFunctor X).toReflPrefunctor) ≫
      toReflPrefunctor (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y)

Tactic:
rfl

Result:
no goals

Proof state:
X Y : SSet.Truncated 2
f : X ⟶ Y
⊢ oneTruncation₂.map (f ≫ app Y) = oneTruncation₂.map (app X ≫ nerveFunctor₂.map (hoFunctor₂.map f))

Tactic:
have := (OneTruncation₂.ofNerve₂.natIso).inv.naturality (hoFunctor₂.map f)

Result:
X Y : SSet.Truncated 2
f : X ⟶ Y
this :
  ReflQuiv.forget.map (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj X) ≫ (nerveFunctor₂ ⋙ oneTruncation₂).map (hoFunctor₂.map f)
⊢ oneTruncation₂.map (f ≫ app Y) = oneTruncation₂.map (app X ≫ nerveFunctor₂.map (hoFunctor₂.map f))

Proof state:
X Y : SSet.Truncated 2
f : X ⟶ Y
this :
  toReflPrefunctor (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj X) ≫
      oneTruncation₂.map (nerveFunctor₂.map (hoFunctor₂.map f))
⊢ oneTruncation₂.map (f ≫ app Y) = oneTruncation₂.map (app X ≫ nerveFunctor₂.map (hoFunctor₂.map f))

Tactic:
rw [Functor.map_comp, Functor.map_comp, nerve₂Adj.unit.map_app_eq,
  nerve₂Adj.unit.map_app_eq, ← ReflQuiv.comp_eq_comp (Y := ReflQuiv.of _),
  ← ReflQuiv.comp_eq_comp (Y := ReflQuiv.of _), assoc, ← this]

Result:
X Y : SSet.Truncated 2
f : X ⟶ Y
this :
  toReflPrefunctor (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj X) ≫
      oneTruncation₂.map (nerveFunctor₂.map (hoFunctor₂.map f))
⊢ oneTruncation₂.map f ≫
      (ReflQuiv.adj.unit.app (oneTruncation₂.obj Y) ⋙rq (HomotopyCategory.quotientFunctor Y).toReflPrefunctor) ≫
        OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y) =
    (ReflQuiv.adj.unit.app (oneTruncation₂.obj X) ⋙rq (HomotopyCategory.quotientFunctor X).toReflPrefunctor) ≫
      toReflPrefunctor (hoFunctor₂.map f) ≫ OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj Y)