[GOAL]
C : Type u_1
inst✝ : Bicategory C
X : C
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : EndMonoidal X} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) (f₁ ≫ g₁) (f₂ ≫ g₂) =
      (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) f₁ f₂ ≫ (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) g₁ g₂
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : EndMonoidal X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) (f₁✝ ≫ g₁✝) (f₂✝ ≫ g₂✝) =
    (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) f₁✝ f₂✝ ≫ (fun {X₁ Y₁ X₂ Y₂} f g => f ▷ X₂ ≫ Y₁ ◁ g) g₁✝ g₂✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : EndMonoidal X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (f₁✝ ≫ g₁✝) ▷ X₂✝ ≫ Z₁✝ ◁ (f₂✝ ≫ g₂✝) = (f₁✝ ▷ X₂✝ ≫ Y₁✝ ◁ f₂✝) ≫ g₁✝ ▷ Y₂✝ ≫ Z₁✝ ◁ g₂✝
[PROOFSTEP]
rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
  Bicategory.whisker_exchange_assoc]
