awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : C
apply :
  Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
      (Iso.inv (ρ_ X) ≫ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (λ_ X)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (Iso.hom (λ_ X)))
⊢ Eq.{v₁ + 1} (α := X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (ρ_ X) ≫ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.inv (λ_ X))

Tactic:
apply (cancel_mono (λ_ X).hom).1

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
      (Iso.inv (ρ_ X) ≫ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (λ_ X)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (Iso.hom (λ_ X)))

Tactic:
simp only [assoc, braiding_leftUnitor, Iso.inv_hom_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.braiding_leftUnitor
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X))

Tactic:
simp [← rightUnitor_inv_braiding]

Premises used: CategoryTheory.rightUnitor_inv_braiding
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : C
rw :
  Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
rw [Iso.inv_ext]

Premises used: CategoryTheory.Iso.inv_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : C
rw :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
      (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X)) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rw [braiding_tensorUnit_right]

Premises used: CategoryTheory.braiding_tensorUnit_right
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : C
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
      (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X)) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (Iso.hom (β_ Y X))
    (Iso.inv (β_ X Y))

Tactic:
Iso.inv_ext' (symmetry X Y)

Premises used: CategoryTheory.Iso.inv_ext', CategoryTheory.SymmetricCategory.symmetry
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
dsimp :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
        (G.map (μ F X Y)) ≫
      G.map (F.map (Iso.hom (β_ X Y))))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ (F ⋙ G) X Y ≫ (F ⋙ G).map (Iso.hom (β_ X Y))) (Iso.hom (β_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y)) ≫ μ (F ⋙ G) Y X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
a : G.map (Iso.hom (β_ (F.obj X) (F.obj Y))) ≫ G.map (μ F Y X)
| G.map (μ F X Y) ≫ G.map (F.map (Iso.hom (β_ X Y)))

Tactic:
rw [← CategoryTheory.Functor.map_comp, braided, CategoryTheory.Functor.map_comp]

Premises used: CategoryTheory.Functor.LaxBraided.braided, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
slice_lhs :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
      (G.map (Iso.hom (β_ (F.obj X) (F.obj Y))) ≫ G.map (μ F Y X)))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
        (G.map (μ F X Y)) ≫
      G.map (F.map (Iso.hom (β_ X Y))))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))

Tactic:
slice_lhs 2 3 =>
      rw [← CategoryTheory.Functor.map_comp, braided, CategoryTheory.Functor.map_comp]

Premises used: CategoryTheory.Functor.LaxBraided.braided, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
a : Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫ μ G (F.obj Y) (F.obj X)
| μ G (F.obj X) (F.obj Y) ≫ G.map (Iso.hom (β_ (F.obj X) (F.obj Y)))

Tactic:
rw [braided]

Premises used: CategoryTheory.Functor.LaxBraided.braided
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
slice_lhs :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X)))
      (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫ μ G (F.obj Y) (F.obj X)) (G.map (μ F Y X)))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
      (G.map (Iso.hom (β_ (F.obj X) (F.obj Y))) ≫ G.map (μ F Y X)))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))

Tactic:
slice_lhs 1 2 => rw [braided]

Premises used: CategoryTheory.Functor.LaxBraided.braided
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X)))
      (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫ μ G (F.obj Y) (F.obj X)) (G.map (μ F Y X)))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ G
inst_9 : F.LaxBraided
inst_10 : G.LaxMonoidal
inst_11 : NatTrans.IsMonoidal i.hom
X_1 Y_1 X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ G X Y)
    ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))

Tactic:
simp [NatTrans.IsMonoidal.tensor X Y, tensorHom_comp_tensorHom_assoc]

Premises used: CategoryTheory.NatTrans.IsMonoidal.tensor, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ G
inst_9 : F.LaxBraided
inst_10 : G.LaxMonoidal
inst_11 : NatTrans.IsMonoidal i.hom
X Y : C
⊢ ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ G X Y) ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))

Tactic:
have (X Y : C) : μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app _ := by
      simp [NatTrans.IsMonoidal.tensor X Y, tensorHom_comp_tensorHom_assoc]
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ G
inst_9 : F.LaxBraided
inst_10 : G.LaxMonoidal
inst_11 : NatTrans.IsMonoidal i.hom
X Y : C
this :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ G X Y) ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      G.map (Iso.hom (β_ X Y)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (Iso.hom (β_ X Y)) ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ G X Y ≫ G.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (G.obj X) (G.obj Y)) ≫ μ G Y X)

Tactic:
rw [this X Y, this Y X, ← braiding_naturality_assoc, ← Functor.LaxBraided.braided_assoc]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_assoc, CategoryTheory.Functor.LaxBraided.braided_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ G
inst_9 : F.LaxBraided
inst_10 : G.LaxMonoidal
inst_11 : NatTrans.IsMonoidal i.hom
X Y : C
this :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ G X Y) ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      G.map (Iso.hom (β_ X Y)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (Iso.hom (β_ X Y)) ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : LaxBraidedFunctor.{v₁, v₂, u₁, u₂} C D
⊢ (InducedCategory.Hom.hom (𝟙 F)).hom = 𝟙 F.toLaxMonoidalFunctor.toFunctor

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F G H : LaxBraidedFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : G ⟶ H
⊢ (α ≫ β).hom = α.hom ≫ β.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F G : LaxBraidedFunctor.{v₁, v₂, u₁, u₂} C D
α β : F ⟶ G
h : α.hom.hom = β.hom.hom
⊢ α = β

Tactic:
InducedCategory.hom_ext (LaxMonoidalFunctor.hom_ext h)

Premises used: CategoryTheory.InducedCategory.hom_ext, CategoryTheory.LaxMonoidalFunctor.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F G : LaxBraidedFunctor.{v₁, v₂, u₁, u₂} C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_3) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ Iso.hom (e (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (ε G.toFunctor)
tensor :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ Iso.hom (e (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y)
X : C
⊢ (isoOfComponents e ⋯ unit tensor).hom.hom.hom.app X = (e X).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F G : LaxBraidedFunctor.{v₁, v₂, u₁, u₂} C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_3) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ Iso.hom (e (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (ε G.toFunctor)
tensor :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ Iso.hom (e (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y)
X : C
⊢ (isoOfComponents e ⋯ unit tensor).inv.hom.hom.app X = (e X).inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_6 : F.Braided
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (F.map (Iso.hom (β_ X Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y)) (δ F X Y)
      (μ F X Y ≫ F.map (Iso.hom (β_ X Y))))
rw₁ rw₂ :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (F.map (Iso.hom (β_ X Y))) (F.map (Iso.hom (β_ X Y)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (F.map (Iso.hom (β_ X Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y)) (δ F X Y)
      (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X))

Tactic:
rw [← Functor.Braided.braided, δ_μ_assoc]

Premises used: CategoryTheory.Functor.Braided.braided, CategoryTheory.Functor.Monoidal.δ_μ_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
inst_2 : BraidedCategory.{v₁, u₁} C_1
D_1 : Type u₂
inst_3 : Category.{v₂, u₂} D_1
inst_4 : MonoidalCategory.{v₂, u₂} D_1
inst_5 : BraidedCategory.{v₂, u₂} D_1
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
C : Type u_1
D : Type u_2
inst_9 : Category.{v_1, u_1} C
inst_10 : Category.{v_2, u_2} D
inst_11 : MonoidalCategory.{v_1, u_1} C
inst_12 : MonoidalCategory.{v_2, u_2} D
inst_13 : BraidedCategory.{v_1, u_1} C
inst_14 : SymmetricCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_15 : F.Braided
inst_16 : F.Faithful
X Y : C
⊢ F.map (Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X)) = F.map (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_9) X Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
inst_2 : BraidedCategory.{v₁, u₁} C_1
D_1 : Type u₂
inst_3 : Category.{v₂, u₂} D_1
inst_4 : MonoidalCategory.{v₂, u₂} D_1
inst_5 : BraidedCategory.{v₂, u₂} D_1
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
C : Type u_1
D : Type u_2
inst_9 : Category.{v_1, u_1} C
inst_10 : Category.{v_2, u_2} D
inst_11 : MonoidalCategory.{v_1, u_1} C
inst_12 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_13 : F.Monoidal
inst_14 : F.Full
inst_15 : F.Faithful
inst_16 : SymmetricCategory.{v_2, u_2} D
h : BraidedCategory.{v_1, u_1} C := BraidedCategory.ofFullyFaithful F
X Y : C
⊢ Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_10) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_9) Y X))
    (μ F X Y ≫ F.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)

Tactic:
simp +instances [h, BraidedCategory.ofFullyFaithful, BraidedCategory.ofFaithful]

Premises used: CategoryTheory.BraidedCategory.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
toMonoidal : F.Monoidal
braided :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
      (μ F X Y ≫ F.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
braided_1 :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
      (μ F X Y ≫ F.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
⊢ { toMonoidal := toMonoidal, braided := braided : F.Braided } =
    { toMonoidal := { toMonoidal := toMonoidal, braided := braided }.toMonoidal, braided := braided_1 }

Tactic:
rfl