awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
w :
  ∀ (x : C) (x_1 : (obj (𝟭 (C ⥤ Type (max w v u))) G).obj x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Functor.map (𝟭 (C ⥤ Type (max w v u))) f ≫
              Equiv.invFun (functorHomEquiv.{w, v, u} F H (obj (tensorLeft F) H)) (𝟙 (tensorObj (𝒞 := category) F H)))
            x))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Equiv.invFun (functorHomEquiv.{w, v, u} F G (obj (tensorLeft F) G)) (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                  (tensorLeft F ⋙ rightAdj.{w, v, u} F).map f).app
              x)).toFun
        x_1
⊢ Functor.map (𝟭 (C ⥤ Type (max w v u))) f ≫
      Equiv.invFun (functorHomEquiv.{w, v, u} F H (obj (tensorLeft F) H)) (𝟙 (tensorObj (𝒞 := category) F H)) =
    Equiv.invFun (functorHomEquiv.{w, v, u} F G (obj (tensorLeft F) G)) (𝟙 (tensorObj (𝒞 := category) F G)) ≫
      (tensorLeft F ⋙ rightAdj.{w, v, u} F).map f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x : C
x_1 : (obj (𝟭 (C ⥤ Type (max w v u))) G).obj x
w :
  Eq (α := F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (f ≫
                  (Equiv.symm (functorHomEquiv.{w, v, u} F H (tensorObj (𝒞 := category) F H)) :
                      (a : F ⊗ H ⟶ F ⊗ H) → H ⟶ F.functorHom (F ⊗ H))
                    (𝟙 (tensorObj (𝒞 := category) F H)))
                x) :
            TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
          (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
        x_1 :
      F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                ((Equiv.symm (functorHomEquiv.{w, v, u} F G (tensorObj (𝒞 := category) F G)) :
                      (a : F ⊗ G ⟶ F ⊗ G) → G ⟶ F.functorHom (F ⊗ G))
                    (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                  (rightAdj.{w, v, u} F).map (F ◁ f))
                x) :
            TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
          (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
        x_1 :
      F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map (𝟭 (C ⥤ Type (max w v u))) f ≫
            Equiv.invFun (functorHomEquiv.{w, v, u} F H (obj (tensorLeft F) H)) (𝟙 (tensorObj (𝒞 := category) F H)))
          x))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Equiv.invFun (functorHomEquiv.{w, v, u} F G (obj (tensorLeft F) G)) (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                (tensorLeft F ⋙ rightAdj.{w, v, u} F).map f).app
            x)).toFun
      x_1

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x : C
x_1 : (obj (𝟭 (C ⥤ Type (max w v u))) G).obj x
x_2 : C
x_3 : obj (obj coyoneda (Opposite.op x)) x_2
x_4 : F.obj x_2
⊢ Eq (α := F.obj x_2)
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (HomObj.app
            (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (NatTrans.app
                      (f ≫
                        (Equiv.symm (functorHomEquiv.{w, v, u} F H (tensorObj (𝒞 := category) F H)) :
                            (a : F ⊗ H ⟶ F ⊗ H) → H ⟶ F.functorHom (F ⊗ H))
                          (𝟙 (tensorObj (𝒞 := category) F H)))
                      x) :
                  TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
                (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
              x_1)
            x_2 x_3))
        x_4).1
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (HomObj.app
            (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (NatTrans.app
                      ((Equiv.symm (functorHomEquiv.{w, v, u} F G (tensorObj (𝒞 := category) F G)) :
                            (a : F ⊗ G ⟶ F ⊗ G) → G ⟶ F.functorHom (F ⊗ G))
                          (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                        (rightAdj.{w, v, u} F).map (F ◁ f))
                      x) :
                  TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
                (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
              x_1)
            x_2 x_3))
        x_4).1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x : C
x_1 : (obj (𝟭 (C ⥤ Type (max w v u))) G).obj x
x_2 : C
x_3 : obj (obj coyoneda (Opposite.op x)) x_2
x_4 : F.obj x_2
⊢ Eq (α := H.obj x_2)
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (HomObj.app
            (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (NatTrans.app
                      (f ≫
                        (Equiv.symm (functorHomEquiv.{w, v, u} F H (tensorObj (𝒞 := category) F H)) :
                            (a : F ⊗ H ⟶ F ⊗ H) → H ⟶ F.functorHom (F ⊗ H))
                          (𝟙 (tensorObj (𝒞 := category) F H)))
                      x) :
                  TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
                (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
              x_1)
            x_2 x_3))
        x_4).2
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (HomObj.app
            (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (NatTrans.app
                      ((Equiv.symm (functorHomEquiv.{w, v, u} F G (tensorObj (𝒞 := category) F G)) :
                            (a : F ⊗ G ⟶ F ⊗ G) → G ⟶ F.functorHom (F ⊗ G))
                          (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                        (rightAdj.{w, v, u} F).map (F ◁ f))
                      x) :
                  TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
                (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
              x_1)
            x_2 x_3))
        x_4).2

Tactic:
simp
-- 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 : MonoidalClosed.{v₁, u₁} C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B : C
hB : i.essImage B
A : C
rcases : ∀ (B' : D) (iB' : i.obj B' ≅ B), i.essImage (A ⟹ B)
⊢ i.essImage (A ⟹ B)

Tactic:
rcases hB with ⟨B', ⟨iB'⟩⟩
-- 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 : MonoidalClosed.{v₁, u₁} C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B A : C
B' : D
iB' : i.obj B' ≅ B
⊢ i.essImage (A ⟹ B)

Tactic:
Functor.essImage.ofIso ((ihom A).mapIso iB') (h B' A)

Premises used: CategoryTheory.Functor.essImage.ofIso, CategoryTheory.ihom, CategoryTheory.Functor.mapIso
-- 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 : MonoidalClosed.{v₁, u₁} C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B A : C
B' : D
iB' : i.obj B' ≅ B
⊢ i.essImage (A ⟹ B)

Tactic:
exact Functor.essImage.ofIso ((ihom A).mapIso iB') (h B' A)

Premises used: CategoryTheory.Functor.essImage.ofIso, CategoryTheory.ihom, CategoryTheory.Functor.mapIso
-- 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 : MonoidalClosed.{v₁, u₁} C
⊢ ExponentialIdeal.{v₁, u₁, u₁} (𝟭 C)

Tactic:
ExponentialIdeal.mk' _ fun _ _ => ⟨_, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Functor.id, CategoryTheory.Iso.refl, Nonempty.intro, CategoryTheory.ExponentialIdeal.mk', Exists.intro, CategoryTheory.ihom, 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 : MonoidalClosed.{v₁, u₁} C
h :
  ∀ (B : Subterminals.{v₁, u₁} C) (A : C),
    Functor.essImage.{v₁, v₁, u₁, u₁} (C := Subterminals.{v₁, u₁} C) (subterminalInclusion C)
      (A ⟹ Functor.obj (subterminalInclusion C) B)
⊢ ExponentialIdeal.{v₁, u₁, u₁} (D := Subterminals.{v₁, u₁} C) (subterminalInclusion C)

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 : MonoidalClosed.{v₁, u₁} C
B : Subterminals.{v₁, u₁} C
A : C
⊢ Functor.essImage.{v₁, v₁, u₁, u₁} (C := Subterminals.{v₁, u₁} C) (subterminalInclusion C)
    (A ⟹ Functor.obj (subterminalInclusion C) B)

Tactic:
⟨⟨A ⟹ B.1, fun Z g h => ?_⟩, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Iso.refl, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro, CategoryTheory.ihom, 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 : MonoidalClosed.{v₁, u₁} C
B : Subterminals.{v₁, u₁} C
A : C
h : ∀ (Z : C) (g h : Z ⟶ A ⟹ B.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)), g = h
⊢ Functor.essImage.{v₁, v₁, u₁, u₁} (C := Subterminals.{v₁, u₁} C) (subterminalInclusion C)
    (A ⟹ Functor.obj (subterminalInclusion C) B)

Tactic:
refine ⟨⟨A ⟹ B.1, fun Z g h => ?_⟩, ⟨Iso.refl _⟩⟩
-- 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 : MonoidalClosed.{v₁, u₁} C
B : Subterminals.{v₁, u₁} C
A Z : C
g h : Z ⟶ A ⟹ B.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)
⊢ g = h

Tactic:
uncurry_injective (B.2 (MonoidalClosed.uncurry g) (MonoidalClosed.uncurry h))

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.MonoidalClosed.uncurry_injective
-- 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 : MonoidalClosed.{v₁, u₁} C
B : Subterminals.{v₁, u₁} C
A Z : C
g h : Z ⟶ A ⟹ B.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)
⊢ g = h

Tactic:
exact uncurry_injective (B.2 (MonoidalClosed.uncurry g) (MonoidalClosed.uncurry h))

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.MonoidalClosed.uncurry_injective
-- 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 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
symm : i ⋙ ihom A ≅ i ⋙ ihom A ⋙ reflector i ⋙ i
⊢ i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A

Tactic:
symm
-- 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 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
apply : (X : D) → (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X
apply₁ :
  ∀ {X Y : D} (f : X ⟶ Y),
    (i ⋙ ihom A).map f ≫ Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj Y))) =
      Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj X))) ≫
        (i ⋙ ihom A ⋙ reflector i ⋙ i).map f
⊢ i ⋙ ihom A ≅ i ⋙ ihom A ⋙ reflector i ⋙ i

Tactic:
apply NatIso.ofComponents _ _

Premises used: CategoryTheory.NatIso.ofComponents
-- 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 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
X : D
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (A ⟹ i.obj X)) (Y := (reflector i ⋙ i).obj (A ⟹ i.obj X))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj X))

Tactic:
haveI := Functor.essImage.unit_isIso (ExponentialIdeal.exp_closed (i.obj_mem_essImage X) A)
-- 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 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
X : D
this :
  IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (A ⟹ i.obj X)) (Y := (reflector i ⋙ i).obj (A ⟹ i.obj X))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj X))
⊢ (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X

Tactic:
apply asIso ((reflectorAdjunction i).unit.app (A ⟹ i.obj X))

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.reflectorAdjunction, CategoryTheory.ihom, 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 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
⊢ ∀ {X Y : D} (f : X ⟶ Y),
    (i ⋙ ihom A).map f ≫ Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj Y))) =
      Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj X))) ≫
        (i ⋙ ihom A ⋙ reflector i ⋙ i).map f

Tactic:
simp [asIso]

Premises used: 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 : MonoidalClosed.{v₁, u₁} C
inst_4 : Reflective i
h : (A : C) → i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
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 : MonoidalClosed.{v₁, u₁} C
inst_4 : Reflective i
h : (A : C) → i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
B : D
A : C
⊢ i.essImage (A ⟹ i.obj B)

Tactic:
⟨_, ⟨(h A).app B⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro, CategoryTheory.Iso.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 : MonoidalClosed.{v₁, u₁} C
inst_4 : Reflective i
h : (A : C) → i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
B : D
A : C
⊢ i.essImage (A ⟹ i.obj B)

Tactic:
exact ⟨_, ⟨(h A).app B⟩⟩
-- 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 : Limits.HasFiniteProducts.{v₁, u₁} C
inst_3 : Reflective i
⊢ Limits.HasFiniteProducts.{v₁, u₂} D

Tactic:
⟨fun _ => hasLimitsOfShape_of_reflective i⟩

Premises used: CategoryTheory.Limits.HasFiniteProducts.mk, CategoryTheory.hasLimitsOfShape_of_reflective
-- 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
t : IsLimit (i.mapCone (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
⊢ IsLimit.{0, v₁, 0, u₂} (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
apply isLimitOfReflects i

Premises used: CategoryTheory.Limits.isLimitOfReflects
-- 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
t :
  Cone.pt.{0, v₁, 0, u₁} (asEmptyCone (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≅
    (i.mapCone (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))).pt
⊢ IsLimit (i.mapCone (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))

Tactic:
apply isLimitChangeEmptyCone _ isTerminalTensorUnit

Premises used: CategoryTheory.Limits.isLimitChangeEmptyCone, CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit
-- 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
⊢ HasFiniteProducts.{v₁, u₂} D

Tactic:
have := 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
this : HasFiniteProducts.{v₁, u₂} D
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y :=
    (reflector i ⋙ i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
Functor.essImage.unit_isIso ⟨terminal D, ⟨PreservesTerminal.iso i |>.trans ?_⟩⟩

Premises used: CategoryTheory.Limits.PreservesTerminal.iso, Nonempty.intro, CategoryTheory.Functor.essImage.unit_isIso, CategoryTheory.Limits.terminal, CategoryTheory.Iso.trans, Exists.intro
-- 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
this : HasFiniteProducts.{v₁, u₂} D
refine : terminal.{v₁, u₁} C ≅ tensorUnit.{v₁, u₁} C (𝒞 := inst)
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y :=
    (reflector i ⋙ i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
refine Functor.essImage.unit_isIso ⟨terminal D, ⟨PreservesTerminal.iso i |>.trans ?_⟩⟩

Premises used: CategoryTheory.Limits.PreservesTerminal.iso, Nonempty.intro, CategoryTheory.Functor.essImage.unit_isIso, CategoryTheory.Limits.terminal, CategoryTheory.Iso.trans, Exists.intro
-- 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
this : HasFiniteProducts.{v₁, u₂} D
⊢ terminal.{v₁, u₁} C ≅ tensorUnit.{v₁, u₁} C (𝒞 := inst)

Tactic:
exact IsLimit.conePointUniqueUpToIso (limit.isLimit _) isTerminalTensorUnit

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit, CategoryTheory.Limits.limit.isLimit
-- 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
this : IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y :=
  (reflector i ⋙ i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) :=
  ⋯
⊢ Cone.pt.{0, v₁, 0, u₁} (asEmptyCone (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≅
    (i.mapCone (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))).pt

Tactic:
exact asIso ((reflectorAdjunction i).unit.app (𝟙_ C))

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.reflectorAdjunction, CategoryTheory.MonoidalCategoryStruct.tensorUnit, 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
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)))
⊢ 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))

Tactic:
apply isLimitOfReflects i

Premises used: CategoryTheory.Limits.isLimitOfReflects