[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)
[PROOFSTEP]
rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)
[PROOFSTEP]
rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)
[PROOFSTEP]
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)
[PROOFSTEP]
rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]
[GOAL]
B : Type u
inst✝¹ : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ inv (f ◁ η) = f ◁ inv η
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
B : Type u
inst : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst_1 : IsIso η
⊢ f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)
[PROOFSTEP]
simp only [← whiskerLeft_comp, whiskerLeft_id, IsIso.hom_inv_id]
[GOAL]
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
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
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)
[PROOFSTEP]
simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i) =
    inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv
[PROOFSTEP]
rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom) =
    inv ((α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i
[PROOFSTEP]
simp [← cancel_epi (f ◁ (α_ g h i).inv)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv) =
    inv ((α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i
[PROOFSTEP]
rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ ((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i =
    ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) =
    inv ((α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom
[PROOFSTEP]
simp [← cancel_epi ((α_ f g h).hom ▷ i)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) =
    inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom
[PROOFSTEP]
rw [← triangle, inv_hom_id_assoc]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv
[PROOFSTEP]
simp [← cancel_mono (f ◁ (λ_ g).hom)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g
[PROOFSTEP]
simp [← cancel_mono ((ρ_ f).hom ▷ g)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom
[PROOFSTEP]
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ← cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc,
  triangle, ← associator_naturality_middle, ← comp_whiskerRight_assoc, triangle, associator_naturality_left]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ inv ((λ_ f).inv ▷ g) = inv ((λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
[PROOFSTEP]
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ← cancel_epi (f ◁ (α_ _ _ _).inv),
  pentagon_inv_assoc, triangle_assoc_comp_right, ← associator_inv_naturality_middle, ← whiskerLeft_comp_assoc,
  triangle_assoc_comp_right, associator_inv_naturality_right]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ inv (f ◁ (ρ_ g).inv) = inv ((ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
⊢ (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom
[PROOFSTEP]
rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ← rightUnitor_comp,
  rightUnitor_naturality]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
⊢ (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv
[PROOFSTEP]
simp [Iso.inv_eq_inv]
