-- 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
simp :
  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) ≫
          (Equiv.symm
                (Adjunction.homEquiv (ihom.adjunction B) A
                  (i.obj (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)) →
                B ⊗ A ⟶ i.obj ((reflector i).obj A ⊗ (reflector i).obj B))
            (CategoryStruct.comp (Y := i.obj ((reflector i).obj A))
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A)
              ((Adjunction.homEquiv (ihom.adjunction B) (i.obj ((reflector i).obj A))
                    (i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))) :
                  (a : B ⊗ i.obj ((reflector i).obj A) ⟶ i.obj ((reflector i).obj A ⊗ (reflector i).obj B)) →
                    i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj ((reflector i).obj A ⊗ (reflector i).obj B))
                (Iso.hom (β_ B (i.obj ((reflector i).obj A))) ≫
                  (Equiv.symm
                        (Adjunction.homEquiv (ihom.adjunction (i.obj ((reflector i).obj A))) B
                          (i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))) :
                      (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj ((reflector i).obj A ⊗ (reflector i).obj B)) →
                        i.obj ((reflector i).obj A) ⊗ B ⟶ i.obj ((reflector i).obj A ⊗ (reflector i).obj B))
                    (CategoryStruct.comp (Y := i.obj ((reflector i).obj B))
                      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
                      ((Adjunction.homEquiv (ihom.adjunction (i.obj ((reflector i).obj A)))
                            (i.obj ((reflector i).obj B))
                            (i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))) :
                          (a :
                              i.obj ((reflector i).obj A) ⊗ i.obj ((reflector i).obj B) ⟶
                                i.obj ((reflector i).obj A ⊗ (reflector i).obj B)) →
                            i.obj ((reflector i).obj B) ⟶
                              i.obj ((reflector i).obj A) ⟹ i.obj ((reflector i).obj A ⊗ (reflector i).obj B))
                        (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))
⊢ 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 (bijection i A B (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))) :
          (a : (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj A ⊗ (reflector i).obj B) →
            (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj A ⊗ (reflector i).obj B)
        (𝟙 (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((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:
simp only [bijection, Equiv.trans_def, curriedTensor_obj_obj, Equiv.symm_trans_apply,
    Equiv.symm_symm, Functor.FullyFaithful.homEquiv_apply, Functor.map_id, Iso.homCongr_symm,
    Iso.symm_symm_eq, Iso.refl_symm, Iso.homCongr_apply, Iso.refl_hom, Category.comp_id,
    unitCompPartialBijective_symm_apply, Functor.id_obj, Functor.comp_obj, Iso.symm_inv]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.symm_symm_eq, CategoryTheory.Functor.FullyFaithful.homEquiv_apply, Equiv.symm_symm, Equiv.symm_trans_apply, Equiv.trans_def, CategoryTheory.bijection, CategoryTheory.Iso.symm_inv, CategoryTheory.Category.comp_id, CategoryTheory.Iso.homCongr_apply, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.Functor.map_id, CategoryTheory.Iso.refl_symm, CategoryTheory.Functor.id_obj, CategoryTheory.Iso.homCongr_symm, CategoryTheory.Iso.refl_hom, CategoryTheory.unitCompPartialBijective_symm_apply