-- 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_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
          (prodComparison (reflector i) A B)
          ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
              (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
                (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
            (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
rw₁ :
  Eq (α :=
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
        ((bijection i A B (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)) :
            (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj A ⊗ (reflector i).obj B) →
              (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj A ⊗ (reflector i).obj B)
          (prodComparison (reflector i) A B))
        ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
            (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
              (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
          (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
rw₂ :
  Eq (α :=
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
        ((bijection i A B (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)) :
            (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj A ⊗ (reflector i).obj B) →
              (reflector i).obj A ⊗ (reflector i).obj B ⟶ (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)))
        ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
            (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
              (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
          (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
rw₃ :
  Eq.{v₁ + 1} (α :=
    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)) ≫
      (bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))))
    ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
        (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
          (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
      (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))))
rw₄ rw₅ :
  Eq (α :=
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
      (prodComparison (reflector i) A B)
      ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)))) =
    𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))

Tactic:
rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id,
        Equiv.apply_symm_apply, Category.id_comp]

Premises used: Equiv.apply_symm_apply, CategoryTheory.bijection_natural, Function.Injective.eq_iff, CategoryTheory.bijection_symm_apply_id, CategoryTheory.bijection, Equiv.injective, CategoryTheory.Category.id_comp