[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ⊗≫ θ = η ≫ θ
[PROOFSTEP]
dsimp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ≫ 𝟙 g ≫ θ = η ≫ θ
[PROOFSTEP]
simp
