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
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
⊢ 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))
have 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))
Tactic: rw [← F.map_comp, ← F.map_comp]
-- 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))))
B : C
⊢ 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))
have 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))
Tactic: simp only [Functor.map_comp]
-- 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))))
B : C
⊢ 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))
have 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))
Tactic: apply IsIso.eq_inv_of_inv_hom_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
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
⊢ 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))
have 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))
Tactic: simp only [Category.assoc]
-- 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))))
B : C
⊢ 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))
have 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))
Tactic: rw [prodComparison_natural_whiskerLeft, prodComparison_natural_whiskerRight_assoc]
-- 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))))
B : C
| 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)))
have a : prodComparison (L ⋙ F) (F.obj A) (F.obj B)
Tactic: rw [← prodComparison_comp]
-- 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))))
B : C
⊢ 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))
have 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))
Tactic: slice_lhs 2 3 => rw [← prodComparison_comp]
-- 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))))
B : C
⊢ 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))
have 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))
Tactic: simp only [Category.assoc]
-- 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))))
B : C
⊢ 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))
have 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))
Tactic: unfold prodComparison
-- 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
i : IsIso (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A)) (natTrans (expComparison F A))
⊢ IsIso (X := tensorLeft (F.obj A) ⋙ L) (Y := L ⋙ tensorLeft A) (natTrans (frobeniusMorphism F h A))
have 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))
Tactic: rw [← frobeniusMorphism_mate F h] at i
Cleared hypotheses: i
-- 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
i : IsIso (X := tensorLeft (F.obj A) ⋙ L) (Y := L ⋙ tensorLeft A) (frobeniusMorphism F h A)
⊢ IsIso (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A)) (natTrans (expComparison F A))
have rw : 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
j : J
k₁ k₂ : Under.{v₂, u₂} j
φ : k₁ ⟶ k₂
⊢ Eq (α :=
    F₂.obj j ⟶ Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k₁)) k₂)
    ((fun (k : Under.{v₂, u₂} j) ↦
          (F₂.map k.hom ≫ curry (f.app k.right) :
            F₂.obj j ⟶
              Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k))
        k₁ ≫
      Functor.map (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k₁)) φ)
    ((fun (k : Under.{v₂, u₂} j) ↦
          (F₂.map k.hom ≫ curry (f.app k.right) :
            F₂.obj j ⟶
              Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k))
        k₂ ≫
      NatTrans.app (Functor.map (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) φ.op) k₂)
have dsimp : Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
  (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₁.right))
    (F₂.map k₁.hom ≫ curry (f.app k₁.right)) (eHomWhiskerLeft C (F₁.obj k₁.right) (F₃.map (Under.Hom.right φ))))
  (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
    (F₂.map k₂.hom ≫ curry (f.app k₂.right)) (eHomWhiskerRight C (F₁.map (Under.Hom.right φ)) (F₃.obj k₂.right)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
j : J
k₁ k₂ : Under.{v₂, u₂} j
φ : k₁ ⟶ k₂
⊢ Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₁.right))
      (F₂.map k₁.hom ≫ curry (f.app k₁.right)) (eHomWhiskerLeft C (F₁.obj k₁.right) (F₃.map (Under.Hom.right φ))))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
      (F₂.map k₂.hom ≫ curry (f.app k₂.right)) (eHomWhiskerRight C (F₁.map (Under.Hom.right φ)) (F₃.obj k₂.right)))
have simp : Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
  (F₂.map k₁.hom ≫ curry (f.app k₁.right) ≫ Functor.map (ihom (F₁.obj k₁.right)) (F₃.map (Under.Hom.right φ)))
  (F₂.map k₂.hom ≫
    CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
      (curry (f.app k₂.right)) (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
Tactic: simp only [enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Category.assoc,
            enrichedOrdinaryCategorySelf_eHomWhiskerRight]