[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ (downFunctor ⋙ upFunctor).map f ≫ (fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) Y =
    (fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) X ≫ (𝟭 (ULift C)).map f
[PROOFSTEP]
change f ≫ 𝟙 _ = 𝟙 _ ≫ f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ (𝟭 (ULift C)).map f ≫ (fun X => 𝟙 ((𝟭 (ULift C)).obj X)) Y =
    (fun X => 𝟙 ((𝟭 (ULift C)).obj X)) X ≫ (downFunctor ⋙ upFunctor).map f
[PROOFSTEP]
change f ≫ 𝟙 _ = 𝟙 _ ≫ f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) =
    𝟙 (downFunctor ⋙ upFunctor)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ NatTrans.app
      ((NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) x✝ =
    NatTrans.app (𝟙 (downFunctor ⋙ upFunctor)) x✝
[PROOFSTEP]
change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ 𝟙 ((downFunctor ⋙ upFunctor).obj x✝) ≫ 𝟙 ((downFunctor ⋙ upFunctor).obj x✝) = 𝟙 ((downFunctor ⋙ upFunctor).obj x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) =
    𝟙 (𝟭 (ULift C))
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ NatTrans.app
      ((NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) x✝ =
    NatTrans.app (𝟙 (𝟭 (ULift C))) x✝
[PROOFSTEP]
change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ 𝟙 ((𝟭 (ULift C)).obj x✝) ≫ 𝟙 ((𝟭 (ULift C)).obj x✝) = 𝟙 ((𝟭 (ULift C)).obj x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ upFunctor.map (NatTrans.app (Iso.mk (𝟙 (𝟭 C)) (𝟙 (upFunctor ⋙ downFunctor))).hom X) ≫
      NatTrans.app
        (Iso.mk (NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X))
            (NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X))).hom
        (upFunctor.obj X) =
    𝟙 (upFunctor.obj X)
[PROOFSTEP]
change 𝟙 X ≫ 𝟙 X = 𝟙 X
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
simp
