awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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)
⊢ Eq (α := Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (inv (prodComparison F A B)) (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (𝟭 C) B))
have h : 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: apply IsIso.inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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
⊢ 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))
have 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))
Tactic: rw [uncurry_eq, expComparison_ev]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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))
⊢ 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))
have 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))
Tactic: rw [uncurry_eq, expComparison_ev]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (hypothesis)
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')))
    (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 (tensoringLeft D) (F.map f))))
    (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 (tensoringLeft C) f)))
have 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')))
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)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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')))
⊢ 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)
have 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)
Tactic: ext B
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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)
      (F.map f ▷ F.obj B ≫ inv (prodComparison F A B)))
    (F.map (f ▷ B))
have 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))
Tactic: rw [← prodComparison_inv_natural_whiskerRight F f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (hypothesis)
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))
    ((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))
have 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))))
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)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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))))
⊢ 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))
have 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))))
Tactic: rw [← conjeq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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))))
⊢ 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)))
have 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)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
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))))
⊢ 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)
have 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)
Tactic: ext B