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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
⊢ 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)))))
      ⋯ =
    g.app j
have w : ∀ (k : Under.{v₂, u₂} j),
  CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)))
      (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)
      (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k) =
    g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
Tactic: ext k
-- 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
k : Under.{v₂, u₂} j
⊢ CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)))
      (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)))))
        ⋯)
      (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k) =
    g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
have w : g.app j ≫
    enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)
      { left := Comma.left.{0, v₂, v₂, 0, u₂, u₂} (Under.mk (𝟙 k.right)), right := k.right, hom := k.hom ≫ 𝟙 k.right } =
  g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
Tactic: simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, enrichedCategorySelf_hom,
      curry_uncurry, NatTrans.naturality_assoc, functorEnrichedHom_obj, functorEnrichedHom_map,
      Under.map, Comma.mapLeft, Functor.const_obj_obj, Functor.id_obj, Discrete.natTrans_app,
      StructuredArrow.left_eq_id, end_.lift_π, Under.mk_right, Under.mk_hom, Iso.refl_inv,
      NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerRight, pre_id, Iso.refl_hom,
      enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Functor.map_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
k : Under.{v₂, u₂} j
⊢ g.app j ≫
      enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)
        { left := Comma.left.{0, v₂, v₂, 0, u₂, u₂} (Under.mk (𝟙 k.right)), right := k.right,
          hom := k.hom ≫ 𝟙 k.right } =
    g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
have w : k.hom ≫ 𝟙 k.right = k.hom
Tactic: congr
-- 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₃ : Functor.{v₂, v₁, u₂, u₁} J C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ Eq (α := tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
    ((Equiv.symm homEquiv : (a : F₂ ⟶ functorEnrichedHom C F₁ F₃) → F₁ ⊗ F₂ ⟶ F₃) (f₂ ≫ g) :
      tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
    (F₁ ◁ f₂ ≫ (Equiv.symm homEquiv : (a : F₂' ⟶ functorEnrichedHom C F₁ F₃) → F₁ ⊗ F₂' ⟶ F₃) g :
      tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
have dsimp : Eq (α := tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
  {
    app := fun (j : J) ↦
      uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
    naturality := sorry }
  (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 })
Tactic: dsimp [homEquiv]
-- 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₃ : Functor.{v₂, v₁, u₂, u₁} J C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ Eq (α := tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
    {
      app := fun (j : J) ↦
        uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
      naturality := ⋯ }
    (F₁ ◁ f₂ ≫
      {
        app := fun (j : J) ↦
          uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := ⋯ })
have w : ∀ (j : J),
  Eq (α := (tensorObj (𝒞 := Functor.category) F₁ F₂).obj j ⟶ F₃.obj j)
    (NatTrans.app
      {
        app := fun (j : J) ↦
          uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := sorry }
      j)
    (NatTrans.app
      (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 })
      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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
⊢ Eq (α := F₂ ⟶ functorEnrichedHom C F₁ F₃')
    ((homEquiv : (a : F₁ ⊗ F₂ ⟶ F₃') → F₂ ⟶ functorEnrichedHom C F₁ F₃') (f ≫ f₃) : F₂ ⟶ functorEnrichedHom C F₁ F₃')
    (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
        ((homEquiv : (a : F₁ ⊗ F₂ ⟶ F₃) → F₂ ⟶ functorEnrichedHom C F₁ F₃) f)
        (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
          CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
            (functorEnrichedHom C F₁ F₃ ◁
              (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
            (functorEnrichedComp C F₁ F₃ F₃')) :
      F₂ ⟶ functorEnrichedHom C F₁ F₃')
have dsimp : Eq (α := F₂ ⟶ functorEnrichedHom C F₁ F₃')
  {
    app := fun (j : J) ↦
      end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) sorry,
    naturality := sorry }
  (CategoryStruct.comp (Y := functorEnrichedHom C 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 }
    (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
        (functorEnrichedHom C F₁ F₃ ◁
          (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
        (functorEnrichedComp C F₁ F₃ F₃')))
Tactic: dsimp [homEquiv]
-- 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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
⊢ Eq (α := F₂ ⟶ functorEnrichedHom C F₁ F₃')
    {
      app := fun (j : J) ↦
        end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯,
      naturality := ⋯ }
    (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
      { app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
        naturality := ⋯ }
      (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
          (functorEnrichedHom C F₁ F₃ ◁
            (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
          (functorEnrichedComp C F₁ F₃ F₃')))
have w : ∀ (j : J),
  Eq (α := F₂.obj j ⟶ Functor.obj (functorEnrichedHom C F₁ F₃') j)
    (NatTrans.app
      {
        app := fun (j : J) ↦
          end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) sorry,
        naturality := sorry }
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y := functorEnrichedHom C 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 }
        (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
          CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
            (functorEnrichedHom C F₁ F₃ ◁
              (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
            (functorEnrichedComp C F₁ F₃ F₃')))
      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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
⊢ Eq (α := F₂.obj j ⟶ Functor.obj (functorEnrichedHom C F₁ F₃') j)
    (NatTrans.app
      {
        app := fun (j : J) ↦
          end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯,
        naturality := ⋯ }
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
        { app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
          naturality := ⋯ }
        (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
          CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
            (functorEnrichedHom C F₁ F₃ ◁
              (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
            (functorEnrichedComp C F₁ F₃ F₃')))
      j)
have w : Eq (α := F₂.obj j ⟶ enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃'))
  (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) sorry)
  (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) sorry ≫
    Iso.inv (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
          (enrichedHom C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
        (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
          CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
            ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
            (precompEnrichedHom C F₃ F₃' (Under.forget j)))
        (enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
⊢ Eq (α := F₂.obj j ⟶ enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃'))
    (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯)
    (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      Iso.inv (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
            (enrichedHom C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
          (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
            CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
              ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
              (precompEnrichedHom C F₃ F₃' (Under.forget j)))
          (enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
have w : ∀ (k : Under.{v₂, u₂} j),
  Eq (α :=
    F₂.obj j ⟶ Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) (Opposite.op k)) k)
    (CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')))
      (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) sorry)
      (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k))
    (CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')))
      (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) sorry ≫
        Iso.inv (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
              (enrichedHom C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
            (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (precompEnrichedHom C F₃ F₃' (Under.forget j)))
            (enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
      (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k))
Tactic: ext k
-- 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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        Iso.inv
            (ρ_ (Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)) ≫
          Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (enrichedHomπ C F₃ F₃' (Functor.obj (Under.forget j) k) ≫
                  NatTrans.app (pre (NatTrans.app (Iso.inv (Iso.refl (Under.forget j ⋙ F₃))) k))
                      (F₃'.obj (Functor.obj (Under.forget j) k)) ≫
                    Functor.map (ihom ((Under.forget j ⋙ F₃).obj k))
                      (NatTrans.app (Iso.hom (Iso.refl (Under.forget j ⋙ F₃'))) k)) ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)
have w : 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 ≫ f₃.app k.right))
  (F₂.map k.hom ≫
    curry (f.app k.right) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
          (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
          (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
            CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
              ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
              (enrichedHomπ C F₃ F₃' k.right ≫
                NatTrans.app (pre (𝟙 (F₃.obj k.right))) (F₃'.obj k.right) ≫
                  Functor.map (ihom (F₃.obj k.right)) (𝟙 (F₃'.obj k.right))))
          (eComp C (F₁.obj k.right) (F₃.obj k.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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
⊢ 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 ≫ f₃.app k.right))
    (F₂.map k.hom ≫
      curry (f.app k.right) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
              (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (enrichedHomπ C F₃ F₃' k.right ≫
                  NatTrans.app (pre (𝟙 (F₃.obj k.right))) (F₃'.obj k.right) ≫
                    Functor.map (ihom (F₃.obj k.right)) (𝟙 (F₃'.obj k.right))))
            (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))))
have w : 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₃.app k.right))
  (F₂.map k.hom ≫
    curry (f.app k.right) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
          (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
          (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
            (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
              (f₃.app k.right))
          (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))))
Tactic: rw [pre_id, NatTrans.id_app, Functor.map_id, Category.comp_id,
    Category.comp_id, homEquiv_apply_π, curry_natural_right]
-- 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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
⊢ 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₃.app k.right))
    (F₂.map k.hom ≫
      curry (f.app k.right) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
              (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
              (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
                (f₃.app k.right))
            (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))))
have w : Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right) =
  CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
        (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
      (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
        (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
          (f₃.app k.right))
      (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)))
Tactic: congr 2