awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ IsLimit
    (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))
have t : 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 isLimitOfReflects i
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ 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)))
have 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))
Tactic: apply IsLimit.equivOfNatIsoOfIso (pairComp X Y _) _ _ _ |>.invFun
          (tensorProductIsBinaryProduct (i.obj X) (i.obj Y))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ (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))
have 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)))
Tactic: fapply BinaryFan.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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)))
⊢ (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))
have 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)))
Tactic: fapply BinaryFan.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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)))
⊢ (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))
have 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)))
Tactic: fapply BinaryFan.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ ((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)))
have 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))
Tactic: change (reflector i ⋙ i).obj (i.obj X ⊗ i.obj Y) ≅ (𝟭 C).obj (i.obj X ⊗ i.obj Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ 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)))
have h : i.essImage (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
Tactic: apply Functor.essImage.unit_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (hypothesis)
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
⊢ i.essImage (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
have this : HasFiniteProducts.{v₁, u₂} D
Tactic: haveI := reflective_products i
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ i.essImage (tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
have h : Nonempty.{v₁ + 1} (i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
Tactic: use Limits.prod X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ Nonempty.{v₁ + 1} (i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y))
have h : i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ i.obj (Limits.prod.{v₁, u₂} X Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)
have h : Limits.prod.{v₁, u₁} (i.obj X) (i.obj Y) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj X) (i.obj Y)
Tactic: apply Limits.PreservesLimitPair.iso i _ _ |>.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ 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)))
have 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 })
Tactic: simp only [BinaryFan.fst, Cone.postcompose, pairComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ 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)))
have 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 })
Tactic: simp only [BinaryFan.snd, Cone.postcompose, pairComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ ExponentialIdeal i
have h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
Tactic: apply ExponentialIdeal.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
⊢ i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B
have apply : (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) ⟶ B
Tactic: apply MonoidalClosed.curry (ir.homEquiv _ _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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)))) ⟶ B
have 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))
Tactic: apply _ ≫ (ir.homEquiv _ _).symm ((ihom.ev A).app (i.obj B))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
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
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) B :
        (a : (reflector i).obj (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) ⟶ B) → A ⊗ i.obj (L.obj (A ⟹ i.obj B)) ⟶ i.obj B)
      (CategoryStruct.comp (Y := (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)))
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) (L.obj A) (L.obj (i.obj (L.obj (A ⟹ i.obj B)))))
          (prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))))
          (L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))))
        ((Equiv.symm (ir.homEquiv (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)) B) :
            (a : (ihom A ⋙ tensorLeft A).obj (i.obj B) ⟶ i.obj B) →
              (reflector i).obj ((ihom A ⋙ tensorLeft A).obj (i.obj B)) ⟶ B)
          (NatTrans.app (ihom.ev A) (i.obj B)))))
⊢ η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
have rw : Eq (α := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (A ⟹ i.obj B)) ⟶ B)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj (A ⟹ i.obj B)))
    (prodComparison (reflector i) A (A ⟹ i.obj B))
    (CategoryStruct.comp (Y := (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)))
      (inv (prodComparison (reflector i) A (A ⟹ i.obj B)))
      ((Equiv.symm (ir.homEquiv (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)) B) :
          (a : (ihom A ⋙ tensorLeft A).obj (i.obj B) ⟶ i.obj B) →
            (reflector i).obj ((ihom A ⋙ tensorLeft A).obj (i.obj B)) ⟶ B)
        (NatTrans.app (ihom.ev A) (i.obj B)))))
  ((Equiv.symm (ir.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) A (A ⟹ i.obj B)) B) :
      (a : A ⊗ (A ⟹ i.obj B) ⟶ i.obj B) → (reflector i).obj (A ⊗ (A ⟹ i.obj B)) ⟶ B)
    (NatTrans.app (ihom.ev A) (i.obj B)))
Tactic: rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left,
      ir.homEquiv_apply_eq, Category.assoc, Category.assoc,
      prodComparison_natural_whiskerLeft_assoc, ← whiskerLeft_comp_assoc,
      ir.left_triangle_components, whiskerLeft_id, Category.id_comp]