Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case e
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
X Y : D
⊢ ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))).pt ≅
    (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).pt

pp: case h₁
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
X Y : D
⊢ BinaryFan.fst
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))) =
    Iso.hom ?e ≫ (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).fst

pp: case h₂
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
X Y : D
⊢ BinaryFan.snd
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))) =
    Iso.hom ?e ≫ (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).snd

Tactic:
· change (reflector i ⋙ i).obj (i.obj X ⊗ i.obj Y) ≅ (𝟭 C).obj (i.obj X ⊗ i.obj Y)
          letI : IsIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) := by
            apply Functor.essImage.unit_isIso
            have := reflective_products i
            use Limits.prod X Y
            constructor
            apply Limits.PreservesLimitPair.iso i _ _ |>.trans
            refine Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
              (tensorProductIsBinaryProduct _ _)
          exact asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) |>.symm

Goal state after:
case h₁
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
X Y : D
⊢ BinaryFan.fst
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))) =
    (_root_.id (asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))).symm).hom ≫
      (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).fst

case h₂
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
X Y : D
⊢ BinaryFan.snd
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))) =
    (_root_.id (asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))).symm).hom ≫
      (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).snd