awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ⊗ₘ g)
have rw : W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ▷ Y₁ ≫ X₂ ◁ g)
Tactic: rw [tensorHom_def]
-- 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
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W.inverseImage F f
hg : W.inverseImage F g
⊢ W.inverseImage F (X := tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁) (f ⊗ₘ g)
have simp : ∀ (hf : W (F.map f)) (hg : W (F.map g)), W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (F.map (f ⊗ₘ g))
Tactic: simp only [inverseImage_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- 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
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
⊢ W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (F.map (f ⊗ₘ g))
have rw : W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (Y := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂))
  (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Functor.OplaxMonoidal.δ F X₁ Y₁)
    ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂))
Tactic: rw [Functor.Monoidal.map_tensor _ f g]
-- 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
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
⊢ W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (Y := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Functor.OplaxMonoidal.δ F X₁ Y₁)
      ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂))
have hf₁ : W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Y := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂))
  ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂)
Tactic: apply MorphismProperty.RespectsIso.precomp
-- 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
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Y :=
    F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂)) ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂)
have hf₁ : W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (F.map f ⊗ₘ F.map g)
Tactic: apply MorphismProperty.RespectsIso.postcomp
-- 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₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
⊢ IsIso (X :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₁, Y₁))
    (Y :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₂, Y₂))
    (Functor.map (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L'))
        (f₁, f₂) :
      Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₁, Y₁) ⟶
        Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₂, Y₂))
have this : IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (X₁, Y₁).1 Y₁))
  (Functor.map L' (f₁ ▷ Y₁))
Tactic: have := Localization.inverts L' W _ (W.whiskerRight_mem f₁ hf₁ 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₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
this :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (X₁, Y₁).1 Y₁))
    (Functor.map L' (f₁ ▷ Y₁))
⊢ IsIso (X :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₁, Y₁))
    (Y :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₂, Y₂))
    (Functor.map (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L'))
        (f₁, f₂) :
      Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₁, Y₁) ⟶
        Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₂, Y₂))
have this₁ : IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ (X₁, Y₁).2))
  (Functor.map L' (X₂ ◁ f₂))
Tactic: have := Localization.inverts L' W _ (W.whiskerLeft_mem X₂ f₂ hf₂)
-- 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₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
this_1 :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (X₁, Y₁).1 Y₁))
    (Functor.map L' (f₁ ▷ Y₁))
this :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ (X₁, Y₁).2))
    (Functor.map L' (X₂ ◁ f₂))
⊢ IsIso (X :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₁, Y₁))
    (Y :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₂, Y₂))
    (Functor.map (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L'))
        (f₁, f₂) :
      Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₁, Y₁) ⟶
        Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₂, Y₂))
have dsimp : IsIso (C := D) (X :=
  (Functor.obj (L' : Functor.{v_1, v_2, u_1, u_2} C (LocalizedMonoidal L W ε))
      (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) :
    D))
  (Functor.map L' (f₁ ▷ Y₁) ≫ Functor.map L' (X₂ ◁ f₂))
Tactic: dsimp
-- 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 : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) (Functor.obj L' Y))
      (Functor.obj L' Y))
    (Iso.hom (λ_ (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)))
have dsimp : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε) (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y))
    (Functor.obj L' Y))
  (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      NatTrans.app
        (liftNatTrans L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') L'
          (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (𝟭 (LocalizedMonoidal L W ε)) (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom))
        (Functor.obj L' Y) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
  (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
Tactic: dsimp +instances [monoidalCategoryStruct, leftUnitor]
-- 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 : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
        NatTrans.app
          (liftNatTrans L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') L'
            (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (𝟭 (LocalizedMonoidal L W ε)) (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom))
          (Functor.obj L' Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
have rw : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε) (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y))
    (Functor.obj L' Y))
  (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      CategoryStruct.comp (Y := Functor.obj (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') Y)
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          Y)
        (NatTrans.app (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom) Y ≫
          NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) Y) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
  (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
Tactic: rw [liftNatTrans_app]
-- 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 : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
        CategoryStruct.comp (Y := Functor.obj (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') Y)
          (NatTrans.app
            (Iso.hom
              (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
                (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
            Y)
          (NatTrans.app (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom) Y ≫
            NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
have dsimp : NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
    CategoryStruct.comp (Y := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
      (NatTrans.app
        (Iso.hom
          (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
            (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
        Y)
      ((Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y)) ≫ 𝟙 (Functor.obj L' Y)) =
  NatTrans.app (Functor.map (tensorBifunctor L W ε) (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: dsimp
-- 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 : C
⊢ NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          Y)
        ((Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y)) ≫ 𝟙 (Functor.obj L' Y)) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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))
have rw : NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
    CategoryStruct.comp (Y := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
      (NatTrans.app
        (Iso.hom
          (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
            (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
        Y)
      (Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y) ≫ 𝟙 (Functor.obj L' Y)) =
  NatTrans.app (Functor.map (tensorBifunctor L W ε) (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: rw [assoc]
-- 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 : C
⊢ NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          Y)
        (Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y) ≫ 𝟙 (Functor.obj L' Y)) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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))
have change : NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
    Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y) ≫
      Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (Functor.obj L' Y) ≫ 𝟙 (Functor.obj L' Y) =
  NatTrans.app (Functor.map (tensorBifunctor L W ε) (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: change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
-- 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 : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X)
        (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
      (Functor.obj L' X))
    (Iso.hom (ρ_ (Functor.obj L' X)))
    (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)))
have dsimp : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε) (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit)
    (Functor.obj L' X))
  (Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      NatTrans.app
        (liftNatTrans L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') L'
          (Functor.obj (Functor.flip (tensorBifunctor L W ε)) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (𝟭 (LocalizedMonoidal L W ε)) (Functor.whiskerRight (Iso.hom (rightUnitorNatIso C)) L' ≫ L.leftUnitor.hom))
        (Functor.obj L' X) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))
  (Functor.map (Functor.obj (tensorBifunctor 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)) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))
Tactic: dsimp +instances [monoidalCategoryStruct, rightUnitor]