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
A B B' : C
h : B ⟶ B'
hB : B ∈ Functor.essImage i
hB' : B' ∈ Functor.essImage i
f : i.obj ((leftAdjoint i).obj A) ⟶ B
⊢ ↑(unitCompPartialBijective A hB').symm (f ≫ h) = ↑(unitCompPartialBijective A hB).symm f ≫ h
simp