case hom_inv_id
B : Type u
inst : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst_1 : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)
B : Type u
inst✝¹ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ inv (η ▷ h) = inv η ▷ h
aesop_cat_nonterminal
no goals
case hom_inv_id
B : Type u
inst : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst_1 : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)
simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]