awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
e_w :
  ∀ (B : C),
    Eq (α := (F ⋙ tensorLeft (F.obj A)).obj B ⟶ (tensorLeft A ⋙ F).obj B)
      (NatTrans.app
        (natTrans
          ((mateEquiv h h :
              (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
                TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
            (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A)))))
        B)
      (NatTrans.app (natTrans (Iso.inv (prodComparisonNatIso F A))) B)
⊢ Eq (α := TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
    ((mateEquiv h h :
          (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
            TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
        (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))) :
      TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
    (Iso.inv (prodComparisonNatIso F A) :
      F ⋙ Functor.obj (curriedTensor D) (F.obj A) ⟶ Functor.obj (curriedTensor C) A ⋙ F)

Tactic:
ext B
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      F.map (prodComparison L (F.obj A) (F.obj B) ≫ h.counit.app A ▷ L.obj (F.obj B) ≫ A ◁ h.counit.app B))
    (inv (prodComparison F A B))
⊢ Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫
        F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B))
    (inv (prodComparison F A B))

Tactic:
rw [← F.map_comp, ← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫
        F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B))
    (inv (prodComparison F A B))
⊢ Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      F.map (prodComparison L (F.obj A) (F.obj B) ≫ h.counit.app A ▷ L.obj (F.obj B) ≫ A ◁ h.counit.app B))
    (inv (prodComparison F A B))

Tactic:
simp only [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
      (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
        F.map (prodComparison L (F.obj A) (F.obj B)) ≫
          F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B))
      (prodComparison F A B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))
⊢ Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫
        F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B))
    (inv (prodComparison F A B))

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Premises used: CategoryTheory.IsIso.eq_inv_of_inv_hom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) (L.obj (F.obj A)) (L.obj (F.obj B))))
        (F.map (prodComparison L (F.obj A) (F.obj B)))
        (F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B) ≫ prodComparison F A B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
      (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
        F.map (prodComparison L (F.obj A) (F.obj B)) ≫
          F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B))
      (prodComparison F A B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) (L.obj (F.obj A)) (L.obj (F.obj B))))
        (F.map (prodComparison L (F.obj A) (F.obj B)))
        (prodComparison F (L.obj (F.obj A)) (L.obj (F.obj B)) ≫
          F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B)) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))
⊢ h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) (L.obj (F.obj A)) (L.obj (F.obj B))))
        (F.map (prodComparison L (F.obj A) (F.obj B)))
        (F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B) ≫ prodComparison F A B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))

Tactic:
rw [prodComparison_natural_whiskerLeft, prodComparison_natural_whiskerRight_assoc]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
a : prodComparison (L ⋙ F) (F.obj A) (F.obj B)
| CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) (L.obj (F.obj A)) (L.obj (F.obj B))))
    (F.map (prodComparison L (F.obj A) (F.obj B))) (prodComparison F (L.obj (F.obj A)) (L.obj (F.obj B)))

Tactic:
rw [← prodComparison_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      (prodComparison (L ⋙ F) (F.obj A) (F.obj B) ≫ F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B))) ≫
        F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))
⊢ h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) (L.obj (F.obj A)) (L.obj (F.obj B))))
        (F.map (prodComparison L (F.obj A) (F.obj B)))
        (prodComparison F (L.obj (F.obj A)) (L.obj (F.obj B)) ≫
          F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B)) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))

Tactic:
slice_lhs 2 3 => rw [← prodComparison_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      prodComparison (L ⋙ F) (F.obj A) (F.obj B) ≫
        F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))
⊢ h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      (prodComparison (L ⋙ F) (F.obj A) (F.obj B) ≫ F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B))) ≫
        F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      lift ((L ⋙ F).map (fst (F.obj A) (F.obj B))) ((L ⋙ F).map (snd (F.obj A) (F.obj B))) ≫
        F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))
⊢ h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      prodComparison (L ⋙ F) (F.obj A) (F.obj B) ≫
        F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))

Tactic:
unfold prodComparison

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
⊢ h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      lift ((L ⋙ F).map (fst (F.obj A) (F.obj B))) ((L ⋙ F).map (snd (F.obj A) (F.obj B))) ≫
        F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A)) (natTrans (expComparison F A))
⊢ IsIso (C := Functor.{v, v, u, u'} C D) (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
          (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
        (natTrans (frobeniusMorphism F h A)) :
      ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))

Tactic:
rw [← frobeniusMorphism_mate F h] at i

Premises used: CategoryTheory.frobeniusMorphism_mate
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso (C := Functor.{v, v, u, u'} C D) (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
          (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
        (natTrans (frobeniusMorphism F h A)) :
      ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
⊢ IsIso (X := tensorLeft (F.obj A) ⋙ L) (Y := L ⋙ tensorLeft A) (natTrans (frobeniusMorphism F h A))

Tactic:
@conjugateEquiv_of_iso _ _ _ _ _ _ _ _ _ _ _ i

Premises used: CategoryTheory.conjugateEquiv_of_iso