-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma triangle (X Y : LocalizedMonoidal L W ε) :
    (α_ X (𝟙_ _) 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 ε).hom ▷ L'.obj Y' ≫ (ε' L W ε).inv ▷ L'.obj Y' ≫ (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
simp only [← whiskerRight_comp_assoc, Iso.hom_inv_id, whiskerRight_id, id_comp] 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
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ 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₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫ L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom) =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
replace h₃ := ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫= (h₃ =≫ (_ ◁ e₂.hom)) =≫ (e₁.hom ▷ _)

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
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' ≫ (λ_ (L'.obj Y')).hom)) ≫
          L'.obj X' ◁ e₂.hom) ≫
        e₁.hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y' ≫ L'.obj X' ◁ e₂.hom) ≫ e₁.hom ▷ Y
⊢ (α_ 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₃ :
  (((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom) ≫
      L'.map ((α_ X' (𝟙_ C) Y').hom ≫ X' ◁ (λ_ Y').hom) =
    (((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom) ≫ L'.map ((ρ_ X').hom ▷ Y')
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
simp only [assoc, Functor.map_comp, ← reassoc_of% h₁] 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
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
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'.map (X' ◁ (λ_ Y').hom) =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map ((ρ_ X').hom ▷ Y')
⊢ (α_ 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
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
have h₂ := (ε' L W ε).hom ▷ (L').obj Y' ≫= leftUnitor_hom_app L W ε Y'

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
h₂ :
  (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom =
    (ε' L W ε).hom ▷ L'.obj Y' ≫ (ε' L W ε).inv ▷ L'.obj Y' ≫ (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y