-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
rw :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
      NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
        (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
⊢ Eq (α :=
    (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
    ((Equiv.symm
            (Adjunction.homEquiv (reflectorAdjunction i) (tensorObj.{v₁, u₁} (𝒞 := inst) A B)
              (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))) :
          (a : A ⊗ B ⟶ i.obj ((reflector i).obj A ⊗ (reflector i).obj B)) →
            (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj A ⊗ (reflector i).obj B)
        (Iso.hom (β_ A B) ≫
          uncurry
            (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ≫
              curry
                (Iso.hom (β_ B (i.obj ((reflector i).obj A))) ≫
                  uncurry
                    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B ≫
                      curry (Iso.inv (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B))))))) :
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶
        tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
    (prodComparison (reflector i) A B :
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶
        tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))

Tactic:
rw [uncurry_natural_left, uncurry_curry, uncurry_natural_left, uncurry_curry,
    ← BraidedCategory.braiding_naturality_left_assoc, SymmetricCategory.symmetry_assoc,
    ← MonoidalCategory.whisker_exchange_assoc, ← tensorHom_def'_assoc,
    Adjunction.homEquiv_symm_apply, ← Adjunction.eq_unit_comp_map_iff, Iso.comp_inv_eq,
    Category.assoc, prodComparisonIso_hom i ((reflector i).obj A) ((reflector i).obj B)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_hom, CategoryTheory.reflector, CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.SymmetricCategory.symmetry_assoc, CategoryTheory.MonoidalClosed.uncurry_natural_left, CategoryTheory.Adjunction.eq_unit_comp_map_iff, CategoryTheory.BraidedCategory.braiding_naturality_left_assoc, CategoryTheory.Functor.obj, CategoryTheory.Adjunction.homEquiv_symm_apply