no goals
B : Type u
inst✝ : Bicategory B
a b c d e : B
⊢ (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom
rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
    rightUnitor_comp, rightUnitor_naturality]