-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma triangle (X Y : LocalizedMonoidal L W ε) :
    (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Proof state:
case h.e'_2.h.h.e'_7.h.e'_7.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y
this :
  ((e₁.symm.hom ⊗ ε.symm.hom) ⊗ e₂.symm.hom) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.symm.inv ⊗ ε.symm.inv ⊗ e₂.symm.inv) =
    (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom
e_1✝ : ((X ⊗ 𝟙_ (LocalizedMonoidal L W ε)) ⊗ Y ⟶ X ⊗ Y) = ((X ⊗ unit) ⊗ Y ⟶ X ⊗ Y)
e_4✝ : L'.obj X' ⊗ L.obj (𝟙_ C) ⊗ L'.obj Y' = L'.obj X' ⊗ L'.obj (𝟙_ C) ⊗ L'.obj Y'
⊢ e₁.hom ⊗ (ε.hom ⊗ e₂.hom) ≫ (λ_ Y).hom =
    L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y

Tactic:
exact triangle_aux₂ _ _ _ e₁ e₂

Result:
no goals

Proof state:
case intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (𝟙 (L'.obj X') ⊗ (μ L W ε (𝟙_ C) Y').hom) =
    (((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫
        (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫
          L'.map (α_ X' (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).inv ≫ (𝟙 (L'.obj X') ⊗ (μ L W ε (𝟙_ C) Y').inv)) ≫
      (𝟙 (L'.obj X') ⊗ (μ L W ε (𝟙_ C) Y').hom)
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
simp only [assoc, id_tensorHom, ← whiskerLeft_comp,
  Iso.inv_hom_id, whiskerLeft_id, comp_id, Iso.inv_hom_id,
  ← cancel_mono (μ L W ε X' (𝟙_ C ⊗ Y')).hom] at h₁

Result:
case intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Proof state:
case intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y
this :
  ((e₁.symm.hom ⊗ ε.symm.hom) ⊗ e₂.symm.hom) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.symm.inv ⊗ ε.symm.inv ⊗ e₂.symm.inv) =
    (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom
⊢ ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.hom ⊗ (ε.hom ⊗ e₂.hom) ≫ (λ_ Y).hom) =
    (ρ_ X).hom ▷ Y

Tactic:
convert h₃

Result:
case h.e'_2.h.h.e'_7.h.e'_7.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y
this :
  ((e₁.symm.hom ⊗ ε.symm.hom) ⊗ e₂.symm.hom) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.symm.inv ⊗ ε.symm.inv ⊗ e₂.symm.inv) =
    (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom
e_1✝ : ((X ⊗ 𝟙_ (LocalizedMonoidal L W ε)) ⊗ Y ⟶ X ⊗ Y) = ((X ⊗ unit) ⊗ Y ⟶ X ⊗ Y)
e_4✝ : L'.obj X' ⊗ L.obj (𝟙_ C) ⊗ L'.obj Y' = L'.obj X' ⊗ L'.obj (𝟙_ C) ⊗ L'.obj Y'
⊢ e₁.hom ⊗ (ε.hom ⊗ e₂.hom) ≫ (λ_ Y).hom =
    L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y

case h.e'_3.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y
this :
  ((e₁.symm.hom ⊗ ε.symm.hom) ⊗ e₂.symm.hom) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.symm.inv ⊗ ε.symm.inv ⊗ e₂.symm.inv) =
    (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom
e_1✝ : ((X ⊗ 𝟙_ (LocalizedMonoidal L W ε)) ⊗ Y ⟶ X ⊗ Y) = ((X ⊗ unit) ⊗ Y ⟶ X ⊗ Y)
⊢ (ρ_ X).hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y