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
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₂
j : J
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫
      Iso.inv (ρ_ (@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) ◁ eId V (F₂.obj j) ≫
          eComp V (F₁.obj j) (F₂.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j)
have h : Eq.{v₁ + 1} (α :=
  enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
  (end_.π (diagram V F₁ F₂) j ≫ 𝟙 (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
  (end_.π (diagram V F₁ F₂) j)
Tactic: rw [e_comp_id, comp_id]
-- 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 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₂
j : J
h :
  Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫ 𝟙 (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
    (end_.π (diagram V F₁ F₂) j)
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫
      Iso.inv (ρ_ (@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) ◁ eId V (F₂.obj j) ≫
          eComp V (F₁.obj j) (F₂.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j)
have h₁ : Eq.{v₁ + 1} (α :=
  enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
  (end_.π (diagram V F₁ F₂) j) (end_.π (diagram V F₁ F₂) j)
Tactic: rw [e_comp_id, comp_id]
-- 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₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
      enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄)
    (Iso.inv
        (α_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄))
        (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄) (enrichedComp V F₁ F₃ F₄))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄))
      (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ F₂ F₄))
have h : ∀ (j : J),
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
      obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₄) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
      (Iso.inv
          (α_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
            (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
            (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄))
          (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄) (enrichedComp V F₁ F₃ F₄))
      (end_.π (diagram V F₁ F₄) j))
    (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄))
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ F₂ F₄))
      (end_.π (diagram V F₁ F₄) j))
Tactic: ext j
-- 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₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
| CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
    (Iso.inv
        (α_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄))
        (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄) (enrichedComp V F₁ F₃ F₄))
    (end_.π (diagram V F₁ F₄) j)
have rw : (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
  Iso.inv
      (α_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)
        (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j)
        (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₃ F₄) (Opposite.op j)) j)) ≫
    eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
        obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₃ F₄) (Opposite.op j)) j ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)
Tactic: rw [assoc, assoc, enrichedComp_π,
      tensorHom_def_assoc, ← comp_whiskerRight_assoc, enrichedComp_π,
      comp_whiskerRight_assoc, ← whisker_exchange_assoc,
      ← whisker_exchange_assoc, ← tensorHom_def'_assoc, ← associator_inv_naturality_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
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
| CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄))
      (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ F₂ F₄))
    (end_.π (diagram V F₁ F₄) j)
have rw : (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
  obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j ◁
      eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
    eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)
Tactic: rw [assoc, enrichedComp_π, tensorHom_def'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
      enrichedComp_π, MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange_assoc,
      whisker_exchange_assoc, ← tensorHom_def_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
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
      obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₄) (Opposite.op j)) j)
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      Iso.inv
          (α_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)
            (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j)
            (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₃ F₄) (Opposite.op j)) j)) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
            obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₃ F₄) (Opposite.op j)) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j ◁
          eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j))
have h : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₄.obj j))
  ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    Iso.inv
        (α_ (@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))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j))) ≫
      eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ▷
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j) ≫
        eComp V (F₁.obj j) (F₃.obj j) (F₄.obj j))
  ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
        eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
      eComp V (F₁.obj j) (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
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      Iso.inv
          (α_ (@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))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j))) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ▷
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j) ≫
          eComp V (F₁.obj j) (F₃.obj j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
          eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j))
have h : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₄.obj j))
  ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
        eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
      eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j))
  ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
        eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
      eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j))
Tactic: rw [e_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₂
X : J
⊢ precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
      (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂))
have h : ∀ (j : Under.{v₃, u₃} X),
  CategoryStruct.comp (Y := end_ (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)))
      (precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)))
      (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) ≫
      end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j
Tactic: ext j
-- 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 : J
j : Under.{v₃, u₃} X
⊢ CategoryStruct.comp (Y := end_ (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)))
      (precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)))
      (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) ≫
      end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j
have h : 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₂) (obj (Under.map (𝟙 X)) j))
  (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j)
Tactic: simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π,
      Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
      eHomWhiskerLeft_id, comp_id, id_comp]
-- 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 : J
j : Under.{v₃, u₃} X
⊢ 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₂) (obj (Under.map (𝟙 X)) j))
    (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j)
have h : obj (Under.map (𝟙 X)) j = 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₂
X : J
j : Under.{v₃, u₃} X
⊢ obj (Under.map (𝟙 X)) j = j
have h : { left := j.left, right := j.right, hom := j.hom : Comma.{0, v₃, v₃, 0, u₃, u₃} (fromPUnit X) (𝟭 J) } = j
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
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
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      enrichedHom V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂))
    (precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₁))
      (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₂)))
    (CategoryStruct.comp (Y := enrichedHom V (Under.forget Y ⋙ F₁) (Under.forget Y ⋙ F₂))
      (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₂)))
      (precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₁))
        (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₂))))
have h : ∀ (j : Under.{v₃, u₃} Z),
  Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      obj (obj (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
      (precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₂)))
      (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
      (CategoryStruct.comp (Y := enrichedHom V (Under.forget Y ⋙ F₁) (Under.forget Y ⋙ F₂))
        (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₂)))
        (precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₁))
          (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₂))))
      (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))
Tactic: ext j
-- 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₂) ⟶
      obj (obj (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
      (precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₂)))
      (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
      (CategoryStruct.comp (Y := enrichedHom V (Under.forget Y ⋙ F₁) (Under.forget Y ⋙ F₂))
        (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₂)))
        (precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₁))
          (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₂))))
      (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))
have h : 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)))
Tactic: simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π,
      Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
      eHomWhiskerLeft_id, comp_id, assoc]