-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
theorem nerve₂Adj.counit.naturality {C D : Type u} [SmallCategory C] [SmallCategory D]
    (F : C ⥤ D) :
    (nerveFunctor₂ ⋙ hoFunctor₂).map F ⋙ nerve₂Adj.counit.app D =
      nerve₂Adj.counit.app C ⋙ F

Proof state:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ (oneTruncation₂ ⋙ Cat.freeRefl).map (nerveFunctor₂.map F) ⋙
      HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of D)) ⋙ app D =
    HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ app C ⋙ F

Tactic:
rw [nerve₂Adj.counit.app_eq D]

Result:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ (oneTruncation₂ ⋙ Cat.freeRefl).map (nerveFunctor₂.map F) ⋙
      (whiskerRight OneTruncation₂.ofNerve₂.natIso.hom Cat.freeRefl ≫ ReflQuiv.adj.counit).app (Cat.of D) =
    HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ app C ⋙ F

Proof state:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ (oneTruncation₂ ⋙ Cat.freeRefl).map (nerveFunctor₂.map F) ⋙
      (whiskerRight OneTruncation₂.ofNerve₂.natIso.hom Cat.freeRefl ≫ ReflQuiv.adj.counit).app (Cat.of D) =
    (whiskerRight OneTruncation₂.ofNerve₂.natIso.hom Cat.freeRefl ≫ ReflQuiv.adj.counit).app (Cat.of C) ⋙ F

Tactic:
exact (whiskerRight OneTruncation₂.ofNerve₂.natIso.{u}.hom Cat.freeRefl ≫
  ReflQuiv.adj.counit).naturality _

Result:
no goals

Proof state:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ (nerveFunctor₂ ⋙ hoFunctor₂).map F ⋙ app D =
    HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ app C ⋙ F

Tactic:
change ((oneTruncation₂ ⋙ Cat.freeRefl).map (nerveFunctor₂.map _)) ⋙
  HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of D)) ⋙ app D = _

Result:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ (oneTruncation₂ ⋙ Cat.freeRefl).map (nerveFunctor₂.map F) ⋙
      HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of D)) ⋙ app D =
    HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ app C ⋙ F

Proof state:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ (nerveFunctor₂ ⋙ hoFunctor₂).map F ⋙ app D = app C ⋙ F

Tactic:
apply HomotopyCategory.lift_unique'

Result:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ (nerveFunctor₂ ⋙ hoFunctor₂).map F ⋙ app D =
    HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ app C ⋙ F

Proof state:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ (oneTruncation₂ ⋙ Cat.freeRefl).map (nerveFunctor₂.map F) ⋙
      (whiskerRight OneTruncation₂.ofNerve₂.natIso.hom Cat.freeRefl ≫ ReflQuiv.adj.counit).app (Cat.of D) =
    HomotopyCategory.quotientFunctor (nerveFunctor₂.obj (Cat.of C)) ⋙ app C ⋙ F

Tactic:
rw [← Functor.assoc _ _ F, nerve₂Adj.counit.app_eq C]

Result:
case h
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
⊢ (oneTruncation₂ ⋙ Cat.freeRefl).map (nerveFunctor₂.map F) ⋙
      (whiskerRight OneTruncation₂.ofNerve₂.natIso.hom Cat.freeRefl ≫ ReflQuiv.adj.counit).app (Cat.of D) =
    (whiskerRight OneTruncation₂.ofNerve₂.natIso.hom Cat.freeRefl ≫ ReflQuiv.adj.counit).app (Cat.of C) ⋙ F