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
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
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')
⊢ 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'))
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
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')
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'))
⊢ 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₆ : e₁.inv ▷ tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ≫
    Iso.hom (ρ_ (Functor.obj L' X')) =
  (e₁.inv ⊗ₘ ε.inv) ≫ Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ 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]
-- 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
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')
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_f₆ :
  e₁.inv ▷ tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ≫
      Iso.hom (ρ_ (Functor.obj L' X')) =
    (e₁.inv ⊗ₘ ε.inv) ≫ Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X'))
⊢ 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₇ : e₁.inv ▷ tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ≫
    Functor.obj L' X' ◁ Iso.inv (ε' L W ε) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) =
  (e₁.inv ⊗ₘ ε.inv) ≫ Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ 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]
-- 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
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')
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_f₆ :
  e₁.inv ▷ tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ≫
      Iso.hom (ρ_ (Functor.obj L' X')) =
    (e₁.inv ⊗ₘ ε.inv) ≫ Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X'))
e_f₇ :
  e₁.inv ▷ tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ≫
      Functor.obj L' X' ◁ Iso.inv (ε' L W ε) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) =
    (e₁.inv ⊗ₘ ε.inv) ≫ Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X'))
⊢ 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₈ : (e₁.inv ⊗ₘ 𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε))) ≫
    Functor.obj L' X' ◁ Iso.inv (ε' L W ε) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) =
  (e₁.inv ⊗ₘ ε.inv) ≫ Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ 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]
-- 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 ε
⊢ 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 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
have obtain : ∀ (X' : C) (e₁ : Functor.obj L' X' ≅ X),
  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 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
Tactic: obtain ⟨X', ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩
-- 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' : C
e₁ : Functor.obj L' X' ≅ X
⊢ 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 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
have obtain : ∀ (Y' : C) (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 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
Tactic: obtain ⟨Y', ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (hypothesis)
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' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
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 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
have h₁ : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε)
    (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
        (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (Functor.obj L' Y'))
    (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
      (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
  (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
    (𝟙 (Functor.obj L' X') ⊗ₘ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
  (((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
        Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')) ≫
          Iso.inv (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')) ≫
            (𝟙 (Functor.obj L' X') ⊗ₘ Iso.inv (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))) ≫
    (𝟙 (Functor.obj L' X') ⊗ₘ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
Tactic: have h₁ := (associator_hom_app L W ε X' (𝟙_ _) Y' =≫
    (𝟙 ((L').obj X') ⊗ₘ (μ L W ε (𝟙_ C) Y').hom))
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (hypothesis)
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' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
e₂ : Functor.obj L' Y' ≅ Y
h₁ :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
          (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (Functor.obj L'
        (tensorObj.{v_1, u_1} (𝒞 := inst) X'
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
    (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      Functor.obj L' X' ◁ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫
        Iso.hom (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
    ((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
        Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
have h₂ : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε)
    (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
      (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
    (Functor.obj L' Y'))
  (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
  (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫
    Iso.inv (ε' L W ε) ▷ Functor.obj L' Y' ≫
      Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ Y')))
Tactic: have h₂ := (ε' L W ε).hom ▷ (L').obj Y' ≫= leftUnitor_hom_app L W ε Y'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (hypothesis)
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' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
e₂ : Functor.obj L' Y' ≅ Y
h₁ :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
          (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (Functor.obj L'
        (tensorObj.{v_1, u_1} (𝒞 := inst) X'
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
    (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      Functor.obj L' X' ◁ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫
        Iso.hom (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
    ((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
        Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
h₂ :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
      (Functor.obj L' Y'))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫
      Iso.inv (ε' L W ε) ▷ Functor.obj L' Y' ≫
        Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ 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 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
have h₃ : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε)
    (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
      (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
    (Functor.obj L' Y'))
  (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
  (Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ Y')))
Tactic: simp only [← whiskerRight_comp_assoc, Iso.hom_inv_id, whiskerRight_id, id_comp] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Braided (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
inst_5 : BraidedCategory.{v_1, u_1} C
X Y : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
      (obj (obj (Functor.flip (tensorBifunctor L W ε)) (obj L' X)) (obj L' Y)))
    (NatTrans.app (NatTrans.app (Iso.hom (braidingNatIso L W ε)) (obj L' X)) (obj L' Y))
    (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (LaxMonoidal.μ L' X Y)
      (Functor.map L' (Iso.hom (β_ X Y)) ≫ OplaxMonoidal.δ L' Y X))
have simp : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
    (obj (obj (tensorBifunctor L W ε) (obj L' Y)) (obj L' X)))
  (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))
      (NatTrans.app
        (NatTrans.app
          (Iso.hom
            (Lifting₂.iso L' L' W W (curriedTensor C ⋙ obj (whiskeringRight C C (LocalizedMonoidal L W ε)) L')
              (tensorBifunctor L W ε)))
          X)
        Y)
      (Functor.map L' (Iso.hom (β_ X Y)) ≫
        NatTrans.app
          (NatTrans.app
            (Iso.inv
              (Lifting₂.iso L' L' W W
                (Functor.flip (curriedTensor C) ⋙ obj (whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                (Functor.flip (tensorBifunctor L W ε))))
            X)
          Y) :
    Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
      (obj (obj (tensorBifunctor L W ε) (obj L' Y)) (obj L' X)))
  (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (LaxMonoidal.μ L' X Y)
      (Functor.map L' (Iso.hom (β_ X Y)) ≫ OplaxMonoidal.δ L' Y X) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y) (obj L' X)))
Tactic: simp [braidingNatIso, lift₂NatIso]