awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 Z : C
| 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) ▷
      obj L' Z ≫
    LaxMonoidal.μ L' Y X ▷ obj L' Z ≫ LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y X) Z
have a : LaxMonoidal.μ L' X Y ▷ obj L' Z ≫
  LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫ Functor.map L' (Iso.hom (β_ X Y) ▷ Z)
Tactic: simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal,
      Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, comp_whiskerRight, assoc,
      Functor.Monoidal.whiskerRight_δ_μ_assoc, Functor.LaxMonoidal.μ_natural_left]
-- 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 Z : C
| NatTrans.app (NatTrans.app (Iso.hom (braidingNatIso L W ε)) (obj L' X))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y) (obj L' Z)) ≫
    LaxMonoidal.μ L' Y Z ▷ obj L' X
have a : obj L' X ◁ LaxMonoidal.μ L' Y Z ≫
  CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))
    (LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))
    (Functor.map L' (Iso.hom (β_ X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))) ≫
      OplaxMonoidal.δ L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) X)
Tactic: rw [braidingNatIso_hom_app_naturality_μ_left, braidingNatIso_hom_app]
-- 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 Z : C
| obj L' X ◁
      CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) (LaxMonoidal.μ L' Y Z)
        (Functor.map L' (Iso.hom (β_ Y Z)) ≫ OplaxMonoidal.δ L' Z Y) ≫
    obj L' X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y)
have a : CategoryStruct.comp (Y :=
  tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X)
    (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))
  (obj L' X ◁ LaxMonoidal.μ L' Y Z)
  (obj L' X ◁ Functor.map L' (Iso.hom (β_ Y Z)) ≫
    obj L' X ◁ OplaxMonoidal.δ L' Z Y ≫
      obj L' X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
Tactic: simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal,
      Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.whiskerLeft_comp, assoc,
      Functor.Monoidal.whiskerLeft_δ_μ, comp_id]
-- 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 Z : C
| NatTrans.app
      (NatTrans.app (Iso.hom (braidingNatIso L W ε))
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y)))
      (obj L' Z) ≫
    obj L' Z ◁ LaxMonoidal.μ L' X Y
have a : LaxMonoidal.μ L' X Y ▷ obj L' Z ≫
  CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z))
    (LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z)
    (Functor.map L' (Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z)) ≫
      OplaxMonoidal.δ L' Z (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))
Tactic: rw [braidingNatIso_hom_app_naturality_μ_right, braidingNatIso_hom_app]
-- 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
⊢ BraidedCategory.{v_2, u_2} (LocalizedMonoidal L W ε)
have refine_1 : Eq (α :=
  Quiver.Hom (V :=
    LocalizedMonoidal L W ε ⥤
      LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
    (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
    (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)))
  (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
    ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
  (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
    ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))
Tactic: refine .ofBifunctor (braidingNatIso L W ε) ?_ ?_
-- 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
refine_1 :
  Eq (α :=
    Quiver.Hom (V :=
      LocalizedMonoidal L W ε ⥤
        LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
      (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
      (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)))
    (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
      ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
    (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))
⊢ BraidedCategory.{v_2, u_2} (LocalizedMonoidal L W ε)
have refine_2 : Eq (α :=
  Quiver.Hom (V :=
    LocalizedMonoidal L W ε ⥤
      LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
    (bifunctorComp₂₃ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
    (Hexagon.functor₃₁₂ (LocalizedMonoidal L W ε)))
  (Iso.inv (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
    ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε))
  (ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
    ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε))
Tactic: refine .ofBifunctor (braidingNatIso L W ε) ?_ ?_
-- 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
⊢ Eq (α :=
    Quiver.Hom (V :=
      LocalizedMonoidal L W ε ⥤
        LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
      (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
      (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)))
    (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
      ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
    (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))
have refine_1 : ∀ (X₁ X₂ X₃ : C),
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (obj.{v_2, v_2, u_2, u_2}
        (obj
          (obj (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
      (obj.{v_2, v_2, u_2, u_2} (obj (obj (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)) (obj L' X₁)) (obj L' X₂))
        (obj L' X₃)))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
            ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫
              ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
          (obj L' X₁))
        (obj L' X₂))
      (obj L' X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
            ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫
              ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))
          (obj L' X₁))
        (obj L' X₂))
      (obj L' X₃))
Tactic: apply natTrans₃_ext (L') (L') (L') W W W
-- 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
⊢ Eq (α :=
    Quiver.Hom (V :=
      LocalizedMonoidal L W ε ⥤
        LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
      (bifunctorComp₂₃ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
      (Hexagon.functor₃₁₂ (LocalizedMonoidal L W ε)))
    (Iso.inv (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε))
    (ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε))
have refine_2 : ∀ (X₁ X₂ X₃ : C),
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (obj.{v_2, v_2, u_2, u_2}
        (obj
          (obj (bifunctorComp₂₃ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
      (obj.{v_2, v_2, u_2, u_2} (obj (obj (Hexagon.functor₃₁₂ (LocalizedMonoidal L W ε)) (obj L' X₁)) (obj L' X₂))
        (obj L' X₃)))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          (Iso.inv (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
            ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫
              ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε))
          (obj L' X₁))
        (obj L' X₂))
      (obj L' X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          (ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
            ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫
              ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε))
          (obj L' X₁))
        (obj L' X₂))
      (obj L' X₃))
Tactic: apply natTrans₃_ext (L') (L') (L') W W W
-- 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 : SymmetricCategory.{v_1, u_1} C
⊢ SymmetricCategory.{v_2, u_2} (LocalizedMonoidal L W ε)
have refine : ∀ (X Y : C),
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (obj.{v_2, v_2, u_2, u_2} (obj (curriedTensor (LocalizedMonoidal L W ε)) (obj L' X)) (obj L' Y))
      (obj.{v_2, v_2, u_2, u_2}
        (obj
          (obj (flipFunctor (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
            (Functor.flip (curriedTensor (LocalizedMonoidal L W ε))))
          (obj L' X))
        (obj L' Y)))
    (NatTrans.app
      (NatTrans.app
        (Iso.hom (curriedBraidingNatIso (LocalizedMonoidal L W ε)) ≫
          Functor.map (flipFunctor (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
            (Iso.hom (curriedBraidingNatIso (LocalizedMonoidal L W ε))))
        (obj L' X))
      (obj L' Y))
    (NatTrans.app (NatTrans.app (𝟙 (curriedTensor (LocalizedMonoidal L W ε))) (obj L' X)) (obj L' Y))
Tactic: refine .ofCurried (natTrans₂_ext (L') (L') W W fun X Y ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
⊢ Eq (α := ((curriedTensorPre F).obj Y₁).obj Y₂ ⟶ ((curriedTensorPost F).obj Y₁).obj Y₂)
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂)
    ((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂)) (μ G X₁ X₂)
        ((Lifting.iso L W G F).inv.app (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))))
have h₁ : ((curriedTensorPre F).obj Y₁).map e₂.hom ≫
    NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) (L.obj X₂) =
  NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂ ≫
    ((curriedTensorPost F).obj Y₁).map e₂.hom
Tactic: have h₁ := ((curriedTensorPreIsoPost L W F G).hom.app Y₁).naturality e₂.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  ((curriedTensorPre F).obj Y₁).map e₂.hom ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) (L.obj X₂) =
    NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂ ≫
      ((curriedTensorPost F).obj Y₁).map e₂.hom
⊢ Eq (α := ((curriedTensorPre F).obj Y₁).obj Y₂ ⟶ ((curriedTensorPost F).obj Y₁).obj Y₂)
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂)
    ((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂)) (μ G X₁ X₂)
        ((Lifting.iso L W G F).inv.app (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))))
have h₂ : ∀ (X : D),
  NatTrans.app ((curriedTensorPre F).map e₁.hom ≫ NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
      X =
    NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁ ≫ (curriedTensorPost F).map e₁.hom) X
Tactic: have h₂ := congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality e₁.hom)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ F.CoreMonoidal
have refine_1 : Eq (α := curriedTensorPrePre F ⟶ curriedTensorPostPost' F)
  (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
  (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
Tactic: refine Functor.CoreMonoidal.ofBifunctor
    (εIso G ≪≫ e.symm.app _ ≪≫ F.mapIso (εIso L).symm) (curriedTensorPreIsoPost L W F G) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
refine_1 :
  Eq (α := curriedTensorPrePre F ⟶ curriedTensorPostPost' F)
    (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
    (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
⊢ F.CoreMonoidal
have refine_2 : Eq (α := F ⋙ tensorUnitLeft E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapₗ F)
  (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
    (LaxMonoidal.ofBifunctor.topMapₗ
      (Iso.hom
        (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
          (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
    (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
      LaxMonoidal.ofBifunctor.bottomMapₗ F))
Tactic: refine Functor.CoreMonoidal.ofBifunctor
    (εIso G ≪≫ e.symm.app _ ≪≫ F.mapIso (εIso L).symm) (curriedTensorPreIsoPost L W F G) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
refine_1 :
  Eq (α := curriedTensorPrePre F ⟶ curriedTensorPostPost' F)
    (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
    (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
refine_2 :
  Eq (α := F ⋙ tensorUnitLeft E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapₗ F)
    (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.topMapₗ
        (Iso.hom
          (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
            (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
        LaxMonoidal.ofBifunctor.bottomMapₗ F))
⊢ F.CoreMonoidal
have refine_3 : Eq (α := F ⋙ tensorUnitRight E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapᵣ F)
  (CategoryStruct.comp (Y := (curriedTensorPre F).flip.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
    (LaxMonoidal.ofBifunctor.topMapᵣ
      (Iso.hom
        (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
          (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
    (CategoryStruct.comp (Y :=
      (obj (flipFunctor D D E) (curriedTensorPost F)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (NatTrans.app (map (flipFunctor D D E) (Iso.hom (curriedTensorPreIsoPost L W F G)))
        (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.bottomMapᵣ F)))
Tactic: refine Functor.CoreMonoidal.ofBifunctor
    (εIso G ≪≫ e.symm.app _ ≪≫ F.mapIso (εIso L).symm) (curriedTensorPreIsoPost L W F G) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ Eq (α := curriedTensorPrePre F ⟶ curriedTensorPostPost' F)
    (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
    (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
have refine_1 : ∀ (X₁ X₂ X₃ : C),
  Eq (α :=
    (((curriedTensorPrePre F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃) ⟶
      (((curriedTensorPostPost' F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
        (L.obj X₂))
      (L.obj X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
        (L.obj X₂))
      (L.obj X₃))
Tactic: refine natTrans₃_ext L L L W W W (fun X₁ X₂ X₃ ↦ ?_)