diff --git a/src/category_theory/bicategory/basic.lean b/src/category_theory/bicategory/basic.lean
index cf03afb4d6cc0..3ab618c76cae9 100644
--- a/src/category_theory/bicategory/basic.lean
+++ b/src/category_theory/bicategory/basic.lean
@@ -60,118 +60,139 @@ class bicategory (B : Type u) extends category_struct.{v} B :=
 (hom_category : ∀ (a b : B), category.{w} (a ⟶ b) . tactic.apply_instance)
 -- left whiskering:
 (whisker_left {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) : f ≫ g ⟶ f ≫ h)
-(infixr ` ◁ `:70 := whisker_left)
--- functoriality of left whiskering:
-(whisker_left_id' : ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), f ◁ 𝟙 g = 𝟙 (f ≫ g) . obviously)
-(whisker_left_comp' :
-  ∀ {a b c} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i),
-  f ◁ (η ≫ θ) = (f ◁ η) ≫ (f ◁ θ) . obviously)
+(infixr ` ◁ `:81 := whisker_left)
 -- right whiskering:
 (whisker_right {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) : f ≫ h ⟶ g ≫ h)
-(infixr ` ▷ `:70 := whisker_right)
--- functoriality of right whiskering:
-(whisker_right_id' : ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), 𝟙 f ▷ g = 𝟙 (f ≫ g) . obviously)
-(whisker_right_comp' :
-  ∀ {a b c} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
-  (η ≫ θ) ▷ i = (η ▷ i) ≫ (θ ▷ i) . obviously)
--- exchange law of left and right whiskerings:
-(whisker_exchange' : ∀ {a b c} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i),
-  (f ◁ θ) ≫ (η ▷ i) = (η ▷ h) ≫ (g ◁ θ) . obviously)
+(infixl ` ▷ `:81 := whisker_right)
 -- associator:
 (associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
   (f ≫ g) ≫ h ≅ f ≫ (g ≫ h))
 (notation `α_` := associator)
-(associator_naturality_left' :
-  ∀ {a b c d} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
-  ((η ▷ g) ▷ h) ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ (η ▷ (g ≫ h)) . obviously)
-(associator_naturality_middle' :
-  ∀ {a b c d} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
-  ((f ◁ η) ▷ h) ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ (f ◁ (η ▷ h)) . obviously)
-(associator_naturality_right' :
-  ∀ {a b c d} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
-  ((f ≫ g) ◁ η) ≫ (α_ f g h').hom = (α_ f g h).hom ≫ (f ◁ (g ◁ η)) . obviously)
 --left unitor:
 (left_unitor {a b : B} (f : a ⟶ b) : 𝟙 a ≫ f ≅ f)
 (notation `λ_` := left_unitor)
-(left_unitor_naturality' : ∀ {a b} {f f' : a ⟶ b} (η : f ⟶ f'),
-  (𝟙 a ◁ η) ≫ (λ_ f').hom = (λ_ f).hom ≫ η . obviously)
 -- right unitor:
 (right_unitor {a b : B} (f : a ⟶ b) : f ≫ 𝟙 b ≅ f)
 (notation `ρ_` := right_unitor)
-(right_unitor_naturality' : ∀ {a b} {f f' : a ⟶ b} (η : f ⟶ f'),
-  (η ▷ 𝟙 b) ≫ (ρ_ f').hom = (ρ_ f).hom ≫ η . obviously)
+-- axioms for left whiskering:
+(whisker_left_id' : ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c),
+  f ◁ 𝟙 g = 𝟙 (f ≫ g) . obviously)
+(whisker_left_comp' : ∀ {a b c} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i),
+  f ◁ (η ≫ θ) = f ◁ η ≫ f ◁ θ . obviously)
+(id_whisker_left' : ∀ {a b} {f g : a ⟶ b} (η : f ⟶ g),
+  𝟙 a ◁ η = (λ_ f).hom ≫ η ≫ (λ_ g).inv . obviously)
+(comp_whisker_left' : ∀ {a b c d} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
+  (f ≫ g) ◁ η = (α_ f g h).hom ≫ f ◁ g ◁ η ≫ (α_ f g h').inv . obviously)
+-- axioms for right whiskering:
+(id_whisker_right' : ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c),
+  𝟙 f ▷ g = 𝟙 (f ≫ g) . obviously)
+(comp_whisker_right' : ∀ {a b c} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
+  (η ≫ θ) ▷ i = η ▷ i ≫ θ ▷ i . obviously)
+(whisker_right_id' : ∀ {a b} {f g : a ⟶ b} (η : f ⟶ g),
+  η ▷ 𝟙 b = (ρ_ f).hom ≫ η ≫ (ρ_ g).inv . obviously)
+(whisker_right_comp' : ∀ {a b c d} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
+  η ▷ (g ≫ h) = (α_ f g h).inv ≫ η ▷ g ▷ h ≫ (α_ f' g h).hom . obviously)
+-- associativity of whiskerings:
+(whisker_assoc' : ∀ {a b c d} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
+  (f ◁ η) ▷ h = (α_ f g h).hom ≫ f ◁ (η ▷ h) ≫ (α_ f g' h).inv . obviously)
+-- exchange law of left and right whiskerings:
+(whisker_exchange' : ∀ {a b c} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i),
+  f ◁ θ ≫ η ▷ i = η ▷ h ≫ g ◁ θ . obviously)
 -- pentagon identity:
 (pentagon' : ∀ {a b c d e} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
-  ((α_ f g h).hom ▷ i) ≫ (α_ f (g ≫ h) i).hom ≫ (f ◁ (α_ g h i).hom) =
+  (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom =
     (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom . obviously)
 -- triangle identity:
 (triangle' : ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c),
-  (α_ f (𝟙 b) g).hom ≫ (f ◁ (λ_ g).hom) = (ρ_ f).hom ▷ g . obviously)
-
-restate_axiom bicategory.whisker_left_id'
-restate_axiom bicategory.whisker_left_comp'
-restate_axiom bicategory.whisker_right_id'
-restate_axiom bicategory.whisker_right_comp'
-restate_axiom bicategory.whisker_exchange'
-restate_axiom bicategory.associator_naturality_left'
-restate_axiom bicategory.associator_naturality_middle'
-restate_axiom bicategory.associator_naturality_right'
-restate_axiom bicategory.left_unitor_naturality'
-restate_axiom bicategory.right_unitor_naturality'
-restate_axiom bicategory.pentagon'
-restate_axiom bicategory.triangle'
-attribute [simp]
-  bicategory.whisker_left_id bicategory.whisker_right_id
-  bicategory.whisker_exchange bicategory.triangle
-attribute [reassoc]
-  bicategory.whisker_left_comp bicategory.whisker_right_comp
-  bicategory.whisker_exchange bicategory.associator_naturality_left
-  bicategory.associator_naturality_middle bicategory.associator_naturality_right
-  bicategory.left_unitor_naturality bicategory.right_unitor_naturality
-  bicategory.pentagon bicategory.triangle
-attribute [simp] bicategory.whisker_left_comp bicategory.whisker_right_comp
-attribute [instance] bicategory.hom_category
-
-localized "infixr ` ◁ `:70 := bicategory.whisker_left" in bicategory
-localized "infixr ` ▷ `:70 := bicategory.whisker_right" in bicategory
+  (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = (ρ_ f).hom ▷ g . obviously)
+
+-- The precedence of the whiskerings is higher than that of the composition `≫`.
+localized "infixr ` ◁ `:81 := bicategory.whisker_left" in bicategory
+localized "infixl ` ▷ `:81 := bicategory.whisker_right" in bicategory
 localized "notation `α_` := bicategory.associator" in bicategory
 localized "notation `λ_` := bicategory.left_unitor" in bicategory
 localized "notation `ρ_` := bicategory.right_unitor" in bicategory
 
 namespace bicategory
 
-section
+/-!
+### Simp-normal form for 2-morphisms
+
+Rewriting involving associators and unitors could be very complicated. We try to ease this
+complexity by putting carefully chosen simp lemmas that rewrite any 2-morphisms into simp-normal
+form defined below. Rewriting into simp-normal form is also useful when applying (forthcoming)
+`coherence` tactic.
+
+The simp-normal form of 2-morphisms is defined to be an expression that has the minimal number of
+parentheses. More precisely,
+1. it is a composition of 2-morphisms like `η₁ ≫ η₂ ≫ η₃ ≫ η₄ ≫ η₅` such that each `ηᵢ` is
+  either a structural 2-morphisms (2-morphisms made up only of identities, associators, unitors)
+  or non-structural 2-morphisms, and
+2. each non-structural 2-morphism in the composition is of the form `f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅`,
+  where each `fᵢ` is a 1-morphism that is not the identity or a composite and `η` is a
+  non-structural 2-morphisms that is also not the identity or a composite.
+
+Note that `f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅` is actually `f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅)))`.
+-/
+
+restate_axiom whisker_left_id'
+restate_axiom whisker_left_comp'
+restate_axiom id_whisker_left'
+restate_axiom comp_whisker_left'
+restate_axiom id_whisker_right'
+restate_axiom comp_whisker_right'
+restate_axiom whisker_right_id'
+restate_axiom whisker_right_comp'
+restate_axiom whisker_assoc'
+restate_axiom whisker_exchange'
+restate_axiom pentagon'
+restate_axiom triangle'
+
+attribute [simp]  pentagon triangle
+attribute [reassoc]
+  whisker_left_comp id_whisker_left comp_whisker_left
+  comp_whisker_right whisker_right_id whisker_right_comp
+  whisker_assoc whisker_exchange pentagon triangle
+/-
+The following simp attributes are put in order to rewrite any 2-morphisms into normal forms. There
+are associators and unitors in the RHS in the several simp lemmas here (e.g. `id_whisker_left`),
+which at first glance look more complicated than the LHS, but they will be eventually reduced by the
+pentagon or the triangle identities, and more generally, (forthcoming) `coherence` tactic.
+-/
+attribute [simp]
+  whisker_left_id whisker_left_comp id_whisker_left comp_whisker_left
+  id_whisker_right comp_whisker_right whisker_right_id whisker_right_comp
+  whisker_assoc
+attribute [instance] hom_category
 
 variables {B : Type u} [bicategory.{w v} B] {a b c d e : B}
 
 @[simp, reassoc]
 lemma hom_inv_whisker_left (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
-  (f ◁ η.hom) ≫ (f ◁ η.inv) = 𝟙 (f ≫ g) :=
+  f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g) :=
 by rw [←whisker_left_comp, hom_inv_id, whisker_left_id]
 
 @[simp, reassoc]
 lemma hom_inv_whisker_right {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
-  (η.hom ▷ h) ≫ (η.inv ▷ h) = 𝟙 (f ≫ h) :=
-by rw [←whisker_right_comp, hom_inv_id, whisker_right_id]
+  η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h) :=
+by rw [←comp_whisker_right, hom_inv_id, id_whisker_right]
 
 @[simp, reassoc]
 lemma inv_hom_whisker_left (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
-  (f ◁ η.inv) ≫ (f ◁ η.hom) = 𝟙 (f ≫ h) :=
+  f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h) :=
 by rw [←whisker_left_comp, inv_hom_id, whisker_left_id]
 
 @[simp, reassoc]
 lemma inv_hom_whisker_right {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
-  (η.inv ▷ h) ≫ (η.hom ▷ h) = 𝟙 (g ≫ h) :=
-by rw [←whisker_right_comp, inv_hom_id, whisker_right_id]
+  η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h) :=
+by rw [←comp_whisker_right, inv_hom_id, id_whisker_right]
 
 /-- The left whiskering of a 2-isomorphism is a 2-isomorphism. -/
 @[simps]
 def whisker_left_iso (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
   f ≫ g ≅ f ≫ h :=
 { hom := f ◁ η.hom,
-  inv := f ◁ η.inv,
-  hom_inv_id' := by simp only [hom_inv_whisker_left],
-  inv_hom_id' := by simp only [inv_hom_whisker_left] }
+  inv := f ◁ η.inv }
 
 instance whisker_left_is_iso (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [is_iso η] :
   is_iso (f ◁ η) :=
@@ -187,9 +208,7 @@ by { ext, simp only [←whisker_left_comp, whisker_left_id, is_iso.hom_inv_id] }
 def whisker_right_iso {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
   f ≫ h ≅ g ≫ h :=
 { hom := η.hom ▷ h,
-  inv := η.inv ▷ h,
-  hom_inv_id' := by simp only [hom_inv_whisker_right],
-  inv_hom_id' := by simp only [inv_hom_whisker_right] }
+  inv := η.inv ▷ h }
 
 instance whisker_right_is_iso {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [is_iso η] :
   is_iso (η ▷ h) :=
@@ -198,255 +217,228 @@ is_iso.of_iso (whisker_right_iso (as_iso η) h)
 @[simp]
 lemma inv_whisker_right {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [is_iso η] :
   inv (η ▷ h) = (inv η) ▷ h :=
-by { ext, simp only [←whisker_right_comp, whisker_right_id, is_iso.hom_inv_id] }
-
-@[reassoc]
-lemma left_unitor_inv_naturality {f f' : a ⟶ b} (η : f ⟶ f') :
-  η ≫ (λ_ f').inv = (λ_ f).inv ≫ (𝟙 a ◁ η) :=
-begin
-  apply (cancel_mono (λ_ f').hom).1,
-  simp only [assoc, comp_id, inv_hom_id, left_unitor_naturality, inv_hom_id_assoc]
-end
+by { ext, simp only [←comp_whisker_right, id_whisker_right, is_iso.hom_inv_id] }
 
-@[reassoc]
-lemma right_unitor_inv_naturality {f f' : a ⟶ b} (η : f ⟶ f') :
-  η ≫ (ρ_ f').inv = (ρ_ f ).inv ≫ (η ▷ 𝟙 b) :=
-begin
-  apply (cancel_mono (ρ_ f').hom).1,
-  simp only [assoc, comp_id, inv_hom_id, right_unitor_naturality, inv_hom_id_assoc]
-end
+@[simp, reassoc]
+lemma pentagon_inv (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)).inv ≫ (α_ (f ≫ g) h i).inv :=
+eq_of_inv_eq_inv (by simp)
 
-@[simp]
-lemma right_unitor_conjugation {f g : a ⟶ b} (η : f ⟶ g) :
-  (ρ_ f).inv ≫ (η ▷ 𝟙 b) ≫ (ρ_ g).hom = η :=
-by rw [right_unitor_naturality, inv_hom_id_assoc]
+@[simp, reassoc]
+lemma pentagon_inv_inv_hom_hom_inv (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 :=
+by { rw [←cancel_epi (f ◁ (α_ g h i).inv), ←cancel_mono (α_ (f ≫ g) h i).inv], simp }
 
-@[simp]
-lemma left_unitor_conjugation {f g : a ⟶ b} (η : f ⟶ g) :
-  (λ_ f).inv ≫ (𝟙 a ◁ η) ≫ (λ_ g).hom = η :=
-by rw [left_unitor_naturality, inv_hom_id_assoc]
+@[simp, reassoc]
+lemma pentagon_inv_hom_hom_hom_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
+  (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom =
+    (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv :=
+eq_of_inv_eq_inv (by simp)
 
-@[simp]
-lemma whisker_left_iff {f g : a ⟶ b} (η θ : f ⟶ g) :
-  (𝟙 a ◁ η = 𝟙 a ◁ θ) ↔ (η = θ) :=
-by rw [←cancel_mono (λ_ g).hom, left_unitor_naturality, left_unitor_naturality,
-    cancel_iso_hom_left]
+@[simp, reassoc]
+lemma pentagon_hom_inv_inv_inv_inv (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 :=
+by simp [←cancel_epi (f ◁ (α_ g h i).inv)]
 
-@[simp]
-lemma whisker_right_iff {f g : a ⟶ b} (η θ : f ⟶ g) :
-  (η ▷ 𝟙 b = θ ▷ 𝟙 b) ↔ (η = θ) :=
-by rw [←cancel_mono (ρ_ g).hom, right_unitor_naturality, right_unitor_naturality,
-    cancel_iso_hom_left]
+@[simp, reassoc]
+lemma pentagon_hom_hom_inv_hom_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
+  (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv =
+    (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom :=
+eq_of_inv_eq_inv (by simp)
 
-@[reassoc]
-lemma left_unitor_comp' (f : a ⟶ b) (g : b ⟶ c) :
-  (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom = (λ_ f).hom ▷ g :=
-by rw [←whisker_left_iff, whisker_left_comp, ←cancel_epi (α_ (𝟙 a) (𝟙 a ≫ f) g).hom,
-    ←cancel_epi ((α_ (𝟙 a) (𝟙 a) f).hom ▷ g), pentagon_assoc, triangle,
-    ←associator_naturality_middle, ←whisker_right_comp_assoc, triangle,
-    associator_naturality_left, cancel_iso_hom_left]
-
--- We state it as a `@[simp]` lemma. Generally, we think the component index of a natural
--- transformation "weighs more" in considering the complexity of an expression than
--- does a structural isomorphism (associator, etc).
-@[reassoc, simp]
-lemma left_unitor_comp (f : a ⟶ b) (g : b ⟶ c) :
-  (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ ((λ_ f).hom ▷ g) :=
-by { rw [←left_unitor_comp', inv_hom_id_assoc] }
+@[simp, reassoc]
+lemma pentagon_hom_inv_inv_inv_hom (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 :=
+by { rw [←cancel_epi (α_ f g (h ≫ i)).inv, ←cancel_mono ((α_ f g h).inv ▷ i)], simp }
 
-lemma left_unitor_comp_inv' (f : a ⟶ b) (g : b ⟶ c) :
-  (λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv = ((λ_ f).inv ▷ g) :=
-eq_of_inv_eq_inv (by simp only [left_unitor_comp, inv_whisker_right,
-  is_iso.iso.inv_inv, hom_inv_id_assoc, is_iso.inv_comp])
+@[simp, reassoc]
+lemma pentagon_hom_hom_inv_inv_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
+  (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv =
+    (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom :=
+eq_of_inv_eq_inv (by simp)
 
-@[reassoc, simp]
-lemma left_unitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
-  (λ_ (f ≫ g)).inv = ((λ_ f).inv ▷ g) ≫ (α_ (𝟙 a) f g).hom :=
-by { rw [←left_unitor_comp_inv'], simp only [inv_hom_id, assoc, comp_id] }
+@[simp, reassoc]
+lemma pentagon_inv_hom_hom_hom_hom (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 :=
+by simp [←cancel_epi ((α_ f g h).hom ▷ i)]
 
-@[reassoc, simp]
-lemma right_unitor_comp (f : a ⟶ b) (g : b ⟶ c) :
-  (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ (f ◁ (ρ_ g).hom) :=
-by rw [←whisker_right_iff, whisker_right_comp, ←cancel_mono (α_ f g (𝟙 c)).hom,
-    assoc, associator_naturality_middle, ←triangle_assoc, ←triangle,
-    whisker_left_comp, pentagon_assoc, ←associator_naturality_right]
+@[simp, reassoc]
+lemma pentagon_inv_inv_hom_inv_inv (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).hom ▷ i =
+    f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv :=
+eq_of_inv_eq_inv (by simp)
 
-@[reassoc, simp]
-lemma right_unitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
-  (ρ_ (f ≫ g)).inv = (f ◁ (ρ_ g).inv) ≫ (α_ f g (𝟙 c)).inv :=
-eq_of_inv_eq_inv (by simp only [inv_whisker_left, right_unitor_comp,
-  is_iso.iso.inv_inv, is_iso.inv_comp])
+lemma triangle_assoc_comp_left (f : a ⟶ b) (g : b ⟶ c) :
+  (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = (ρ_ f).hom ▷ g :=
+triangle f g
 
-@[reassoc]
-lemma whisker_left_right_unitor_inv (f : a ⟶ b) (g : b ⟶ c) :
-  f ◁ (ρ_ g).inv = (ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom :=
-by simp only [right_unitor_comp_inv, comp_id, inv_hom_id, assoc]
+@[simp, reassoc]
+lemma triangle_assoc_comp_right (f : a ⟶ b) (g : b ⟶ c) :
+  (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom :=
+by rw [←triangle, inv_hom_id_assoc]
 
-@[reassoc]
-lemma whisker_left_right_unitor (f : a ⟶ b) (g : b ⟶ c) :
-  f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom :=
-by simp only [right_unitor_comp, inv_hom_id_assoc]
+@[simp, reassoc]
+lemma triangle_assoc_comp_right_inv (f : a ⟶ b) (g : b ⟶ c) :
+  (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv :=
+by simp [←cancel_mono (f ◁ (λ_ g).hom)]
 
-@[reassoc]
-lemma left_unitor_inv_whisker_right (f : a ⟶ b) (g : b ⟶ c) :
-  (λ_ f).inv ▷ g = (λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv :=
-by simp only [left_unitor_comp_inv, assoc, comp_id, hom_inv_id]
+@[simp, reassoc]
+lemma triangle_assoc_comp_left_inv (f : a ⟶ b) (g : b ⟶ c) :
+  f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g :=
+by simp [←cancel_mono ((ρ_ f).hom ▷ g)]
 
 @[reassoc]
-lemma left_unitor_whisker_right (f : a ⟶ b) (g : b ⟶ c) :
-  (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom :=
-by simp only [left_unitor_comp, hom_inv_id_assoc]
+lemma associator_naturality_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
+  (η ▷ g) ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h) :=
+by simp
 
 @[reassoc]
 lemma associator_inv_naturality_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
-  (η ▷ (g ≫ h)) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ ((η ▷ g) ▷ h) :=
-by rw [comp_inv_eq, assoc, associator_naturality_left, inv_hom_id_assoc]
+  η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ (η ▷ g) ▷ h :=
+by simp
 
 @[reassoc]
-lemma associator_conjugation_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
-  (α_ f g h).hom ≫ (η ▷ (g ≫ h)) ≫ (α_ f' g h).inv = (η ▷ g) ▷ h :=
-by rw [associator_inv_naturality_left, hom_inv_id_assoc]
+lemma whisker_right_comp_symm {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
+  (η ▷ g) ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv :=
+by simp
 
 @[reassoc]
-lemma associator_inv_conjugation_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
-  (α_ f g h).inv ≫ ((η ▷ g) ▷ h) ≫ (α_ f' g h).hom = η ▷ (g ≫ h) :=
-by rw [associator_naturality_left, inv_hom_id_assoc]
+lemma associator_naturality_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
+  (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ (η ▷ h) :=
+by simp
 
 @[reassoc]
 lemma associator_inv_naturality_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
-  (f ◁ (η ▷ h)) ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ ((f ◁ η) ▷ h) :=
-by rw [comp_inv_eq, assoc, associator_naturality_middle, inv_hom_id_assoc]
+  f ◁ (η ▷ h) ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h :=
+by simp
 
 @[reassoc]
-lemma associator_conjugation_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
-  (α_ f g h).hom ≫ (f ◁ (η ▷ h)) ≫ (α_ f g' h).inv = (f ◁ η) ▷ h :=
-by rw [associator_inv_naturality_middle, hom_inv_id_assoc]
+lemma whisker_assoc_symm (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
+  f ◁ (η ▷ h) = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom :=
+by simp
 
 @[reassoc]
-lemma associator_inv_conjugation_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
-  (α_ f g h).inv ≫ ((f ◁ η) ▷ h) ≫ (α_ f g' h).hom = f ◁ (η ▷ h) :=
-by rw [associator_naturality_middle, inv_hom_id_assoc]
+lemma associator_naturality_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
+  (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ (g ◁ η) :=
+by simp
 
 @[reassoc]
 lemma associator_inv_naturality_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
-  (f ◁ (g ◁ η)) ≫ (α_ f g h').inv = (α_ f g h).inv ≫ ((f ≫ g) ◁ η) :=
-by rw [comp_inv_eq, assoc, associator_naturality_right, inv_hom_id_assoc]
+  f ◁ (g ◁ η) ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η :=
+by simp
 
 @[reassoc]
-lemma associator_conjugation_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
-  (α_ f g h).hom ≫ (f ◁ (g ◁ η)) ≫ (α_ f g h').inv = (f ≫ g) ◁ η :=
-by rw [associator_inv_naturality_right, hom_inv_id_assoc]
+lemma comp_whisker_left_symm (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
+  f ◁ (g ◁ η) = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom :=
+by simp
 
 @[reassoc]
-lemma associator_inv_conjugation_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
-  (α_ f g h).inv ≫ ((f ≫ g) ◁ η) ≫ (α_ f g h').hom = f ◁ (g ◁ η) :=
-by rw [associator_naturality_right, inv_hom_id_assoc]
+lemma left_unitor_naturality {f g : a ⟶ b} (η : f ⟶ g) :
+  𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η :=
+by simp
 
 @[reassoc]
-lemma pentagon_inv (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)).inv ≫ (α_ (f ≫ g) h i).inv :=
-eq_of_inv_eq_inv (by simp only [pentagon, inv_whisker_left, inv_whisker_right,
-  is_iso.iso.inv_inv, is_iso.inv_comp, assoc])
+lemma left_unitor_inv_naturality {f g : a ⟶ b} (η : f ⟶ g) :
+  η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η :=
+by simp
 
-@[reassoc]
-lemma pentagon_inv_inv_hom_hom_inv (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 :=
-begin
-  rw ←((eq_comp_inv _).mp (pentagon_inv f g h i)),
-  slice_rhs 1 2 { rw [←whisker_left_comp, hom_inv_id] },
-  simp only [assoc, id_comp, whisker_left_id]
-end
+lemma id_whisker_left_symm {f g : a ⟶ b} (η : f ⟶ g) :
+  η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom :=
+by simp
 
 @[reassoc]
-lemma pentagon_inv_hom_hom_hom_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
-  (α_ (f ≫ g) h i).inv ≫ ((α_ f g h).hom ▷ i) ≫ (α_ f (g ≫ h) i).hom =
-    (α_ f g (h ≫ i)).hom ≫ (f ◁ (α_ g h i).inv) :=
-eq_of_inv_eq_inv (by simp only [pentagon_inv_inv_hom_hom_inv, inv_whisker_left,
-  is_iso.iso.inv_hom, inv_whisker_right, is_iso.iso.inv_inv, is_iso.inv_comp, assoc])
+lemma right_unitor_naturality {f g : a ⟶ b} (η : f ⟶ g) :
+  η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η :=
+by simp
 
 @[reassoc]
-lemma pentagon_hom_inv_inv_inv_inv (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) :=
-begin
-  rw ←((eq_comp_inv _).mp (pentagon_inv f g h i)),
-  slice_lhs 1 2 { rw [←whisker_left_comp, hom_inv_id] },
-  simp only [assoc, id_comp, whisker_left_id, comp_id, hom_inv_id]
-end
+lemma right_unitor_inv_naturality {f g : a ⟶ b} (η : f ⟶ g) :
+  η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b :=
+by simp
 
-@[reassoc]
-lemma pentagon_hom_hom_inv_hom_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
-  (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ (f ◁ (α_ g h i).inv) =
-    ((α_ f g h).hom ▷ i) ≫ (α_ f (g ≫ h) i).hom :=
-eq_of_inv_eq_inv (by simp only [pentagon_hom_inv_inv_inv_inv, inv_whisker_left,
-  is_iso.iso.inv_hom, inv_whisker_right, is_iso.iso.inv_inv, is_iso.inv_comp, assoc])
+lemma whisker_right_id_symm {f g : a ⟶ b} (η : f ⟶ g) :
+  η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom :=
+by simp
 
-@[reassoc]
-lemma pentagon_hom_inv_inv_inv_hom (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) :=
-begin
-  have pent := pentagon f g h i,
-  rw ←inv_comp_eq at pent,
-  rw ←pent,
-  simp only [hom_inv_whisker_left_assoc, assoc, comp_id, hom_inv_id]
-end
+lemma whisker_left_iff {f g : a ⟶ b} (η θ : f ⟶ g) :
+  (𝟙 a ◁ η = 𝟙 a ◁ θ) ↔ (η = θ) :=
+by simp
 
-@[reassoc]
-lemma pentagon_hom_hom_inv_inv_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
-  (α_ f (g ≫ h) i).hom ≫ (f ◁ (α_ g h i).hom) ≫ (α_ f g (h ≫ i)).inv =
-    ((α_ f g h).inv ▷ i) ≫ (α_ (f ≫ g) h i).hom :=
-eq_of_inv_eq_inv (by simp only [pentagon_hom_inv_inv_inv_hom, inv_whisker_left,
-  is_iso.iso.inv_hom, inv_whisker_right, is_iso.iso.inv_inv, is_iso.inv_comp, assoc])
+lemma whisker_right_iff {f g : a ⟶ b} (η θ : f ⟶ g) :
+  (η ▷ 𝟙 b = θ ▷ 𝟙 b) ↔ (η = θ) :=
+by simp
 
-@[reassoc]
-lemma pentagon_inv_hom_hom_hom_hom (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) :=
-by { rw ←pentagon f g h i, simp only [inv_hom_whisker_right_assoc] }
+/--
+We state it as a simp lemma, which is regarded as an involved version of
+`id_whisker_right f g : 𝟙 f ▷ g = 𝟙 (f ≫ g)`.
+-/
+@[reassoc, simp]
+lemma left_unitor_whisker_right (f : a ⟶ b) (g : b ⟶ c) :
+  (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom :=
+by rw [←whisker_left_iff, whisker_left_comp, ←cancel_epi (α_ _ _ _).hom,
+  ←cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle,
+  ←associator_naturality_middle, ←comp_whisker_right_assoc, triangle,
+  associator_naturality_left]; apply_instance
 
-@[reassoc]
-lemma pentagon_inv_inv_hom_inv_inv (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).hom ▷ i) =
-    (f ◁ (α_ g h i).inv) ≫ (α_ f (g ≫ h) i).inv :=
-eq_of_inv_eq_inv (by simp only [pentagon_inv_hom_hom_hom_hom, inv_whisker_left,
-  is_iso.iso.inv_hom, inv_whisker_right, is_iso.iso.inv_inv, is_iso.inv_comp, assoc])
+@[reassoc, simp]
+lemma left_unitor_inv_whisker_right (f : a ⟶ b) (g : b ⟶ c) :
+  (λ_ f).inv ▷ g = (λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv :=
+eq_of_inv_eq_inv (by simp)
 
-lemma triangle_assoc_comp_left (f : a ⟶ b) (g : b ⟶ c) :
-  (α_ f (𝟙 b) g).hom ≫ (f ◁ (λ_ g).hom) = (ρ_ f).hom ▷ g :=
-triangle f g
+@[reassoc, simp]
+lemma whisker_left_right_unitor (f : a ⟶ b) (g : b ⟶ c) :
+  f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom :=
+by rw [←whisker_right_iff, comp_whisker_right, ←cancel_epi (α_ _ _ _).inv,
+  ←cancel_epi (f ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right,
+  ←associator_inv_naturality_middle, ←whisker_left_comp_assoc, triangle_assoc_comp_right,
+  associator_inv_naturality_right]; apply_instance
 
-@[simp, reassoc]
-lemma triangle_assoc_comp_right (f : a ⟶ b) (g : b ⟶ c) :
-  (α_ f (𝟙 b) g).inv ≫ ((ρ_ f).hom ▷ g) = f ◁ (λ_ g).hom :=
-by rw [←triangle, inv_hom_id_assoc]
+@[reassoc, simp]
+lemma whisker_left_right_unitor_inv (f : a ⟶ b) (g : b ⟶ c) :
+  f ◁ (ρ_ g).inv = (ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom :=
+eq_of_inv_eq_inv (by simp)
 
-@[simp, reassoc]
-lemma triangle_assoc_comp_right_inv (f : a ⟶ b) (g : b ⟶ c) :
-  ((ρ_ f).inv ▷ g) ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv :=
-begin
-  apply (cancel_mono (f ◁ (λ_ g).hom)).1,
-  simp only [inv_hom_whisker_left, inv_hom_whisker_right, assoc, triangle]
-end
+/-
+It is not so obvious whether `left_unitor_whisker_right` or `left_unitor_comp` should be a simp
+lemma. Our choice is the former. One reason is that the latter yields the following loop:
+[id_whisker_left]   : 𝟙 a ◁ (ρ_ f).hom ==> (λ_ (f ≫ 𝟙 b)).hom ≫ (ρ_ f).hom ≫ (λ_ f).inv
+[left_unitor_comp]  : (λ_ (f ≫ 𝟙 b)).hom ==> (α_ (𝟙 a) f (𝟙 b)).inv ≫ (λ_ f).hom ▷ 𝟙 b
+[whisker_right_id]  : (λ_ f).hom ▷ 𝟙 b ==> (ρ_ (𝟙 a ≫ f)).hom ≫ (λ_ f).hom ≫ (ρ_ f).inv
+[right_unitor_comp] : (ρ_ (𝟙 a ≫ f)).hom ==> (α_ (𝟙 a) f (𝟙 b)).hom ≫ 𝟙 a ◁ (ρ_ f).hom
+-/
+@[reassoc]
+lemma left_unitor_comp (f : a ⟶ b) (g : b ⟶ c) :
+  (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g :=
+by simp
 
-@[simp, reassoc]
-lemma triangle_assoc_comp_left_inv (f : a ⟶ b) (g : b ⟶ c) :
-  (f ◁ (λ_ g).inv) ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g :=
-begin
-  apply (cancel_mono ((ρ_ f).hom ▷ g)).1,
-  simp only [triangle_assoc_comp_right, inv_hom_whisker_left, inv_hom_whisker_right, assoc]
-end
+@[reassoc]
+lemma left_unitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
+  (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom :=
+by simp
+
+@[reassoc]
+lemma right_unitor_comp (f : a ⟶ b) (g : b ⟶ c) :
+  (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom :=
+by simp
+
+@[reassoc]
+lemma right_unitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
+  (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv :=
+by simp
 
+@[simp]
 lemma unitors_equal : (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom :=
-by rw [←whisker_left_iff, ←cancel_epi (α_ (𝟙 a) (𝟙 _) (𝟙 _)).hom,
-       ←cancel_mono (ρ_ (𝟙 a)).hom, triangle, ←right_unitor_comp, right_unitor_naturality]
+by rw [←whisker_left_iff, ←cancel_epi (α_ _ _ _).hom, ←cancel_mono (ρ_ _).hom, triangle,
+  ←right_unitor_comp, right_unitor_naturality]; apply_instance
 
+@[simp]
 lemma unitors_inv_equal : (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv :=
-by { ext, rw [←unitors_equal], simp only [hom_inv_id] }
-
-end
+by simp [iso.inv_eq_inv]
 
 end bicategory
 
diff --git a/src/category_theory/bicategory/coherence.lean b/src/category_theory/bicategory/coherence.lean
index fe7843dc07d0d..c0b364e1e9122 100644
--- a/src/category_theory/bicategory/coherence.lean
+++ b/src/category_theory/bicategory/coherence.lean
@@ -71,6 +71,11 @@ def preinclusion (B : Type u) [quiver.{v+1} B] :
   map   := λ a b, (inclusion_path a b).obj,
   map₂  := λ a b, (inclusion_path a b).map }
 
+@[simp]
+lemma preinclusion_obj (a : B) :
+  (preinclusion B).obj a = a :=
+rfl
+
 /--
 The normalization of the composition of `p : path a b` and `f : hom b c`.
 `p` will eventually be taken to be `nil` and we then get the normalization
@@ -135,7 +140,7 @@ end
 
 /-- The 2-isomorphism `normalize_iso p f` is natural in `f`. -/
 lemma normalize_naturality {a b c : B} (p : path a b) {f g : hom b c} (η : f ⟶ g) :
-  ((preinclusion B).map p ◁ η) ≫ (normalize_iso p g).hom =
+  (preinclusion B).map p ◁ η ≫ (normalize_iso p g).hom =
     (normalize_iso p f).hom ≫ eq_to_hom (congr_arg _ (normalize_aux_congr p η)) :=
 begin
   rcases η, induction η,
@@ -146,37 +151,14 @@ begin
     slice_lhs 1 2 { rw ihf },
     simp },
   case whisker_left : _ _ _ _ _ _ _ ih
-  { dsimp,
-    slice_lhs 1 2 { rw associator_inv_naturality_right },
-    slice_lhs 2 3 { rw whisker_exchange },
-    slice_lhs 3 4 { erw ih }, /- p ≠ nil required! See the docstring of `normalize_aux`. -/
-    simp only [assoc] },
+  /- p ≠ nil required! See the docstring of `normalize_aux`. -/
+  { dsimp, simp_rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih, assoc] },
   case whisker_right : _ _ _ _ _ h η ih
   { dsimp,
-    slice_lhs 1 2 { rw associator_inv_naturality_middle },
-    slice_lhs 2 3 { erw [←bicategory.whisker_right_comp, ih, bicategory.whisker_right_comp] },
+    rw [associator_inv_naturality_middle_assoc, ←comp_whisker_right_assoc, ih, comp_whisker_right],
     have := dcongr_arg (λ x, (normalize_iso x h).hom) (normalize_aux_congr p (quot.mk _ η)),
     dsimp at this, simp [this] },
-  case associator
-  { dsimp,
-    slice_lhs 3 4 { erw associator_inv_naturality_left },
-    slice_lhs 1 3 { erw pentagon_hom_inv_inv_inv_inv },
-    simpa only [assoc, bicategory.whisker_right_comp, comp_id] },
-  case associator_inv
-  { dsimp,
-    slice_rhs 2 3 { erw associator_inv_naturality_left },
-    slice_rhs 1 2 { erw ←pentagon_inv },
-    simpa only [bicategory.whisker_right_comp, assoc, comp_id] },
-  case left_unitor { erw [comp_id, ←triangle_assoc_comp_right_assoc], refl },
-  case left_unitor_inv
-  { dsimp,
-    slice_lhs 1 2 { erw triangle_assoc_comp_left_inv },
-    rw [inv_hom_whisker_right, id_comp, comp_id] },
-  case right_unitor
-  { erw [comp_id, whisker_left_right_unitor, assoc, ←right_unitor_naturality], refl },
-  case right_unitor_inv
-  { erw [comp_id, whisker_left_right_unitor_inv, assoc, iso.hom_inv_id_assoc,
-      right_unitor_conjugation] }
+  all_goals { dsimp, dsimp [id_def, comp_def], simp }
 end
 
 @[simp]
diff --git a/src/category_theory/bicategory/free.lean b/src/category_theory/bicategory/free.lean
index 2bb968b99d833..6b78babfdbf1c 100644
--- a/src/category_theory/bicategory/free.lean
+++ b/src/category_theory/bicategory/free.lean
@@ -93,24 +93,28 @@ inductive rel : Π {a b : B} {f g : hom a b}, hom₂ f g → hom₂ f g → Prop
 | whisker_left_id {a b c} (f : hom a b) (g : hom b c) :
     rel (f ◁ 𝟙 g) (𝟙 (f.comp g))
 | whisker_left_comp {a b c} (f : hom a b) {g h i : hom b c} (η : hom₂ g h) (θ : hom₂ h i) :
-    rel (f ◁ (η ≫ θ)) ((f ◁ η) ≫ (f ◁ θ))
+    rel (f ◁ (η ≫ θ)) (f ◁ η ≫ f ◁ θ)
+| id_whisker_left {a b} {f g : hom a b} (η : hom₂ f g) :
+    rel (hom.id a ◁ η) (λ_ f ≫ η ≫ λ⁻¹_ g)
+| comp_whisker_left
+    {a b c d} (f : hom a b) (g : hom b c) {h h' : hom c d} (η : hom₂ h h') :
+    rel ((f.comp g) ◁ η) (α_ f g h ≫ f ◁ g ◁ η ≫ α⁻¹_ f g h')
 | whisker_right {a b c} (f g : hom a b) (h : hom b c) (η η' : hom₂ f g) :
     rel η η' → rel (η ▷ h) (η' ▷ h)
-| whisker_right_id {a b c} (f : hom a b) (g : hom b c) :
+| id_whisker_right {a b c} (f : hom a b) (g : hom b c) :
     rel (𝟙 f ▷ g) (𝟙 (f.comp g))
-| whisker_right_comp {a b c} {f g h : hom a b} (i : hom b c) (η : hom₂ f g) (θ : hom₂ g h) :
-    rel ((η ≫ θ) ▷ i) ((η ▷ i) ≫ (θ ▷ i))
-| whisker_exchange {a b c} {f g : hom a b} {h i : hom b c} (η : hom₂ f g) (θ : hom₂ h i) :
-    rel ((f ◁ θ) ≫ (η ▷ i)) ((η ▷ h) ≫ (g ◁ θ))
-| associator_naturality_left
+| comp_whisker_right {a b c} {f g h : hom a b} (i : hom b c) (η : hom₂ f g) (θ : hom₂ g h) :
+    rel ((η ≫ θ) ▷ i) (η ▷ i ≫ θ ▷ i)
+| whisker_right_id {a b} {f g : hom a b} (η : hom₂ f g) :
+    rel (η ▷ hom.id b) (ρ_ f ≫ η ≫ ρ⁻¹_ g)
+| whisker_right_comp
     {a b c d} {f f' : hom a b} (g : hom b c) (h : hom c d) (η : hom₂ f f') :
-    rel (((η ▷ g) ▷ h) ≫ α_ f' g h) (α_ f g h ≫ (η ▷ (g.comp h)))
-| associator_naturality_middle
+    rel (η ▷ (g.comp h)) (α⁻¹_ f g h ≫ η ▷ g ▷ h ≫ α_ f' g h)
+| whisker_assoc
     {a b c d} (f : hom a b) {g g' : hom b c} (η : hom₂ g g') (h : hom c d) :
-    rel (((f ◁ η) ▷ h) ≫ α_ f g' h) (α_ f g h ≫ (f ◁ (η ▷ h)))
-| associator_naturality_right
-    {a b c d} (f : hom a b) (g : hom b c) {h h' : hom c d} (η : hom₂ h h') :
-    rel (((f.comp g) ◁ η) ≫ α_ f g h') (α_ f g h ≫ (f ◁ (g ◁ η)))
+    rel ((f ◁ η) ▷ h) (α_ f g h ≫ f ◁ (η ▷ h)≫ α⁻¹_ f g' h)
+| whisker_exchange {a b c} {f g : hom a b} {h i : hom b c} (η : hom₂ f g) (θ : hom₂ h i) :
+    rel (f ◁ θ ≫ η ▷ i) (η ▷ h ≫ g ◁ θ)
 | associator_hom_inv {a b c d} (f : hom a b) (g : hom b c) (h : hom c d) :
     rel (α_ f g h ≫ α⁻¹_ f g h) (𝟙 ((f.comp g).comp h))
 | associator_inv_hom {a b c d} (f : hom a b) (g : hom b c) (h : hom c d) :
@@ -119,19 +123,15 @@ inductive rel : Π {a b : B} {f g : hom a b}, hom₂ f g → hom₂ f g → Prop
     rel (λ_ f ≫ λ⁻¹_ f) (𝟙 ((hom.id a).comp f))
 | left_unitor_inv_hom {a b} (f : hom a b) :
     rel (λ⁻¹_ f ≫ λ_ f) (𝟙 f)
-| left_unitor_naturality {a b} {f f' : hom a b} (η : hom₂ f f') :
-    rel ((hom.id a ◁ η) ≫ λ_ f') (λ_ f ≫ η)
 | right_unitor_hom_inv {a b} (f : hom a b) :
     rel (ρ_ f ≫ ρ⁻¹_ f) (𝟙 (f.comp (hom.id b)))
 | right_unitor_inv_hom {a b} (f : hom a b) :
     rel (ρ⁻¹_ f ≫ ρ_ f) (𝟙 f)
-| right_unitor_naturality {a b} {f f' : hom a b} (η : hom₂ f f') :
-    rel ((η ▷ hom.id b) ≫ ρ_ f') (ρ_ f ≫ η)
 | pentagon {a b c d e} (f : hom a b) (g : hom b c) (h : hom c d) (i : hom d e) :
-    rel ((α_ f g h ▷ i) ≫ α_ f (g.comp h) i ≫ (f ◁ α_ g h i))
+    rel (α_ f g h ▷ i ≫ α_ f (g.comp h) i ≫ f ◁ α_ g h i)
         (α_ (f.comp g) h i ≫ α_ f g (h.comp i))
 | triangle {a b c} (f : hom a b) (g : hom b c) :
-    rel (α_ f (hom.id b) g ≫ (f ◁ λ_ g)) (ρ_ f ▷ g)
+    rel (α_ f (hom.id b) g ≫ f ◁ λ_ g) (ρ_ f ▷ g)
 
 end
 
@@ -156,11 +156,21 @@ instance bicategory : bicategory (free_bicategory B) :=
   whisker_left_id' := λ a b c f g, quot.sound (rel.whisker_left_id f g),
   whisker_left_comp' := by
   { rintros a b c f g h i ⟨η⟩ ⟨θ⟩, exact quot.sound (rel.whisker_left_comp f η θ) },
+  id_whisker_left' := by
+  { rintros a b f g ⟨η⟩, exact quot.sound (rel.id_whisker_left η) },
+  comp_whisker_left' := by
+  { rintros a b c d f g h h' ⟨η⟩, exact quot.sound (rel.comp_whisker_left f g η) },
   whisker_right := λ a b c f g η h,
     quot.map (hom₂.whisker_right h) (rel.whisker_right f g h) η,
-  whisker_right_id' := λ a b c f g, quot.sound (rel.whisker_right_id f g),
+  id_whisker_right' := λ a b c f g, quot.sound (rel.id_whisker_right f g),
+  comp_whisker_right' := by
+  { rintros a b c f g h ⟨η⟩ ⟨θ⟩ i, exact quot.sound (rel.comp_whisker_right i η θ) },
+  whisker_right_id' := by
+  { rintros a b f g ⟨η⟩, exact quot.sound (rel.whisker_right_id η) },
   whisker_right_comp' := by
-  { rintros a b c f g h ⟨η⟩ ⟨θ⟩ i, exact quot.sound (rel.whisker_right_comp i η θ) },
+  { rintros a b c d f f' ⟨η⟩ g h, exact quot.sound (rel.whisker_right_comp g h η) },
+  whisker_assoc' := by
+  { rintros a b c d f g g' ⟨η⟩ h, exact quot.sound (rel.whisker_assoc f η h) },
   whisker_exchange' := by
   { rintros a b c f g h i ⟨η⟩ ⟨θ⟩, exact quot.sound (rel.whisker_exchange η θ) },
   associator := λ a b c d f g h,
@@ -168,26 +178,16 @@ instance bicategory : bicategory (free_bicategory B) :=
     inv := quot.mk rel (hom₂.associator_inv f g h),
     hom_inv_id' := quot.sound (rel.associator_hom_inv f g h),
     inv_hom_id' := quot.sound (rel.associator_inv_hom f g h) },
-  associator_naturality_left' := by
-  { rintros a b c d f f' ⟨η⟩ g h, exact quot.sound (rel.associator_naturality_left g h η) },
-  associator_naturality_middle' := by
-  { rintros a b c d f g g' ⟨η⟩ h, exact quot.sound (rel.associator_naturality_middle f η h) },
-  associator_naturality_right' := by
-  { rintros a b c d f g h h' ⟨η⟩, exact quot.sound (rel.associator_naturality_right f g η) },
   left_unitor := λ a b f,
   { hom := quot.mk rel (hom₂.left_unitor f),
     inv := quot.mk rel (hom₂.left_unitor_inv f),
     hom_inv_id' := quot.sound (rel.left_unitor_hom_inv f),
     inv_hom_id' := quot.sound (rel.left_unitor_inv_hom f) },
-  left_unitor_naturality' := by
-  { rintros a b f f' ⟨η⟩, exact quot.sound (rel.left_unitor_naturality η) },
   right_unitor := λ a b f,
   { hom := quot.mk rel (hom₂.right_unitor f),
     inv := quot.mk rel (hom₂.right_unitor_inv f),
     hom_inv_id' := quot.sound (rel.right_unitor_hom_inv f),
     inv_hom_id' := quot.sound (rel.right_unitor_inv_hom f) },
-  right_unitor_naturality' := by
-  { rintros a b f f' ⟨η⟩, exact quot.sound (rel.right_unitor_naturality η) },
   pentagon' := λ a b c d e f g h i, quot.sound (rel.pentagon f g h i),
   triangle' := λ a b c f g, quot.sound (rel.triangle f g) }
 
@@ -255,9 +255,7 @@ def lift_hom₂ : ∀ {a b : B} {f g : hom a b}, hom₂ f g → (lift_hom F f 
 | _ _ _ _ (hom₂.whisker_left f η)       := lift_hom F f ◁ lift_hom₂ η
 | _ _ _ _ (hom₂.whisker_right h η)      := lift_hom₂ η ▷ lift_hom F h
 
-local attribute [simp]
-  associator_naturality_left associator_naturality_middle associator_naturality_right
-  left_unitor_naturality right_unitor_naturality pentagon
+local attribute [simp] whisker_exchange
 
 lemma lift_hom₂_congr {a b : B} {f g : hom a b} {η θ : hom₂ f g} (H : rel η θ) :
   lift_hom₂ F η = lift_hom₂ F θ :=
diff --git a/src/category_theory/bicategory/functor.lean b/src/category_theory/bicategory/functor.lean
index bff991973c2a2..e2697618d3fec 100644
--- a/src/category_theory/bicategory/functor.lean
+++ b/src/category_theory/bicategory/functor.lean
@@ -126,8 +126,8 @@ def oplax_functor.map₂_associator_aux
   (map₂ : Π {a b : B} {f g : a ⟶ b}, (f ⟶ g) → (map f ⟶ map g))
   (map_comp : Π {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) ⟶ map f ≫ map g)
   {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Prop :=
-map₂ (α_ f g h).hom ≫ map_comp f (g ≫ h) ≫ (map f ◁ map_comp g h) =
-  map_comp (f ≫ g) h ≫ (map_comp f g ▷ map h) ≫ (α_ (map f) (map g) (map h)).hom
+map₂ (α_ f g h).hom ≫ map_comp f (g ≫ h) ≫ map f ◁ map_comp g h =
+  map_comp (f ≫ g) h ≫ map_comp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
 
 /--
 An oplax functor `F` between bicategories `B` and `C` consists of a function between objects
@@ -146,9 +146,9 @@ structure oplax_functor (B : Type u₁) [bicategory.{w₁ v₁} B] (C : Type u
 (map_id (a : B) : map (𝟙 a) ⟶ 𝟙 (obj a))
 (map_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : map (f ≫ g) ⟶ map f ≫ map g)
 (map_comp_naturality_left' : ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
-  map₂ (η ▷ g) ≫ map_comp f' g = map_comp f g ≫ (map₂ η ▷ map g) . obviously)
+  map₂ (η ▷ g) ≫ map_comp f' g = map_comp f g ≫ map₂ η ▷ map g . obviously)
 (map_comp_naturality_right' : ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
-  map₂ (f ◁ η) ≫ map_comp f g' = map_comp f g ≫ (map f ◁ map₂ η) . obviously)
+  map₂ (f ◁ η) ≫ map_comp f g' = map_comp f g ≫ map f ◁ map₂ η . obviously)
 (map₂_id' : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f) . obviously)
 (map₂_comp' : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
   map₂ (η ≫ θ) = map₂ η ≫ map₂ θ . obviously)
@@ -156,9 +156,9 @@ structure oplax_functor (B : Type u₁) [bicategory.{w₁ v₁} B] (C : Type u
   oplax_functor.map₂_associator_aux obj (λ a b, map) (λ a b f g, map₂) (λ a b c, map_comp) f g h
     . obviously)
 (map₂_left_unitor' : ∀ {a b : B} (f : a ⟶ b),
-  map₂ (λ_ f).hom = map_comp (𝟙 a) f ≫ (map_id a ▷ map f) ≫ (λ_ (map f)).hom . obviously)
+  map₂ (λ_ f).hom = map_comp (𝟙 a) f ≫ map_id a ▷ map f ≫ (λ_ (map f)).hom . obviously)
 (map₂_right_unitor' : ∀ {a b : B} (f : a ⟶ b),
-  map₂ (ρ_ f).hom = map_comp f (𝟙 b) ≫ (map f ◁ map_id b) ≫ (ρ_ (map f)).hom . obviously)
+  map₂ (ρ_ f).hom = map_comp f (𝟙 b) ≫ map f ◁ map_id b ≫ (ρ_ (map f)).hom . obviously)
 
 namespace oplax_functor
 
@@ -225,11 +225,11 @@ def comp (F : oplax_functor B C) (G : oplax_functor C D) : oplax_functor B D :=
     simp only [map₂_associator, ←map₂_comp_assoc, ←map_comp_naturality_right_assoc,
       whisker_left_comp, assoc],
     simp only [map₂_associator, map₂_comp, map_comp_naturality_left_assoc,
-      whisker_right_comp, assoc] },
+      comp_whisker_right, assoc] },
   map₂_left_unitor' := λ a b f, by
   { dsimp,
     simp only [map₂_left_unitor, map₂_comp, map_comp_naturality_left_assoc,
-      whisker_right_comp, assoc] },
+      comp_whisker_right, assoc] },
   map₂_right_unitor' := λ a b f, by
   { dsimp,
     simp only [map₂_right_unitor, map₂_comp, map_comp_naturality_right_assoc,
@@ -270,8 +270,8 @@ def pseudofunctor.map₂_associator_aux
   (map₂ : Π {a b : B} {f g : a ⟶ b}, (f ⟶ g) → (map f ⟶ map g))
   (map_comp : Π {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) ≅ map f ≫ map g)
   {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Prop :=
-map₂ (α_ f g h).hom = (map_comp (f ≫ g) h).hom ≫ ((map_comp f g).hom ▷ map h) ≫
-  (α_ (map f) (map g) (map h)).hom ≫ (map f ◁ (map_comp g h).inv) ≫ (map_comp f (g ≫ h)).inv
+map₂ (α_ f g h).hom = (map_comp (f ≫ g) h).hom ≫ (map_comp f g).hom ▷ map h ≫
+  (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (map_comp g h).inv ≫ (map_comp f (g ≫ h)).inv
 
 /--
 A pseudofunctor `F` between bicategories `B` and `C` consists of a function between objects
@@ -293,17 +293,17 @@ structure pseudofunctor (B : Type u₁) [bicategory.{w₁ v₁} B] (C : Type u
 (map₂_comp' : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
   map₂ (η ≫ θ) = map₂ η ≫ map₂ θ . obviously)
 (map₂_whisker_left' : ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
-  map₂ (f ◁ η) = (map_comp f g).hom ≫ (map f ◁ map₂ η) ≫ (map_comp f h).inv . obviously)
+  map₂ (f ◁ η) = (map_comp f g).hom ≫ map f ◁ map₂ η ≫ (map_comp f h).inv . obviously)
 (map₂_whisker_right' : ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
-  map₂ (η ▷ h) = (map_comp f h).hom ≫ (map₂ η ▷ map h) ≫ (map_comp g h).inv . obviously)
+  map₂ (η ▷ h) = (map_comp f h).hom ≫ map₂ η ▷ map h ≫ (map_comp g h).inv . obviously)
 (map₂_associator' : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
   pseudofunctor.map₂_associator_aux obj (λ a b, map) (λ a b f g, map₂) (λ a b c, map_comp) f g h
     . obviously)
 (map₂_left_unitor' : ∀ {a b : B} (f : a ⟶ b),
-  map₂ (λ_ f).hom = (map_comp (𝟙 a) f).hom ≫ ((map_id a).hom ▷ map f) ≫ (λ_ (map f)).hom
+  map₂ (λ_ f).hom = (map_comp (𝟙 a) f).hom ≫ (map_id a).hom ▷ map f ≫ (λ_ (map f)).hom
     . obviously)
 (map₂_right_unitor' : ∀ {a b : B} (f : a ⟶ b),
-  map₂ (ρ_ f).hom = (map_comp f (𝟙 b)).hom ≫ (map f ◁ (map_id b).hom) ≫ (ρ_ (map f)).hom
+  map₂ (ρ_ f).hom = (map_comp f (𝟙 b)).hom ≫ map f ◁ (map_id b).hom ≫ (ρ_ (map f)).hom
     . obviously)
 
 namespace pseudofunctor
diff --git a/src/category_theory/bicategory/functor_bicategory.lean b/src/category_theory/bicategory/functor_bicategory.lean
index 861ffa2ec11ee..0d1cd9f0e4618 100644
--- a/src/category_theory/bicategory/functor_bicategory.lean
+++ b/src/category_theory/bicategory/functor_bicategory.lean
@@ -31,61 +31,29 @@ namespace oplax_nat_trans
 def whisker_left (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) : η ≫ θ ⟶ η ≫ ι :=
 { app := λ a, η.app a ◁ Γ.app a,
   naturality' := λ a b f, by
-  { dsimp,
-    simp only [assoc],
-    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc,
-        associator_naturality_right_assoc, Γ.whisker_left_naturality_assoc,
-        associator_inv_naturality_middle] } }
+  { dsimp, rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc], simp } }
 
 /-- Right whiskering of an oplax natural transformation and a modification. -/
 @[simps]
 def whisker_right {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) : η ≫ ι ⟶ θ ≫ ι :=
 { app := λ a, Γ.app a ▷ ι.app a,
   naturality' := λ a b f, by
-  { dsimp,
-    simp only [assoc],
-    rw [associator_inv_naturality_middle_assoc, Γ.whisker_right_naturality_assoc,
-        associator_naturality_left_assoc, ←whisker_exchange_assoc,
-        associator_inv_naturality_left] } }
+  { dsimp, simp_rw [assoc, ←associator_inv_naturality_left, whisker_exchange_assoc], simp } }
 
 /-- Associator for the vertical composition of oplax natural transformations. -/
 @[simps]
 def associator (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) : (η ≫ θ) ≫ ι ≅ η ≫ (θ ≫ ι) :=
-modification_iso.of_components (λ a, α_ (η.app a) (θ.app a) (ι.app a))
-begin
-  intros a b f,
-  dsimp,
-  simp only [whisker_right_comp, whisker_left_comp, assoc],
-  rw [←pentagon_inv_inv_hom_hom_inv_assoc, ←associator_naturality_left_assoc,
-      pentagon_hom_hom_inv_hom_hom_assoc, ←associator_naturality_middle_assoc,
-      ←pentagon_inv_hom_hom_hom_hom_assoc, ←associator_naturality_right_assoc,
-      pentagon_hom_inv_inv_inv_hom]
-end
+modification_iso.of_components (λ a, α_ (η.app a) (θ.app a) (ι.app a)) (by tidy)
 
 /-- Left unitor for the vertical composition of oplax natural transformations. -/
 @[simps]
 def left_unitor (η : F ⟶ G) : 𝟙 F ≫ η ≅ η :=
-modification_iso.of_components (λ a, λ_ (η.app a))
-begin
-  intros a b f,
-  dsimp,
-  simp only [triangle_assoc_comp_right_assoc, whisker_right_comp, assoc, whisker_exchange_assoc],
-  rw [←left_unitor_comp, left_unitor_naturality, left_unitor_comp],
-  simp only [iso.hom_inv_id_assoc, inv_hom_whisker_right_assoc, assoc, whisker_exchange_assoc]
-end
+modification_iso.of_components (λ a, λ_ (η.app a)) (by tidy)
 
 /-- Right unitor for the vertical composition of oplax natural transformations. -/
 @[simps]
 def right_unitor (η : F ⟶ G) : η ≫ 𝟙 G ≅ η :=
-modification_iso.of_components (λ a, ρ_ (η.app a))
-begin
-  intros a b f,
-  dsimp,
-  simp only [triangle_assoc_comp_left_inv, inv_hom_whisker_right_assoc, whisker_exchange,
-    assoc, whisker_left_comp],
-  rw [←right_unitor_comp, right_unitor_naturality, right_unitor_comp],
-  simp only [iso.inv_hom_id_assoc, assoc]
-end
+modification_iso.of_components (λ a, ρ_ (η.app a)) (by tidy)
 
 end oplax_nat_trans
 
@@ -96,15 +64,9 @@ variables (B C)
 instance oplax_functor.bicategory : bicategory (oplax_functor B C) :=
 { whisker_left  := λ F G H η _ _ Γ, oplax_nat_trans.whisker_left η Γ,
   whisker_right := λ F G H _ _ Γ η, oplax_nat_trans.whisker_right Γ η,
-  associator := λ F G H I, oplax_nat_trans.associator,
+  associator    := λ F G H I, oplax_nat_trans.associator,
   left_unitor   := λ F G, oplax_nat_trans.left_unitor,
   right_unitor  := λ F G, oplax_nat_trans.right_unitor,
-  associator_naturality_left'   := by { intros, ext, apply associator_naturality_left },
-  associator_naturality_middle' := by { intros, ext, apply associator_naturality_middle },
-  associator_naturality_right'  := by { intros, ext, apply associator_naturality_right },
-  left_unitor_naturality'   := by { intros, ext, apply left_unitor_naturality },
-  right_unitor_naturality'  := by { intros, ext, apply right_unitor_naturality },
-  pentagon' := by { intros, ext, apply pentagon },
-  triangle' := by { intros, ext, apply triangle } }
+  whisker_exchange' := by { intros, ext, apply whisker_exchange } }
 
 end category_theory
diff --git a/src/category_theory/bicategory/natural_transformation.lean b/src/category_theory/bicategory/natural_transformation.lean
index 178f28e78f468..08f8db6d452fe 100644
--- a/src/category_theory/bicategory/natural_transformation.lean
+++ b/src/category_theory/bicategory/natural_transformation.lean
@@ -42,15 +42,15 @@ structure oplax_nat_trans (F G : oplax_functor B C) :=
 (app (a : B) : F.obj a ⟶ G.obj a)
 (naturality {a b : B} (f : a ⟶ b) : F.map f ≫ app b ⟶ app a ≫ G.map f)
 (naturality_naturality' : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
-  (F.map₂ η ▷ app b) ≫ naturality g = naturality f ≫ (app a ◁ G.map₂ η) . obviously)
+  F.map₂ η ▷ app b ≫ naturality g = naturality f ≫ app a ◁ G.map₂ η . obviously)
 (naturality_id' : ∀ a : B,
-  naturality (𝟙 a) ≫ (app a ◁ G.map_id a) =
-    (F.map_id a ▷ app a) ≫ (λ_ (app a)).hom ≫ (ρ_ (app a)).inv . obviously)
+  naturality (𝟙 a) ≫ app a ◁ G.map_id a =
+    F.map_id a ▷ app a ≫ (λ_ (app a)).hom ≫ (ρ_ (app a)).inv . obviously)
 (naturality_comp' : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
-  naturality (f ≫ g) ≫ (app a ◁ G.map_comp f g) =
-    (F.map_comp f g ▷ app c) ≫ (α_ _ _ _).hom ≫
-      (F.map f ◁ naturality g) ≫ (α_ _ _ _).inv ≫
-        (naturality f ▷ G.map g) ≫ (α_ _ _ _).hom . obviously)
+  naturality (f ≫ g) ≫ app a ◁ G.map_comp f g =
+    F.map_comp f g ▷ app c ≫ (α_ _ _ _).hom ≫
+      F.map f ◁ naturality g ≫ (α_ _ _ _).inv ≫
+        naturality f ▷ G.map g ≫ (α_ _ _ _).hom . obviously)
 
 restate_axiom oplax_nat_trans.naturality_naturality'
 restate_axiom oplax_nat_trans.naturality_id'
@@ -67,16 +67,7 @@ variables (F : oplax_functor B C)
 @[simps]
 def id : oplax_nat_trans F F :=
 { app := λ a, 𝟙 (F.obj a),
-  naturality := λ a b f, (ρ_ (F.map f)).hom ≫ (λ_ (F.map f)).inv,
-  naturality_naturality' := λ a b f f' η, by
-  { rw [assoc, ←left_unitor_inv_naturality, ←right_unitor_naturality_assoc] },
-  naturality_comp' := λ a b c f g, by
-  { rw [assoc, ←left_unitor_inv_naturality, ←right_unitor_naturality_assoc],
-    simp only [triangle_assoc_comp_right_assoc, right_unitor_comp, left_unitor_comp_inv,
-      whisker_right_comp, inv_hom_whisker_left_assoc, assoc, whisker_left_comp] },
-  naturality_id' := λ a, by
-  { rw [assoc, ←left_unitor_inv_naturality, ←right_unitor_naturality_assoc,
-      unitors_equal, unitors_inv_equal] } }
+  naturality := λ a b f, (ρ_ (F.map f)).hom ≫ (λ_ (F.map f)).inv }
 
 instance : inhabited (oplax_nat_trans F F) := ⟨id F⟩
 
@@ -87,43 +78,44 @@ variables {a b c : B} {a' : C}
 
 @[simp, reassoc]
 lemma whisker_left_naturality_naturality (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) :
-  (f ◁ (G.map₂ β ▷ θ.app b)) ≫ (f ◁ θ.naturality h) =
-    (f ◁ θ.naturality g) ≫ (f ◁ (θ.app a ◁ H.map₂ β)) :=
-by simp only [←whisker_left_comp, naturality_naturality]
+  f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ θ.naturality h =
+    f ◁ θ.naturality g ≫ f ◁ θ.app a ◁ H.map₂ β :=
+by simp_rw [←bicategory.whisker_left_comp, naturality_naturality]
 
 @[simp, reassoc]
 lemma whisker_right_naturality_naturality {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') :
-  ((F.map₂ β ▷ η.app b) ▷ h) ≫ (η.naturality g ▷ h) =
-    (η.naturality f ▷ h) ≫ ((η.app a ◁ G.map₂ β) ▷ h) :=
-by simp only [←whisker_right_comp, naturality_naturality]
+  F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
+    η.naturality f ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ _ _ _).inv :=
+by rw [←comp_whisker_right, naturality_naturality, comp_whisker_right, whisker_assoc]
 
 @[simp, reassoc]
 lemma whisker_left_naturality_comp (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) :
-  (f ◁ θ.naturality (g ≫ h)) ≫ (f ◁ (θ.app a ◁ H.map_comp g h)) =
-    (f ◁ (G.map_comp g h ▷ θ.app c)) ≫ (f ◁ (α_ _ _ _).hom) ≫
-      (f ◁ (G.map g ◁ θ.naturality h)) ≫ (f ◁ (α_ _ _ _).inv) ≫
-        (f ◁ (θ.naturality g ▷ H.map h)) ≫ (f ◁ (α_ _ _ _).hom) :=
-by simp only [←whisker_left_comp, naturality_comp]
+  f ◁ θ.naturality (g ≫ h) ≫ f ◁ θ.app a ◁ H.map_comp g h =
+    f ◁ G.map_comp g h ▷ θ.app c ≫ f ◁ (α_ _ _ _).hom ≫
+      f ◁ G.map g ◁ θ.naturality h ≫ f ◁ (α_ _ _ _).inv ≫
+        f ◁ θ.naturality g ▷ H.map h ≫ f ◁ (α_ _ _ _).hom :=
+by simp_rw [←bicategory.whisker_left_comp, naturality_comp]
 
 @[simp, reassoc]
 lemma whisker_right_naturality_comp (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') :
-  (η.naturality (f ≫ g) ▷ h) ≫ ((η.app a ◁ G.map_comp f g) ▷ h) =
-    ((F.map_comp f g ▷ η.app c) ▷ h) ≫ ((α_ _ _ _).hom ▷ h) ≫
-      ((F.map f ◁ η.naturality g) ▷ h) ≫ ((α_ _ _ _).inv ▷ h) ≫
-        ((η.naturality f ▷ G.map g) ▷ h) ≫ ((α_ _ _ _).hom ▷ h) :=
-by simp only [←whisker_right_comp, naturality_comp]
+  η.naturality (f ≫ g) ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.map_comp f g ▷ h =
+    F.map_comp f g ▷ η.app c ▷ h ≫ (α_ _ _ _).hom ▷ h ≫ (α_ _ _ _).hom ≫
+      F.map f ◁ η.naturality g ▷ h ≫ (α_ _ _ _).inv ≫ (α_ _ _ _).inv ▷ h ≫
+        η.naturality f ▷ G.map g ▷ h ≫ (α_ _ _ _).hom ▷ h ≫ (α_ _ _ _).hom :=
+by { rw [←associator_naturality_middle, ←comp_whisker_right_assoc, naturality_comp], simp }
 
 @[simp, reassoc]
 lemma whisker_left_naturality_id (f : a' ⟶ G.obj a) :
-  (f ◁ θ.naturality (𝟙 a)) ≫ (f ◁ (θ.app a ◁ H.map_id a)) =
-    (f ◁ (G.map_id a ▷ θ.app a)) ≫ (f ◁ (λ_ (θ.app a)).hom) ≫ (f ◁ (ρ_ (θ.app a)).inv) :=
-by simp only [←whisker_left_comp, naturality_id]
+  f ◁ θ.naturality (𝟙 a) ≫ f ◁ θ.app a ◁ H.map_id a =
+    f ◁ G.map_id a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv :=
+by simp_rw [←bicategory.whisker_left_comp, naturality_id]
 
 @[simp, reassoc]
 lemma whisker_right_naturality_id (f : G.obj a ⟶ a') :
-  (η.naturality (𝟙 a) ▷ f) ≫ ((η.app a ◁ G.map_id a) ▷ f) =
-    ((F.map_id a ▷ η.app a) ▷ f) ≫ ((λ_ (η.app a)).hom ▷ f) ≫ ((ρ_ (η.app a)).inv ▷ f) :=
-by simp only [←whisker_right_comp, naturality_id]
+  η.naturality (𝟙 a) ▷ f ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.map_id a ▷ f =
+    F.map_id a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫
+      (ρ_ (η.app a)).inv ▷ f ≫ (α_ _ _ _).hom :=
+by { rw [←associator_naturality_middle, ←comp_whisker_right_assoc, naturality_id], simp }
 
 end
 
@@ -132,41 +124,30 @@ end
 def vcomp (η : oplax_nat_trans F G) (θ : oplax_nat_trans G H) : oplax_nat_trans F H :=
 { app := λ a, η.app a ≫ θ.app a,
   naturality := λ a b f,
-    (α_ _ _ _).inv ≫ (η.naturality f ▷ θ.app b) ≫ (α_ _ _ _).hom ≫
-      (η.app a ◁ θ.naturality f) ≫ (α_ _ _ _).inv,
-  naturality_naturality' := λ a b f g ι, by
-  { simp only [whisker_right_comp, assoc, whisker_left_comp],
-    rw [←associator_inv_naturality_right, ←whisker_left_naturality_naturality_assoc,
-        ←associator_naturality_middle_assoc, ←whisker_right_naturality_naturality_assoc,
-        ←associator_inv_naturality_left_assoc] },
+    (α_ _ _ _).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ _ _ _).hom ≫
+      η.app a ◁ θ.naturality f ≫ (α_ _ _ _).inv,
   naturality_comp' := λ a b c f g, by
-  { simp only [whisker_right_comp, assoc, whisker_left_comp],
-    rw [←associator_inv_naturality_right, whisker_left_naturality_comp_assoc,
-        ←associator_naturality_middle_assoc, whisker_right_naturality_comp_assoc,
-        ←associator_inv_naturality_left_assoc],
-    rw [←pentagon_hom_hom_inv_inv_hom, associator_naturality_middle_assoc,
-        ←pentagon_inv_hom_hom_hom_inv_assoc, ←associator_naturality_middle_assoc],
-    slice_rhs 5 13
-    { rw [←pentagon_inv_hom_hom_hom_hom_assoc, ←pentagon_hom_hom_inv_hom_hom,
-          associator_naturality_left_assoc, ←associator_naturality_right_assoc,
-          pentagon_inv_inv_hom_hom_inv_assoc, inv_hom_whisker_left_assoc, iso.hom_inv_id_assoc,
-          whisker_exchange_assoc, associator_naturality_right_assoc,
-          ←associator_naturality_left_assoc, ←pentagon_assoc] },
-    simp only [assoc] },
-  naturality_id' := λ a, by
-  { simp only [whisker_right_comp, assoc, whisker_left_comp],
-    rw [←associator_inv_naturality_right, whisker_left_naturality_id_assoc,
-        ←associator_naturality_middle_assoc, whisker_right_naturality_id_assoc,
-        ←associator_inv_naturality_left_assoc],
-    simp only [left_unitor_comp, triangle_assoc, inv_hom_whisker_right_assoc, assoc,
-      right_unitor_comp_inv] } }
+  { calc _ =  _ ≫
+    F.map_comp f g ▷ η.app c ▷ θ.app c ≫ _ ≫
+      F.map f ◁ η.naturality g ▷ θ.app c ≫ _ ≫
+        (F.map f ≫ η.app b) ◁ θ.naturality g ≫
+          η.naturality f ▷ (θ.app b ≫ H.map g) ≫ _ ≫
+            η.app a ◁ θ.naturality f ▷ H.map g ≫ _  : _
+    ... =  _ : _,
+    exact (α_ _ _ _).inv,
+    exact (α_ _ _ _).hom ▷ _ ≫ (α_ _ _ _).hom,
+    exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv,
+    exact (α_ _ _ _).hom ≫ _ ◁ (α_ _ _ _).inv,
+    exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv,
+    { rw [whisker_exchange_assoc], simp },
+    { simp } } }
 
 variables (B C)
 
 @[simps]
 instance : category_struct (oplax_functor B C) :=
-{ hom := λ F G, oplax_nat_trans F G,
-  id := oplax_nat_trans.id,
+{ hom  := oplax_nat_trans,
+  id   := oplax_nat_trans.id,
   comp := λ F G H, oplax_nat_trans.vcomp }
 
 end
@@ -206,17 +187,17 @@ variables {η}
 section
 variables (Γ : modification η θ) {a b c : B} {a' : C}
 
-@[reassoc]
+@[simp, reassoc]
 lemma whisker_left_naturality (f : a' ⟶ F.obj b) (g : b ⟶ c) :
-  (f ◁ (F.map g ◁ Γ.app c)) ≫ (f ◁ θ.naturality g) =
-    (f ◁ η.naturality g) ≫ (f ◁ (Γ.app b ▷ G.map g)) :=
-by simp only [←bicategory.whisker_left_comp, naturality]
+  f ◁ F.map g ◁ Γ.app c ≫ f ◁ θ.naturality g =
+    f ◁ η.naturality g ≫ f ◁ Γ.app b ▷ G.map g :=
+by simp_rw [←bicategory.whisker_left_comp, naturality]
 
-@[reassoc]
+@[simp, reassoc]
 lemma whisker_right_naturality (f : a ⟶ b) (g : G.obj b ⟶ a') :
-  ((F.map f ◁ Γ.app b) ▷ g) ≫ (θ.naturality f ▷ g) =
-    (η.naturality f ▷ g) ≫ ((Γ.app a ▷ G.map f) ▷ g) :=
-by simp only [←bicategory.whisker_right_comp, naturality]
+  F.map f ◁ Γ.app b ▷ g ≫ (α_ _ _ _).inv ≫ θ.naturality f ▷ g =
+    (α_ _ _ _).inv ≫ η.naturality f ▷ g ≫ Γ.app a ▷ G.map f ▷ g :=
+by simp_rw [associator_inv_naturality_middle_assoc, ←comp_whisker_right, naturality]
 
 end
 
@@ -242,13 +223,13 @@ by giving object level isomorphisms, and checking naturality only in the forward
 def modification_iso.of_components
   (app : ∀ a, η.app a ≅ θ.app a)
   (naturality : ∀ {a b} (f : a ⟶ b),
-    (F.map f ◁ (app b).hom) ≫ θ.naturality f = η.naturality f ≫ ((app a).hom ▷ G.map f)) :
+    F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f) :
   η ≅ θ :=
 { hom := { app := λ a, (app a).hom },
   inv :=
   { app := λ a, (app a).inv,
     naturality' := λ a b f, by simpa using
-      congr_arg (λ f, (_ ◁ (app b).inv) ≫ f ≫ ((app a).inv ▷ _)) (naturality f).symm } }
+      congr_arg (λ f, _ ◁ (app b).inv ≫ f ≫ (app a).inv ▷ _) (naturality f).symm } }
 
 end
 
diff --git a/src/category_theory/bicategory/strict.lean b/src/category_theory/bicategory/strict.lean
index 57001ac2288f5..7cd3b4d8c3f89 100644
--- a/src/category_theory/bicategory/strict.lean
+++ b/src/category_theory/bicategory/strict.lean
@@ -75,7 +75,7 @@ by { cases η, simp only [whisker_left_id, eq_to_hom_refl] }
 @[simp]
 lemma eq_to_hom_whisker_right {a b c : B} {f g : a ⟶ b} (η : f = g) (h : b ⟶ c) :
   eq_to_hom η ▷ h = eq_to_hom (congr_arg2 (≫) η rfl) :=
-by { cases η, simp only [whisker_right_id, eq_to_hom_refl] }
+by { cases η, simp only [id_whisker_right, eq_to_hom_refl] }
 
 end bicategory