Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X')).symm
            ((unitCompPartialBijective B ⋯)
              (((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X'))
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X')).symm
                      ((unitCompPartialBijective A ⋯)
                        (((ihom.adjunction B).homEquiv A (i.obj X'))
                          ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X)).symm
              ((unitCompPartialBijective B ⋯)
                (((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X))
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X)).symm
                        ((unitCompPartialBijective A ⋯)
                          (((ihom.adjunction B).homEquiv A (i.obj X))
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g

Tactic:
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq,
    homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        uncurry
            ((unitCompPartialBijective B ⋯)
              (curry
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  uncurry
                      ((unitCompPartialBijective A ⋯)
                        (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g