awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
    (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)))
have rw : Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
  (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ 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: rw [← curry_natural_left_assoc, ← curry_natural_left_assoc,
            ← curry_natural_right, curry_pre_app, Category.assoc,
            ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc,
            ← Under.w φ, Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc,
            whisker_exchange_assoc]
-- 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₂
rw :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ 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)))
⊢ 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)))
have rw₁ : Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
  (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫
    Functor.map (ihom (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))
    (curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
    (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
Tactic: rw [← curry_natural_left_assoc, ← curry_natural_left_assoc,
            ← curry_natural_right, curry_pre_app, Category.assoc,
            ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc,
            ← Under.w φ, Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc,
            whisker_exchange_assoc]
-- 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₂
rw :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ 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)))
rw₁ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫
      Functor.map (ihom (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))
      (curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
      (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
⊢ 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)))
have rw₂ : Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
  (curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app 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))
    (curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
    (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
Tactic: rw [← curry_natural_left_assoc, ← curry_natural_left_assoc,
            ← curry_natural_right, curry_pre_app, Category.assoc,
            ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc,
            ← Under.w φ, Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc,
            whisker_exchange_assoc]
-- 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₂
rw :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ 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)))
rw₁ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫
      Functor.map (ihom (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))
      (curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
      (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
rw₂ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app 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))
      (curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
      (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
⊢ 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)))
have rw₃ : Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
  (curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ F₃.map (Under.Hom.right φ)))
  (curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
Tactic: rw [← curry_natural_left_assoc, ← curry_natural_left_assoc,
            ← curry_natural_right, curry_pre_app, Category.assoc,
            ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc,
            ← Under.w φ, Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc,
            whisker_exchange_assoc]
-- 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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ Eq (α := (tensorObj (𝒞 := Functor.category) F₁ F₂).obj j ⟶ F₃.obj j')
    ((tensorObj (𝒞 := Functor.category) F₁ F₂).map φ ≫
      uncurry (g.app j' ≫ enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j'))))
    (uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))) ≫ F₃.map φ)
have dsimp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
  ((F₁.map φ ⊗ₘ F₂.map φ) ≫
    uncurry (g.app j' ≫ enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j'))))
  (uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))) ≫ F₃.map φ)
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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    ((F₁.map φ ⊗ₘ F₂.map φ) ≫
      uncurry (g.app j' ≫ enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j'))))
    (uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))) ≫ F₃.map φ)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
  (uncurry
    (g.app j ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (diagram C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) (Opposite.op (Under.mk (𝟙 j'))))
          (Under.mk (𝟙 j')))
        (CategoryStruct.comp (Y :=
          @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))))
          (CategoryStruct.comp (Y :=
            @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _ ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
              ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
            (NatTrans.app
              (pre (NatTrans.app (Iso.inv (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₁))) (Under.mk (𝟙 j'))))
              ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
            (eHomWhiskerLeft C ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
              (NatTrans.app (Iso.hom (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₃))) (Under.mk (𝟙 j'))))))
        (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
  (uncurry
    (g.app j ≫
      CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
        (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))
Tactic: rw [← uncurry_natural_right, tensorHom_def'_assoc, ← uncurry_pre_app,
          ← uncurry_natural_left, Category.assoc, Category.assoc,
          NatTrans.naturality_assoc, functorEnrichedHom_map,
          end_.lift_π_assoc, enrichedOrdinaryCategorySelf_eHomWhiskerRight]
-- 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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
          (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
            (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
              enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
                @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
                  ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
                  ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
            (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
              (NatTrans.app (pre (𝟙 (F₁.obj j'))) (F₃.obj j')) (eHomWhiskerLeft C (F₁.obj j') (𝟙 (F₃.obj j')))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
  (uncurry
    (g.app j ≫
      CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
          enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
            @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
              ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
              ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
        (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
  (uncurry
    (g.app j ≫
      CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
        (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))
Tactic: rw [pre_id, NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerLeft,
          Functor.map_id, Category.comp_id, Category.comp_id]
-- 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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
            enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
                ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))
have e_a : Eq (α :=
  enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
    Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
  (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
    (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
      enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
          ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
          ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
    (NatTrans.app (pre (F₁.map φ)) (F₃.obj j')))
  (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
    (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
    (Functor.map (ihom (F₁.obj j)) (F₃.map φ)))
Tactic: congr 2
-- 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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ Eq (α :=
    enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
      (NatTrans.app (pre (F₁.map φ)) (F₃.obj j')))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
      (Functor.map (ihom (F₁.obj j)) (F₃.map φ)))
have e_a : Eq (α :=
  enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
    Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
  (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
    (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
      enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
          ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
          ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
    (eHomWhiskerRight C (F₁.map φ) (F₃.obj j')))
  (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
    (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
    (eHomWhiskerLeft C (F₁.obj j) (F₃.map φ)))
Tactic: rw [← enrichedOrdinaryCategorySelf_eHomWhiskerRight,
          ← enrichedOrdinaryCategorySelf_eHomWhiskerLeft]
-- 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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
⊢ (fun (f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃) ↦
        ({ app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
            naturality := ⋯ } :
          NatTrans F₂ (functorEnrichedHom C F₁ F₃)))
      ((fun (g : F₂ ⟶ functorEnrichedHom C F₁ F₃) ↦
          ({
              app := fun (j : J) ↦
                uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
              naturality := ⋯ } :
            NatTrans (tensorObj (𝒞 := Functor.category) F₁ F₂) F₃))
        g) =
    g
have w : ∀ (j : J),
  NatTrans.app
      ((fun (f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃) ↦
          ({ app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) sorry,
              naturality := sorry } :
            NatTrans F₂ (functorEnrichedHom C F₁ F₃)))
        ((fun (g : F₂ ⟶ functorEnrichedHom C F₁ F₃) ↦
            ({
                app := fun (j : J) ↦
                  uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
                naturality := sorry } :
              NatTrans (tensorObj (𝒞 := Functor.category) F₁ F₂) F₃))
          g))
      j =
    g.app j
Tactic: ext j
-- 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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
⊢ NatTrans.app
      ((fun (f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃) ↦
          ({ app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
              naturality := ⋯ } :
            NatTrans F₂ (functorEnrichedHom C F₁ F₃)))
        ((fun (g : F₂ ⟶ functorEnrichedHom C F₁ F₃) ↦
            ({
                app := fun (j : J) ↦
                  uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
                naturality := ⋯ } :
              NatTrans (tensorObj (𝒞 := Functor.category) F₁ F₂) F₃))
          g))
      j =
    g.app j
have w : end_.lift
    (fun (k : Under.{v₂, u₂} j) ↦
      F₂.map k.hom ≫
        curry
          (uncurry
            (g.app k.right ≫
              enrichedHomπ C (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₃) (Under.mk (𝟙 k.right)))))
    sorry =
  g.app j
Tactic: dsimp