C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (ofRightAdjoint i).unit.app (i.obj ((leftAdjoint i).obj X)) ≫
      i.map ((ofRightAdjoint i).counit.app ((leftAdjoint i).obj X)) =
    i.map ((leftAdjoint i).map ((ofRightAdjoint i).unit.app X) ≫ (ofRightAdjoint i).counit.app ((leftAdjoint i).obj X))
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (ofRightAdjoint i).unit.app (i.obj ((leftAdjoint i).obj X)) =
    i.map ((leftAdjoint i).map ((ofRightAdjoint i).unit.app X))
rw [← cancel_mono (i.map ((ofRightAdjoint i).counit.app ((leftAdjoint i).obj X))), ←
  i.map_comp]
no goals
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (ofRightAdjoint i).unit.app (i.obj ((leftAdjoint i).obj X)) ≫
      i.map ((ofRightAdjoint i).counit.app ((leftAdjoint i).obj X)) =
    i.map ((leftAdjoint i).map ((ofRightAdjoint i).unit.app X) ≫ (ofRightAdjoint i).counit.app ((leftAdjoint i).obj X))
simp