awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
X Y : D
apply :
  (Cone.postcompose (pairComp X Y i).hom).obj
      (i.mapCone
        (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
          ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
          ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))) ≅
    BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
      (snd (i.obj X) (i.obj Y))
⊢ IsLimit
    (i.mapCone
      (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
        ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
        ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y)))

Tactic:
apply IsLimit.equivOfNatIsoOfIso (pairComp X Y _) _ _ _ |>.invFun
          (tensorProductIsBinaryProduct (i.obj X) (i.obj Y))

Premises used: CategoryTheory.Limits.pairComp, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct, CategoryTheory.Functor.obj, Equiv.invFun, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- 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
X Y : D
e :
  ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
            ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
              NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y)))).pt ≅
    Cone.pt.{0, v₁, 0, u₁} (F := pair (i.obj X) (i.obj Y))
      (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
        (snd (i.obj X) (i.obj Y)))
h₁ :
  BinaryFan.fst
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
            ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
              NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y)))) =
    Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      BinaryFan.fst
        (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
          (snd (i.obj X) (i.obj Y)))
h₂ :
  BinaryFan.snd
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
            ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
              NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y)))) =
    Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      BinaryFan.snd
        (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
          (snd (i.obj X) (i.obj Y)))
⊢ (Cone.postcompose (pairComp X Y i).hom).obj
      (i.mapCone
        (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
          ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
          ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))) ≅
    BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
      (snd (i.obj X) (i.obj Y))

Tactic:
fapply BinaryFan.ext

Premises used: CategoryTheory.Limits.BinaryFan.ext
-- 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
X Y : D
e :
  (reflector i ⋙ i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) ≅
    Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
⊢ ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
            ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
              NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y)))).pt ≅
    Cone.pt.{0, v₁, 0, u₁} (F := pair (i.obj X) (i.obj Y))
      (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
        (snd (i.obj X) (i.obj Y)))

Tactic:
change (reflector i ⋙ i).obj (i.obj X ⊗ i.obj Y) ≅ (𝟭 C).obj (i.obj X ⊗ i.obj Y)

Premises used: CategoryTheory.reflector, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.Functor.obj
-- 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
X Y : D
h : i.essImage (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))) (Y :=
    (reflector i ⋙ i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))

Tactic:
apply Functor.essImage.unit_isIso

Premises used: CategoryTheory.Functor.essImage.unit_isIso
-- 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
X Y : D
⊢ HasFiniteProducts.{v₁, u₂} D

Tactic:
haveI := reflective_products i
-- 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
X Y : D
this : HasFiniteProducts.{v₁, u₂} D
h : Nonempty.{v₁ + 1} (i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
⊢ i.essImage (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))

Tactic:
use Limits.prod X Y

Premises used: CategoryTheory.Limits.prod
-- 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
X Y : D
this : HasFiniteProducts.{v₁, u₂} D
h : i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)
⊢ Nonempty.{v₁ + 1} (i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))

Tactic:
constructor
-- 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
X Y : D
this : HasFiniteProducts.{v₁, u₂} D
h : Limits.prod.{v₁, u₁} (i.obj X) (i.obj Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)
⊢ i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)

Tactic:
apply Limits.PreservesLimitPair.iso i _ _ |>.trans

Premises used: CategoryTheory.Limits.PreservesLimitPair.iso, CategoryTheory.Iso.trans
-- 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
X Y : D
this : HasFiniteProducts.{v₁, u₂} D
⊢ Limits.prod.{v₁, u₁} (i.obj X) (i.obj Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)

Tactic:
refine Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
              (tensorProductIsBinaryProduct _ _)

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.pair, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct, CategoryTheory.Functor.obj
-- 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
X Y : D
this : IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))) (Y :=
  (reflector i ⋙ i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
  (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))) :=
  ⋯
⊢ (reflector i ⋙ i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) ≅
    Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))

Tactic:
exact asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) |>.symm

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.reflectorAdjunction, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.Iso.symm, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- 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
X Y : D
h₁ :
  Eq (α :=
    Functor.obj.{0, v₁, 0, u₁}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₁, 0, u₁} (pair (i.obj X) (i.obj Y)) { as := WalkingPair.left : Discrete WalkingPair })
    (((i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).π ≫
          (diagramIsoPair (pair X Y ⋙ i)).hom).app
      { as := WalkingPair.left })
    (Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
            (snd (i.obj X) (i.obj Y))))
        { as := WalkingPair.left })
⊢ BinaryFan.fst
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
            ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
              NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y)))) =
    Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      BinaryFan.fst
        (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
          (snd (i.obj X) (i.obj Y)))

Tactic:
simp only [BinaryFan.fst, Cone.postcompose, pairComp]

Premises used: CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.Limits.pairComp, CategoryTheory.Limits.Cone.postcompose
-- 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
X Y : D
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₁, 0, u₁} (pair (i.obj X) (i.obj Y)) { as := WalkingPair.left : Discrete WalkingPair })
    (((i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).π ≫
          (diagramIsoPair (pair X Y ⋙ i)).hom).app
      { as := WalkingPair.left })
    (Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
            (snd (i.obj X) (i.obj Y))))
        { as := WalkingPair.left })

Tactic:
simp [← Functor.comp_map, ← NatTrans.naturality_assoc]

Premises used: CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc
-- 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
X Y : D
h₂ :
  Eq (α :=
    Functor.obj.{0, v₁, 0, u₁}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₁, 0, u₁} (pair (i.obj X) (i.obj Y)) { as := WalkingPair.right : Discrete WalkingPair })
    (((i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).π ≫
          (diagramIsoPair (pair X Y ⋙ i)).hom).app
      { as := WalkingPair.right })
    (Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
            (snd (i.obj X) (i.obj Y))))
        { as := WalkingPair.right })
⊢ BinaryFan.snd
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
            ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
              NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y)))) =
    Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      BinaryFan.snd
        (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
          (snd (i.obj X) (i.obj Y)))

Tactic:
simp only [BinaryFan.snd, Cone.postcompose, pairComp]

Premises used: CategoryTheory.Limits.pairComp, CategoryTheory.Limits.BinaryFan.snd, CategoryTheory.Limits.Cone.postcompose
-- 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
X Y : D
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₁, 0, u₁} (pair (i.obj X) (i.obj Y)) { as := WalkingPair.right : Discrete WalkingPair })
    (((i.mapCone
              (BinaryFan.mk (P := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))
                ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫
                  NatTrans.app (Adjunction.counit (reflectorAdjunction i)) Y))).π ≫
          (diagramIsoPair (pair X Y ⋙ i)).hom).app
      { as := WalkingPair.right })
    (Iso.hom
        (_root_.id
          (Iso.symm
            (asIso
              (NatTrans.app (Adjunction.unit (reflectorAdjunction i))
                (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)))))) ≫
      NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)) (fst (i.obj X) (i.obj Y))
            (snd (i.obj X) (i.obj Y))))
        { as := WalkingPair.right })

Tactic:
simp [← Functor.comp_map, ← NatTrans.naturality_assoc]

Premises used: CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc
-- 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 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : Functor.{v₁, v₁, u₁, u₂} C D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
⊢ ExponentialIdeal i

Tactic:
apply ExponentialIdeal.mk'

Premises used: CategoryTheory.ExponentialIdeal.mk'
-- 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 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : Functor.{v₁, v₁, u₁, u₂} C D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
apply : (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) ⟶ B
⊢ i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B

Tactic:
apply MonoidalClosed.curry (ir.homEquiv _ _ _)

Premises used: CategoryTheory.MonoidalClosed.curry, CategoryTheory.Adjunction.homEquiv, DFunLike.coe
-- 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 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : Functor.{v₁, v₁, u₁, u₂} C D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
apply :
  (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) ⟶
    (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B))
⊢ (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) ⟶ B

Tactic:
apply _ ≫ (ir.homEquiv _ _).symm ((ihom.ev A).app (i.obj B))

Premises used: CategoryTheory.ihom.ev, CategoryTheory.Adjunction.homEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- 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 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : Functor.{v₁, v₁, u₁, u₂} C D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
⊢ (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) ⟶
    (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B))

Tactic:
exact prodComparison L A _ ≫ (_ ◁ (ε.app _)) ≫ inv (prodComparison _ _ _)

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.inv, CategoryTheory.CartesianMonoidalCategory.prodComparison, CategoryTheory.NatTrans.app