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
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
X Y Z : Cᴹᵒᵖ
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) X)
          (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) Y))
        (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) Z) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C)
        (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y Z)))
    (Iso.hom (β_ X.unmop Y.unmop) ▷ Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) Z ≫
      Iso.hom (β_ (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y).unmop Z.unmop) ≫
        Functor.map (unmopFunctor C) (Iso.hom (α_ X Y Z)))
    (Iso.hom
        (α_ (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) X) (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) Y)
          (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) Z)) ≫
      Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) X ◁ Iso.hom (β_ Y.unmop Z.unmop) ≫
        Iso.hom (β_ X.unmop (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y Z).unmop))

Tactic:
simp [← yang_baxter_assoc]

Premises used: CategoryTheory.BraidedCategory.yang_baxter_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
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)))
    (ε (unmopFunctor C)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

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
⊢ η (unmopFunctor C) =
    𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)))

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
X Y : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) Y) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y))
    (μ (unmopFunctor C) X Y) (Iso.hom (β_ X.unmop Y.unmop))

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
X Y : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (unmopFunctor C) Y))
    (δ (unmopFunctor C) X Y) (Iso.inv (β_ X.unmop Y.unmop))

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
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
X x x_1 : C
f : x ⟶ x_1
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X x ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) x_1 X)
    (X ◁ f ≫ Iso.hom (Iso.symm (β_ x_1 X))) (Iso.hom (Iso.symm (β_ x X)) ≫ f ▷ 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
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
x x_1 : C
f : x ⟶ x_1
Z : C
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) x Z ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z x_1)
    (f ▷ Z ≫ Iso.hom (Iso.symm (β_ Z x_1))) (Iso.hom (Iso.symm (β_ Z x)) ≫ Z ◁ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
i : SymmetricCategory.{v₁, u₁} C
e_braiding :
  Eq (α := (X Y : C) → tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≅ tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (fun (X Y : C) ↦ Iso.symm (β_ Y X)) β_
⊢ Eq (α := BraidedCategory.{v₁, u₁} C)
    { braiding := fun (X Y : C) ↦ Iso.symm (β_ Y X), braiding_naturality_right := ⋯, braiding_naturality_left := ⋯,
      hexagon_forward := ⋯, hexagon_reverse := ⋯ }
    toBraidedCategory

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
i : SymmetricCategory.{v₁, u₁} C
e_braiding :
  ∀ (X Y : C),
    Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≅ tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (Iso.symm (β_ Y X))
      (β_ X Y)
⊢ Eq (α := (X Y : C) → tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≅ tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (fun (X Y : C) ↦ Iso.symm (β_ Y X)) β_

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

Tactic:
Iso.ext (braiding_swap_eq_inv_braiding Y X).symm

Premises used: CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding, Eq.symm, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
i : SymmetricCategory.{v₁, u₁} C
X Y : C
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≅ tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (Iso.symm (β_ Y X))
    (β_ X Y)

Tactic:
exact Iso.ext (braiding_swap_eq_inv_braiding Y X).symm

Premises used: CategoryTheory.Iso.ext
-- 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 : 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
C : Type u₁
inst_9 : Category.{v₁, u₁} C
inst_10 : MonoidalCategory.{v₁, u₁} C
inst_11 : SymmetricCategory.{v₁, u₁} C
⊢ ∀ (X Y : C),
    Eq (α :=
      tensorObj.{v₁, u₁} (𝒞 := inst_9) (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) ⟶
        Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst_9) Y X))
      (μ (𝟭 C) X Y ≫ Functor.map (𝟭 C) (Iso.hom (β_ X Y)))
      (Iso.hom (β_ (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y)) ≫ μ (𝟭 C) Y X)

Tactic:
simp +instances [reverseBraiding, braiding_swap_eq_inv_braiding]

Premises used: CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding, CategoryTheory.reverseBraiding
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
⊢ Eq (α := C ⥤ C ⥤ Functor.{v_1, v_1, u_1, u_1} C C)
    (Functor.flip (bifunctorComp₁₂ (curriedTensor C) (curriedTensor C)))
    (bifunctorComp₁₂ (Functor.flip (curriedTensor C)) (curriedTensor C))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
⊢ Eq (α := C ⥤ C ⥤ Functor.{v_1, v_1, u_1, u_1} C C)
    (Functor.flip (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)))
    (flip₁₃ (Functor.flip (bifunctorComp₂₃ (curriedTensor C) (Functor.flip (curriedTensor C)))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
⊢ Eq (α := C ⥤ C ⥤ Functor.{v_1, v_1, u_1, u_1} C C) (bifunctorComp₁₂ (curriedTensor C) (curriedTensor C))
    (flip₂₃ (Functor.flip (bifunctorComp₂₃ (Functor.flip (curriedTensor C)) (curriedTensor C))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Opposite
Goal:
C : Type u_2
inst : Category.{v_2, u_2} C
inst_1 : MonoidalCategory.{v_2, u_2} C
inst_2 : BraidedCategory.{v_2, u_2} C
X Y W Z : Cᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop
        (tensorObj.{v_2, u_2} (𝒞 := Category.opposite) (tensorObj.{v_2, u_2} (𝒞 := Category.opposite) X Y)
          (tensorObj.{v_2, u_2} (𝒞 := Category.opposite) W Z)) ⟶
      unop
        (tensorObj.{v_2, u_2} (𝒞 := Category.opposite) (tensorObj.{v_2, u_2} (𝒞 := Category.opposite) X W)
          (tensorObj.{v_2, u_2} (𝒞 := Category.opposite) Y Z)))
    (Quiver.Hom.unop (tensorμ X W Y Z)) (tensorμ (unop X) (unop Y) (unop W) (unop Z))

Tactic:
simp only [unop_tensorObj, tensorμ, unop_comp, unop_inv_associator, unop_whiskerLeft,
    unop_hom_associator, unop_whiskerRight, unop_hom_braiding, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.unop_inv_associator, CategoryTheory.unop_whiskerRight, CategoryTheory.unop_comp, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.unop_hom_braiding, CategoryTheory.unop_hom_associator, CategoryTheory.unop_tensorObj, CategoryTheory.unop_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Opposite
Goal:
C : Type u_2
inst : Category.{v_2, u_2} C
inst_1 : MonoidalCategory.{v_2, u_2} C
inst_2 : BraidedCategory.{v_2, u_2} C
X Y W Z : C
⊢ Eq.{v_2 + 1} (α :=
    op
        (tensorObj.{v_2, u_2} (𝒞 := inst) (tensorObj.{v_2, u_2} (𝒞 := inst) X Y)
          (tensorObj.{v_2, u_2} (𝒞 := inst) W Z)) ⟶
      op
        (tensorObj.{v_2, u_2} (𝒞 := inst) (tensorObj.{v_2, u_2} (𝒞 := inst) X W)
          (tensorObj.{v_2, u_2} (𝒞 := inst) Y Z)))
    (Quiver.Hom.op (tensorμ X W Y Z)) (tensorμ (op X) (op Y) (op W) (op Z))

Tactic:
simp only [op_tensorObj, tensorμ, op_comp, op_inv_associator, op_whiskerLeft, op_hom_associator,
    op_whiskerRight, op_hom_braiding, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.op_inv_associator, CategoryTheory.op_whiskerRight, CategoryTheory.op_tensorObj, CategoryTheory.op_whiskerLeft, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.op_hom_braiding, CategoryTheory.op_hom_associator
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ⟶
      R.obj c)
    (d ◁ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetractionAux adj c d)
    (NatTrans.app (ihom.ev d) (R.obj c))
simp : curry (NatTrans.app (ihom.ev d) (R.obj c)) = 𝟙 (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))
⊢ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetraction adj c d =
    𝟙 (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))

Tactic:
simp only [id_obj, comp_obj, adjRetraction, ← curry_natural_left, this]

Premises used: CategoryTheory.Functor.comp_obj, _private.0.CategoryTheory.Monoidal.Reflective.adjRetraction, CategoryTheory.MonoidalClosed.curry_natural_left, CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ⟶
      R.obj c)
    (d ◁ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetractionAux adj c d)
    (NatTrans.app (ihom.ev d) (R.obj c))
⊢ curry (NatTrans.app (ihom.ev d) (R.obj c)) = 𝟙 (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))

Tactic:
simp [curry_eq]

Premises used: CategoryTheory.MonoidalClosed.curry_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
suffices :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ⟶
      R.obj c)
    (d ◁ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetractionAux adj c d)
    (NatTrans.app (ihom.ev d) (R.obj c))
⊢ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetraction adj c d =
    𝟙 (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))

Tactic:
suffices (_ ◁ adj.unit.app _) ≫ adjRetractionAux adj c d = (ihom.ev _).app _ by
    simp only [id_obj, comp_obj, adjRetraction, ← curry_natural_left, this]
    simp [curry_eq]
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
simp :
  Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ≫
      adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ▷ d ≫
        R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ◁ adj.unit.app d ≫
          adj.unit.app
              (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
                (R.obj (L.obj d))) ≫
            inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))) ≫
              R.map (L.map (Iso.hom (β_ (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d))) ≫
                R.map (L.map (NatTrans.app (ihom.ev d) (R.obj c))) ≫ inv (adj.unit.app (R.1 c)) =
    NatTrans.app (ihom.ev d) (R.obj c)
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ⟶
      R.obj c)
    (d ◁ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetractionAux adj c d)
    (NatTrans.app (ihom.ev d) (R.obj c))

Tactic:
simp only [id_obj, comp_obj, adjRetractionAux, Functor.map_inv, Functor.comp_map,
    braiding_naturality_right_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_inv, _private.0.CategoryTheory.Monoidal.Reflective.adjRetractionAux, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.comp_map, CategoryTheory.BraidedCategory.braiding_naturality_right_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
a : adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d
| adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ▷ d ≫
    R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ◁ adj.unit.app d

Tactic:
simp only [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom, Category.id_comp,
      Category.comp_id]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
slice_lhs :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⟶ R.obj c)
    (Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ≫
      (((((adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d) ≫
                adj.unit.app
                  (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
                    (R.obj (L.obj d)))) ≫
              inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (Iso.hom (β_ (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d)))) ≫
          R.map (L.map (NatTrans.app (ihom.ev d) (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)))
    (NatTrans.app (ihom.ev d) (R.obj c))
⊢ Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ≫
      adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ▷ d ≫
        R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ◁ adj.unit.app d ≫
          adj.unit.app
              (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
                (R.obj (L.obj d))) ≫
            inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))) ≫
              R.map (L.map (Iso.hom (β_ (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d))) ≫
                R.map (L.map (NatTrans.app (ihom.ev d) (R.obj c))) ≫ inv (adj.unit.app (R.1 c)) =
    NatTrans.app (ihom.ev d) (R.obj c)

Tactic:
slice_lhs 2 3 =>
    simp only [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom, Category.id_comp,
      Category.comp_id]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
a :
  adj.unit.app (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d) ≫
    R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)) ≫
      inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)))
| (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d) ≫
    adj.unit.app
        (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
          (R.obj (L.obj d))) ≫
      inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)))

Tactic:
rw [← adj.unit_naturality_assoc]

Premises used: CategoryTheory.Adjunction.unit_naturality_assoc