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 : C
hB : B ∈ Functor.essImage i
f : i.obj ((leftAdjoint i).obj A) ⟶ B
⊢ ↑(unitCompPartialBijective A hB).symm f = (ofRightAdjoint i).unit.app A ≫ f
simp [unitCompPartialBijective, unitCompPartialBijectiveAux_symm_apply]