-- 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
X X' : D
f : (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶ X
g : X ⟶ X'
a :
  Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)) ⟶ i.obj X')
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
      (uncurry
        ((unitCompPartialBijective B ⋯ :
            (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X') →
              i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X')
          (curry
            (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
              uncurry
                ((unitCompPartialBijective A ⋯ : (a : A ⟶ B ⟹ i.obj X') → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X')
                  (curry
                    (Iso.inv (β_ A B) ≫
                      NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
                        i.map f ≫ i.map g))))))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
      (uncurry
          ((unitCompPartialBijective B ⋯ :
              (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) →
                i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X)
            (curry
              (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
                uncurry
                  ((unitCompPartialBijective A ⋯ : (a : A ⟶ B ⟹ i.obj X) → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X)
                    (curry
                      (Iso.inv (β_ A B) ≫
                        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
                          i.map f)))))) ≫
        i.map g))
⊢ Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)) ⟶ i.obj X')
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
      (uncurry
          ((unitCompPartialBijective B ⋯ :
              (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X') →
                i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X')
            (curry
              (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
                uncurry
                    ((unitCompPartialBijective A ⋯ :
                        (a : A ⟶ B ⟹ i.obj X') → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X')
                      (curry
                        (Iso.inv (β_ A B) ≫
                          (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
                              i.map (f ≫ g)) ≫
                            𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X')))
    (i.map
        (i.fullyFaithfulOfReflective.preimage
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
            (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
            (uncurry
                ((unitCompPartialBijective B ⋯ :
                    (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) →
                      i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X)
                  (curry
                    (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯ :
                              (a : A ⟶ B ⟹ i.obj X) → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X)
                            (curry
                              (Iso.inv (β_ A B) ≫
                                (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                                      (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
                                    i.map f) ≫
                                  𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X)))) ≫
      i.map g)

Tactic:
simp only [Category.comp_id, Functor.map_comp, Functor.FullyFaithful.map_preimage, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.FullyFaithful.map_preimage