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
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)))))
dsimp : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
⊢ η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)

Tactic:
dsimp
-- 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
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)))))
⊢ 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:
apply IsIso.hom_inv_id_assoc

Premises used: CategoryTheory.IsIso.hom_inv_id_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
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)

Tactic:
have : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B) := by
    dsimp
    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]
    apply IsIso.hom_inv_id_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
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)))))
this : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
⊢ IsSplitMono (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (A ⟹ i.obj B)) (η.app (A ⟹ i.obj B))

Tactic:
haveI : IsSplitMono (η.app (A ⟹ i.obj B)) := IsSplitMono.mk' ⟨_, this⟩
-- 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
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)))))
this_1 : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
this : IsSplitMono (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (A ⟹ i.obj B)) (η.app (A ⟹ i.obj B))
⊢ i.essImage (A ⟹ i.obj B)

Tactic:
apply mem_essImage_of_unit_isSplitMono

Premises used: CategoryTheory.mem_essImage_of_unit_isSplitMono
-- 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 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
comm1 : i ⋙ tensorLeft (i.obj B) ≅ tensorLeft B ⋙ i
comm2 : i ⋙ ihom (i.obj B) ≅ (i.essImage.lift (i ⋙ ihom (i.obj B)) ⋯ ⋙ l) ⋙ i
⊢ tensorLeft B ⊣ i.essImage.lift (i ⋙ ihom (i.obj B)) ⋯ ⋙ l

Tactic:
apply (ihom.adjunction (i.obj B)).restrictFullyFaithful i.fullyFaithfulOfReflective
          i.fullyFaithfulOfReflective

Premises used: CategoryTheory.Functor.fullyFaithfulOfReflective, CategoryTheory.Adjunction.restrictFullyFaithful, CategoryTheory.ihom.adjunction, 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
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
comm1 : tensorLeft B ⋙ i ≅ i ⋙ tensorLeft (i.obj B)
⊢ i ⋙ tensorLeft (i.obj B) ≅ tensorLeft B ⋙ i

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 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
comm1 : (X : D) → (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X
comm1₁ :
  ∀ {X Y : D} (f : X ⟶ Y),
    (tensorLeft B ⋙ i).map f ≫
        Iso.hom
          ((fun (X : D) ↦
              (asIso (prodComparison i B X) :
                i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
            Y) =
      Iso.hom
          ((fun (X : D) ↦
              (asIso (prodComparison i B X) :
                i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
            X) ≫
        (i ⋙ tensorLeft (i.obj B)).map f
⊢ tensorLeft B ⋙ i ≅ i ⋙ tensorLeft (i.obj B)

Tactic:
refine NatIso.ofComponents (fun X => ?_) (fun f => ?_)

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 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B X : D
⊢ Limits.PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i

Tactic:
haveI :=
              Adjunction.rightAdjoint_preservesLimits.{0, 0} (reflectorAdjunction 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
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B X : D
this : Limits.PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X

Tactic:
apply asIso (prodComparison i B X)

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison, 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
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B X Y : D
f : X ⟶ Y
comm1 :
  Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj Y))
    (i.map (B ◁ f) ≫ prodComparison i B Y) (prodComparison i B X ≫ i.obj B ◁ i.map f)
⊢ (tensorLeft B ⋙ i).map f ≫
      Iso.hom
        ((fun (X : D) ↦
            (asIso (prodComparison i B X) :
              i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
          Y) =
    Iso.hom
        ((fun (X : D) ↦
            (asIso (prodComparison i B X) :
              i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
          X) ≫
      (i ⋙ tensorLeft (i.obj B)).map f

Tactic:
dsimp [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 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B X Y : D
f : X ⟶ Y
comm1 comm1₁ :
  Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj Y))
    (prodComparison i B X ≫ i.obj B ◁ i.map f) (prodComparison i B X ≫ i.obj B ◁ i.map f)
⊢ Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj Y))
    (i.map (B ◁ f) ≫ prodComparison i B Y) (prodComparison i B X ≫ i.obj B ◁ i.map f)

Tactic:
rw [prodComparison_natural_whiskerLeft]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft
-- 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 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
⊢ i ⋙ ihom (i.obj B) ≅ (i.essImage.lift (i ⋙ ihom (i.obj B)) ⋯ ⋙ l) ⋙ i

Tactic:
exact (i.essImage.liftCompιIso _ _).symm.trans <|
            (Functor.isoWhiskerLeft _ φ.symm).trans (Functor.associator _ _ _).symm

Premises used: CategoryTheory.ObjectProperty.liftCompιIso, CategoryTheory.Functor.associator, CategoryTheory.Functor.essImage, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.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 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
h_fst :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
        CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
          (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
h_snd :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj B))
    ((NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
        CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
          (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
      (snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
      NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
        (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))

Tactic:
apply hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_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
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
h_fst :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
    (fst A B ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      i.map ((reflector i).map (fst A B)))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
        CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
          (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))

Tactic:
rw [tensorHom_fst, Category.assoc, Category.assoc, prodComparison_fst, ← i.map_comp,
    prodComparison_fst]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.Functor.map_comp
-- 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 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
    (fst A B ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      i.map ((reflector i).map (fst A B)))

Tactic:
apply (reflectorAdjunction i).unit.naturality

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.reflectorAdjunction, CategoryTheory.NatTrans.naturality
-- 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 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
h_snd :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj B))
    (snd A B ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      i.map ((reflector i).map (snd A B)))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj B))
    ((NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
        CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
          (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
      (snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))

Tactic:
rw [tensorHom_snd, Category.assoc, Category.assoc, prodComparison_snd, ← i.map_comp,
    prodComparison_snd]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_snd, CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.Functor.map_comp