Lean4
theorem pentagon (Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε) : Pentagon Y₁ Y₂ Y₃ Y₄ :=
by
obtain ⟨X₁, ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Y₁) := ⟨_, ⟨(L').objObjPreimageIso Y₁⟩⟩
obtain ⟨X₂, ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y₂) := ⟨_, ⟨(L').objObjPreimageIso Y₂⟩⟩
obtain ⟨X₃, ⟨e₃⟩⟩ : ∃ X₃, Nonempty ((L').obj X₃ ≅ Y₃) := ⟨_, ⟨(L').objObjPreimageIso Y₃⟩⟩
obtain ⟨X₄, ⟨e₄⟩⟩ : ∃ X₄, Nonempty ((L').obj X₄ ≅ Y₄) := ⟨_, ⟨(L').objObjPreimageIso Y₄⟩⟩
suffices Pentagon ((L').obj X₁) ((L').obj X₂) ((L').obj X₃) ((L').obj X₄)
by
dsimp [Pentagon]
refine
Eq.trans ?_
(((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫ (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)
·
rw [← id_tensorHom, ← id_tensorHom, ← tensorHom_id, ← tensorHom_id, assoc, assoc, ← tensor_comp, ←
associator_naturality, id_comp, ← comp_id e₁.hom, tensor_comp, ← associator_naturality_assoc, ←
comp_id (𝟙 ((L').obj X₄)), ← tensor_comp_assoc, associator_naturality, comp_id, comp_id, ← tensor_comp_assoc,
assoc, e₄.inv_hom_id, ← tensor_comp, e₁.inv_hom_id, ← tensor_comp, e₂.inv_hom_id, e₃.inv_hom_id,
id_tensorHom_id, id_tensorHom_id, comp_id]
·
rw [assoc, associator_naturality_assoc, associator_naturality_assoc, ← tensor_comp, e₁.inv_hom_id, ← tensor_comp,
e₂.inv_hom_id, ← tensor_comp, e₃.inv_hom_id, e₄.inv_hom_id, id_tensorHom_id, id_tensorHom_id, id_tensorHom_id,
comp_id]
dsimp [Pentagon]
have :
((L').obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ (L').obj X₄ ≫
(α_ ((L').obj X₁) ((L').obj X₂ ⊗ (L').obj X₃) ((L').obj X₄)).hom ≫
(L').obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ (L').obj X₄ =
(α_ ((L').obj X₁) ((L').obj (X₂ ⊗ X₃)) ((L').obj X₄)).hom :=
pentagon_aux₂ _ _ _ (μ L W ε X₂ X₃).symm
rw [associator_hom_app, tensorHom_id, id_tensorHom, associator_hom_app, tensorHom_id, whiskerLeft_comp,
whiskerRight_comp, whiskerRight_comp, whiskerRight_comp, assoc, assoc, assoc, whiskerRight_comp, assoc,
reassoc_of% this, associator_hom_app, tensorHom_id, ←
pentagon_aux₁ (X₂ := (L').obj X₃) (X₃ := (L').obj X₄) (i := μ L W ε X₁ X₂), ←
pentagon_aux₃ (X₁ := (L').obj X₁) (X₂ := (L').obj X₂) (i := μ L W ε X₃ X₄), associator_hom_app, associator_hom_app]
simp only [assoc, ← whiskerRight_comp_assoc, Iso.inv_hom_id, comp_id, μ_natural_left_assoc, id_tensorHom,
← whiskerLeft_comp, Iso.inv_hom_id_assoc]
rw [← (L').map_comp_assoc, whiskerLeft_comp, μ_inv_natural_right_assoc, ← (L').map_comp_assoc]
simp only [assoc, MonoidalCategory.pentagon, Functor.map_comp, tensorHom_id, whiskerRight_comp_assoc]
congr 3; simp only [← assoc]; congr
simp only [← cancel_mono (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv, assoc, id_comp, whisker_exchange_assoc,
← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id, ← whiskerLeft_comp, whiskerLeft_id]
