case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ eqToHom (_ : g = g) = eqToHom (_ : f ≫ g = f ≫ g)
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g = h
⊢ f ◁ eqToHom η = eqToHom (_ : f ≫ g = f ≫ h)
cases η
no goals
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ eqToHom (_ : g = g) = eqToHom (_ : f ≫ g = f ≫ g)
simp only [whiskerLeft_id, eqToHom_refl]