awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
X Y Z : J
f : X ⟶ Y
g : Y ⟶ Z
j : Under.{v₃, u₃} Z
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j.right) (F₂.obj j.right))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ((Under.map (f ≫ g)).obj j) :
      enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget X ⋙ F₁).obj ((Under.map (f ≫ g)).obj j))
          ((Under.forget X ⋙ F₂).obj ((Under.map (f ≫ g)).obj j)))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ((Under.map f).obj ((Under.map g).obj j)))
have h : (Under.map (f ≫ g)).obj j = (Under.map f).obj ((Under.map g).obj j)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ Eq.{v₁ + 1} (α := s.pt ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j')
    ((fun (j : J) ↦
          (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
            s.pt ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j))
        j ≫
      map (obj (diagram V F₁ F₂) (Opposite.op j)) f)
    ((fun (j : J) ↦
          (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
            s.pt ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j))
        j' ≫
      NatTrans.app (map (diagram V F₁ F₂) f.op) j')
have dsimp : Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
  (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
      s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (eHomWhiskerLeft V (F₁.obj j) (F₂.map f) :
      Quiver.Hom.{v₁, u₁} (V := V) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
        (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))))
  (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
    (s.π.app j' ≫ enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) :
      s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
    (eHomWhiskerRight V (F₁.map f) (F₂.obj j') :
      Quiver.Hom.{v₁, u₁} (V := V) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
        (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f) :
        Quiver.Hom.{v₁, u₁} (V := V) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (s.π.app j' ≫ enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) :
        s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (eHomWhiskerRight V (F₁.map f) (F₂.obj j') :
        Quiver.Hom.{v₁, u₁} (V := V) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))))
have rw : Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
  (s.π.app j ≫
    CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
            ((Under.forget j ⋙ F₂).obj (Under.mk (𝟙 j))))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f)))
  (s.π.app j ≫
    map (functorEnrichedHom V F₁ F₂) f ≫
      CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
        (enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) :
          enrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) ⟶
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
              ((Under.forget j' ⋙ F₂).obj (Under.mk (𝟙 j'))))
        (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
Tactic: rw [← s.w f, assoc, assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (s.π.app j ≫
      CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
        (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
          enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
              ((Under.forget j ⋙ F₂).obj (Under.mk (𝟙 j))))
        (eHomWhiskerLeft V (F₁.obj j) (F₂.map f)))
    (s.π.app j ≫
      map (functorEnrichedHom V F₁ F₂) f ≫
        CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
          (enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) :
            enrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                ((Under.forget j' ⋙ F₂).obj (Under.mk (𝟙 j'))))
          (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
have simp : Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
  (s.π.app j ≫
    CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
            ((Under.forget j ⋙ F₂).obj (Under.mk (𝟙 j))))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f)))
  (s.π.app j ≫
    CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map f).obj (Under.mk (𝟙 j'))) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map f).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₂).obj ((Under.map f).obj (Under.mk (𝟙 j')))))
      (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
Tactic: simp only [functorEnrichedHom_obj, functorEnrichedHom_map, end_.lift_π_assoc, diagram_obj_obj,
      Functor.comp_obj, Under.forget_obj, Under.mk_right, Under.map_obj_right, Iso.refl_inv,
      NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom, eHomWhiskerLeft_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (hypothesis)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (s.π.app j ≫
      CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
        (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
          enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
              ((Under.forget j ⋙ F₂).obj (Under.mk (𝟙 j))))
        (eHomWhiskerLeft V (F₁.obj j) (F₂.map f)))
    (s.π.app j ≫
      CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
        (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map f).obj (Under.mk (𝟙 j'))) :
          enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _
              ((Under.forget j ⋙ F₁).obj ((Under.map f).obj (Under.mk (𝟙 j'))))
              ((Under.forget j ⋙ F₂).obj ((Under.map f).obj (Under.mk (𝟙 j')))))
        (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
have this : Eq.{v₁ + 1} (α :=
  enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
      ((Under.forget j ⋙ F₂).obj (Under.mk f)))
  (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) ≫
    eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j))) ((Under.forget j ⋙ F₂).map (Under.homMk f sorry)))
  (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) ≫
    eHomWhiskerRight V ((Under.forget j ⋙ F₁).map (Under.homMk f sorry)) ((Under.forget j ⋙ F₂).obj (Under.mk f)))
Tactic: have := enrichedHom_condition V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)
      (Under.homMk f : Under.mk (𝟙 j) ⟶ Under.mk f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
this :
  Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
            ((Under.forget j ⋙ F₂).obj (Under.mk (𝟙 j))))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f)))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk f))
            ((Under.forget j ⋙ F₂).obj (Under.mk f)))
      (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
⊢ Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (s.π.app j ≫
      CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
        (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) :
          enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk f))
              ((Under.forget j ⋙ F₂).obj (Under.mk f)))
        (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
    (s.π.app j ≫
      CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
        (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map f).obj (Under.mk (𝟙 j'))) :
          enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _
              ((Under.forget j ⋙ F₁).obj ((Under.map f).obj (Under.mk (𝟙 j'))))
              ((Under.forget j ⋙ F₂).obj ((Under.map f).obj (Under.mk (𝟙 j')))))
        (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
have e_a : Under.mk f = (Under.map f).obj (Under.mk (𝟙 j'))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
this :
  Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
            ((Under.forget j ⋙ F₂).obj (Under.mk (𝟙 j))))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f)))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk f))
            ((Under.forget j ⋙ F₂).obj (Under.mk f)))
      (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
⊢ Under.mk f = (Under.map f).obj (Under.mk (𝟙 j'))
have e_a : Under.mk f = { left := Comma.left.{0, v₃, v₃, 0, u₃, u₃} (Under.mk (𝟙 j')), right := j', hom := f }
Tactic: simp [Under.map, Comma.mapLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
⊢ CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
      (NatTrans.app (Cone.π (coneFunctorEnrichedHom V F₁ F₂)) j) =
    s.π.app j
have dsimp : CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
    (precompEnrichedHom V F₁ F₂ (Under.forget j)) =
  s.π.app j
Tactic: dsimp [coneFunctorEnrichedHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
⊢ CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
      (precompEnrichedHom V F₁ F₂ (Under.forget j)) =
    s.π.app j
have h : ∀ (k : Under.{v₃, u₃} j),
  CategoryStruct.comp (Y := end_ (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)))
      (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
        (precompEnrichedHom V F₁ F₂ (Under.forget j)))
      (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (hypothesis)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
⊢ CategoryStruct.comp (Y := end_ (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)))
      (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
        (precompEnrichedHom V F₁ F₂ (Under.forget j)))
      (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
have this : s.π.app j ≫ map (functorEnrichedHom V F₁ F₂) k.hom = s.π.app k.right
Tactic: have := s.w k.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
this :
  Eq (α := s.pt ⟶ enrichedHom V (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₂))
    (s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)))
    (s.π.app k.right)
⊢ CategoryStruct.comp (Y := end_ (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)))
      (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
        (precompEnrichedHom V F₁ F₂ (Under.forget j)))
      (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
have h : s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map k.hom).obj (Under.mk (𝟙 k.right))) =
  s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
Tactic: simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, lift, functorEnrichedHom_obj,
    assoc, end_.lift_π, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
    eHomWhiskerLeft_id, comp_id, ← this, Under.map_obj_right, Under.mk_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
this :
  Eq (α := s.pt ⟶ enrichedHom V (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₂))
    (s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)))
    (s.π.app k.right)
⊢ s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map k.hom).obj (Under.mk (𝟙 k.right))) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
have h : (Under.map k.hom).obj (Under.mk (𝟙 k.right)) = k
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
this :
  Eq (α := s.pt ⟶ enrichedHom V (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₂))
    (s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)))
    (s.π.app k.right)
⊢ (Under.map k.hom).obj (Under.mk (𝟙 k.right)) = k
have h : { left := Comma.left.{0, v₃, v₃, 0, u₃, u₃} (Under.mk (𝟙 k.right)), right := k.right, hom := k.hom :
    Comma.{0, v₃, v₃, 0, u₃, u₃} (fromPUnit j) (𝟭 J) } =
  k
Tactic: simp [Under.map, Comma.mapLeft]