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'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ?hB)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ?hB✝)
                    (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f))))) ≫
          (ihom (i.obj ((reflector i).obj A))).map (i.map g)) =
    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).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

pp: case hB
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.essImage (i.obj ((reflector i).obj A) ⟹ i.obj X)

pp: case hB
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.essImage (B ⟹ i.obj X)

Tactic:
uncurry_natural_right,

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'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ?hB)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ?hB✝)
                    (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f)))))) ≫
        i.map g =
    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).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

case hB
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.essImage (i.obj ((reflector i).obj A) ⟹ i.obj X)

case hB
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.essImage (B ⟹ i.obj X)