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
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1 :
  (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶ (F ⋙ ihom (F.obj A)).obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
    (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶
      (F ⋙ ihom (F.obj A)).obj (Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A) B))
e_4 :
  Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A) ⋙ ihom (F.obj A)) (F.obj B) =
    Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A) ⋙ ihom (F.obj A))
      (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B))
e_5 :
  Functor.obj.{v, v, u', u'} (ihom (F.obj A)) (F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
    Functor.obj.{v, v, u', u'} (ihom (F.obj A))
      ((Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B))
e_6 :
  Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) =
    Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B))
e_7 :
  F.obj (tensorObj.{v, u} (𝒞 := inst) A B) =
    (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B)
⊢ CategoryStruct.comp (Y := Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B)) (prodComparison F A B)
      (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (𝟭 C) B)) =
    𝟙 (F.obj (tensorObj.{v, u} (𝒞 := inst) A 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
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
rw :
  Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ F.obj B)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (Functor.obj.{v, v, u', u'} (ihom (F.obj A)) (F.obj B)))
      (F.obj A ◁ NatTrans.app (natTrans (expComparison F A)) B) (NatTrans.app (ihom.ev (F.obj A)) (F.obj B)))
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)) ≫ F.map (NatTrans.app (ihom.ev A) B))
rw₁ rw₂ :
  Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ F.obj B)
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)) ≫ F.map (NatTrans.app (ihom.ev A) B))
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)) ≫ F.map (NatTrans.app (ihom.ev A) B))
⊢ Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ F.obj B)
    (uncurry (NatTrans.app (natTrans (expComparison F A)) B))
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)) ≫ F.map (NatTrans.app (ihom.ev A) B))

Tactic:
rw [uncurry_eq, expComparison_ev]

Premises used: CategoryTheory.MonoidalClosed.uncurry_eq, CategoryTheory.expComparison_ev
-- 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
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
⊢ Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
        ((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)))
          (Iso.inv (prodComparisonNatIso F A)))
        ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
            (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
          (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))

Tactic:
have vcomp1 := mateEquiv_conjugateEquiv_vcomp
    (ihom.adjunction A) (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))
    ((prodComparisonNatIso F A).inv) (((curriedTensor D).map (F.map f)))
-- 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
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
        ((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)))
          (Iso.inv (prodComparisonNatIso F A)))
        ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
            (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
          (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
⊢ Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerLeft (Iso.inv (prodComparisonNatIso F A')) (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerTop (T' := ihom A')
        ((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')))
          (Iso.inv (prodComparisonNatIso F A')))
        ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A') :
            (a : tensorLeft A' ⟶ tensorLeft A) → ihom A ⟶ ihom A')
          (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))

Tactic:
have vcomp2 := conjugateEquiv_mateEquiv_vcomp
    (ihom.adjunction A) (ihom.adjunction A') (ihom.adjunction (F.obj A'))
    (((curriedTensor C).map f)) ((prodComparisonNatIso F A').inv)
-- 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
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
        ((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)))
          (Iso.inv (prodComparisonNatIso F A)))
        ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
            (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
          (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
vcomp2 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerLeft (Iso.inv (prodComparisonNatIso F A')) (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerTop (T' := ihom A')
        ((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')))
          (Iso.inv (prodComparisonNatIso F A')))
        ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A') :
            (a : tensorLeft A' ⟶ tensorLeft A) → ihom A ⟶ ihom A')
          (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
h :
  ∀ (B : C),
    Eq (α := (F ⋙ tensorLeft (F.obj A')).obj B ⟶ (tensorLeft A ⋙ F).obj B)
      (NatTrans.app
        (F.whiskerLeft (Functor.map (curriedTensor D) (F.map f)) ≫ natTrans (Iso.inv (prodComparisonNatIso F A))) B)
      (NatTrans.app
        (natTrans (Iso.inv (prodComparisonNatIso F A')) ≫ Functor.whiskerRight (Functor.map (curriedTensor C) f) F) B)
⊢ Eq (α := F ⋙ tensorLeft (F.obj A') ⟶ tensorLeft A ⋙ F)
    (F.whiskerLeft (Functor.map (curriedTensor D) (F.map f)) ≫ natTrans (Iso.inv (prodComparisonNatIso F A)))
    (natTrans (Iso.inv (prodComparisonNatIso F A')) ≫ Functor.whiskerRight (Functor.map (curriedTensor C) f) 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
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
        ((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)))
          (Iso.inv (prodComparisonNatIso F A)))
        ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
            (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
          (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
vcomp2 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerLeft (Iso.inv (prodComparisonNatIso F A')) (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerTop (T' := ihom A')
        ((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')))
          (Iso.inv (prodComparisonNatIso F A')))
        ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A') :
            (a : tensorLeft A' ⟶ tensorLeft A) → ihom A ⟶ ihom A')
          (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
B : C
h :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A') (F.obj B)) (prodComparison F A' B)
      (inv (prodComparison F A' B) ≫ F.map (f ▷ B)))
    (F.map (f ▷ B))
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A') (F.obj B)) (prodComparison F A' B)
      (F.map f ▷ F.obj B ≫ inv (prodComparison F A B)))
    (F.map (f ▷ B))

Tactic:
rw [← prodComparison_inv_natural_whiskerRight F f]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerRight
-- 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
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
        ((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)))
          (Iso.inv (prodComparisonNatIso F A)))
        ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
            (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
          (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
vcomp2 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((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')))
        (TwoSquare.whiskerLeft (Iso.inv (prodComparisonNatIso F A')) (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerTop (T' := ihom A')
        ((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')))
          (Iso.inv (prodComparisonNatIso F A')))
        ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A') :
            (a : tensorLeft A' ⟶ tensorLeft A) → ihom A ⟶ ihom A')
          (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
B : C
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A') (F.obj B)) (prodComparison F A' B)
      (inv (prodComparison F A' B) ≫ F.map (f ▷ B)))
    (F.map (f ▷ 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
⊢ 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))))

Tactic:
have conjeq := iterated_mateEquiv_conjugateEquiv h h
    (ihom.adjunction (F.obj A)) (ihom.adjunction A)
    (prodComparisonNatTrans L (F.obj A) ≫
      Functor.whiskerLeft L ((curriedTensor C).map (h.counit.app A)))
-- 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))))
rw :
  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))))))
    (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)))
        (Iso.inv (prodComparisonNatIso F A))))
⊢ Eq (α := ihom A ⋙ F ⟶ 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
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A)))) :
      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)))
          (Iso.inv (prodComparisonNatIso F A))) :
      ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))

Tactic:
rw [← conjeq]
-- 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 :
  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)
⊢ Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A)))
    ((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)))) :
      TwoSquare (ihom A) F F (ihom (F.obj A)))
    ((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)))
        (Iso.inv (prodComparisonNatIso F A)) :
      TwoSquare (ihom A) F F (ihom (F.obj A)))

Tactic:
apply congr_arg

Premises used: congr_arg