[GOAL]
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)
[PROOFSTEP]
cases η
[GOAL]
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)
[PROOFSTEP]
simp only [whiskerLeft_id, eqToHom_refl]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f = g
h : b ⟶ c
⊢ eqToHom η ▷ h = eqToHom (_ : f ≫ h = g ≫ h)
[PROOFSTEP]
cases η
[GOAL]
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
h : b ⟶ c
⊢ eqToHom (_ : f = f) ▷ h = eqToHom (_ : f ≫ h = f ≫ h)
[PROOFSTEP]
simp only [id_whiskerRight, eqToHom_refl]
