triangle_aux₃ — Mathlib

Lean4
theorem triangle_aux₃ {X Y : LocalizedMonoidal L W ε} {X' Y' : C} (e₁ : (L').obj X' ≅ X) (e₂ : (L').obj Y' ≅ Y) :
    (ρ_ X).hom ▷ _ =
      ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫ _ ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ (L').map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y :=
  by
  simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, assoc, comp_id, id_comp, Iso.inv_hom_id]
  congr
  rw [← cancel_mono e₁.inv, assoc, assoc, assoc, Iso.hom_inv_id, comp_id, ← rightUnitor_naturality, rightUnitor_hom_app,
    ← tensorHom_id, ← id_tensorHom, ← tensor_comp_assoc, comp_id, id_comp]
Похожие утверждения