awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
this :
  Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
    (Functor.obj L' X₄)
refine_1 :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
          (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃)
        Y₄ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂
          (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄)))
    (Iso.hom (α_ Y₁ Y₂ Y₃) ▷ Y₄ ≫
      Iso.hom (α_ Y₁ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃) Y₄) ≫
        Y₁ ◁ Iso.hom (α_ Y₂ Y₃ Y₄))
    ((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      (Iso.hom (α_ (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)) ▷ Functor.obj L' X₄ ≫
          Iso.hom
              (α_ (Functor.obj L' X₁)
                (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₂)
                  (Functor.obj L' X₃))
                (Functor.obj L' X₄)) ≫
            Functor.obj L' X₁ ◁ Iso.hom (α_ (Functor.obj L' X₂) (Functor.obj L' X₃) (Functor.obj L' X₄))) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom))
⊢ Iso.hom (α_ Y₁ Y₂ Y₃) ▷ Y₄ ≫
      Iso.hom (α_ Y₁ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃) Y₄) ≫
        Y₁ ◁ Iso.hom (α_ Y₂ Y₃ Y₄) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
have refine_2 : (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
    (Iso.hom
          (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
            (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
        Iso.hom
          (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
            (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
              (Functor.obj L' X₄)))) ≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
    Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
Tactic: refine Eq.trans ?_ (((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
this :
  Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
    (Functor.obj L' X₄)
⊢ (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      (Iso.hom
            (α_
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
              (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
          Iso.hom
            (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
                (Functor.obj L' X₄)))) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
have refine_2 : (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
    Iso.hom
        (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
          (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
      Iso.hom
          (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
            (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃) (Functor.obj L' X₄))) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
    Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
this :
  Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
    (Functor.obj L' X₄)
refine_2 :
  (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      Iso.hom
          (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
            (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
        Iso.hom
            (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
                (Functor.obj L' X₄))) ≫
          (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
⊢ (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      (Iso.hom
            (α_
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
              (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
          Iso.hom
            (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
                (Functor.obj L' X₄)))) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
have refine_2₁ : Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
    ((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv ⊗ₘ e₄.inv) ≫
      Iso.hom
          (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
            (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃) (Functor.obj L' X₄))) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
    Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
have suffices : Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
  (Functor.obj L' X₄)
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj L' Y')) ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ Iso.hom (λ_ Y))
    (Functor.obj L' X' ◁
        (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫
          tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ◁ e₂.hom ≫
            Iso.hom (λ_ Y)) ≫
      e₁.hom ▷ Y)
have simp : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
        (Functor.obj L' Y')) ⟶
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
  (e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ Iso.hom (λ_ Y))
  (e₁.hom ⊗ₘ
    (Iso.hom (ε' L W ε) ≫
          𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) ⊗ₘ
        e₂.hom) ≫
      Iso.hom (λ_ Y))
Tactic: simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, comp_id, id_comp,
    ← tensor_comp_assoc, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj L' Y')) ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ Iso.hom (λ_ Y))
    (e₁.hom ⊗ₘ
      (Iso.hom (ε' L W ε) ≫
            𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) ⊗ₘ
          e₂.hom) ≫
        Iso.hom (λ_ Y))
have e_g : ε.hom =
  Iso.hom (ε' L W ε) ≫ 𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (Iso.hom (ρ_ X) ▷ Y)
    (((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
            (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ◁
          e₂.hom ≫
        (Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X'))) ▷ Y ≫
          e₁.hom ▷ Y)
have simp : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
        (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
      Y ⟶
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
  (Iso.hom (ρ_ X) ⊗ₘ 𝟙 Y)
  ((e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom ⊗ₘ
    𝟙 Y)
Tactic: simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, assoc, comp_id,
    id_comp, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (Iso.hom (ρ_ X) ⊗ₘ 𝟙 Y)
    ((e₁.inv ⊗ₘ ε.inv) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom ⊗ₘ
      𝟙 Y)
have e_f : Iso.hom (ρ_ X) =
  (e₁.inv ⊗ₘ ε.inv) ≫
    Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
⊢ Iso.hom (ρ_ X) =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom
have e_f : Iso.hom (ρ_ X) ≫ e₁.inv =
  ((e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫
    e₁.inv
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
e_f :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    ((e₁.inv ⊗ₘ ε.inv) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫
      e₁.inv
⊢ Iso.hom (ρ_ X) =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom
have e_f₁ : Iso.hom (ρ_ X) ≫ e₁.inv =
  (e₁.inv ⊗ₘ ε.inv) ≫
    (Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫ e₁.inv
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
e_f :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    ((e₁.inv ⊗ₘ ε.inv) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫
      e₁.inv
e_f₁ :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    (e₁.inv ⊗ₘ ε.inv) ≫
      (Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫ e₁.inv
⊢ Iso.hom (ρ_ X) =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom
have e_f₂ : Iso.hom (ρ_ X) ≫ e₁.inv =
  (e₁.inv ⊗ₘ ε.inv) ≫
    Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ (Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫ e₁.inv
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
e_f :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    ((e₁.inv ⊗ₘ ε.inv) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫
      e₁.inv
e_f₁ :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    (e₁.inv ⊗ₘ ε.inv) ≫
      (Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫ e₁.inv
e_f₂ :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ (Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫ e₁.inv
⊢ Iso.hom (ρ_ X) =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom
have e_f₃ : Iso.hom (ρ_ X) ≫ e₁.inv =
  (e₁.inv ⊗ₘ ε.inv) ≫
    Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom ≫ e₁.inv
Tactic: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
e_f :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    ((e₁.inv ⊗ₘ ε.inv) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫
      e₁.inv
e_f₁ :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    (e₁.inv ⊗ₘ ε.inv) ≫
      (Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫ e₁.inv
e_f₂ :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ (Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom) ≫ e₁.inv
e_f₃ :
  Iso.hom (ρ_ X) ≫ e₁.inv =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom ≫ e₁.inv
⊢ Iso.hom (ρ_ X) =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom
have e_f₄ : Iso.hom (ρ_ X) ≫ e₁.inv =
  (e₁.inv ⊗ₘ ε.inv) ≫
    Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      Functor.map L' (Iso.hom (ρ_ X')) ≫ 𝟙 (Functor.obj L' X')
Tactic: 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]