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 : A ⟶ B
⊢ ↑(unitCompPartialBijective A hB') (f ≫ h) = ↑(unitCompPartialBijective A hB) f ≫ h
rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h, Equiv.symm_apply_apply]