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 : 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₃
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    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 i)) j)
    ((fun (j : J) ↦
          ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
              eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) :
            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))
        i ≫
      map (obj (diagram V F₁ F₃) (Opposite.op i)) f)
    ((fun (j : J) ↦
          ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
              eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) :
            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))
        j ≫
      NatTrans.app (map (diagram V F₁ F₃) f.op) j)
have dsimp : Eq.{v₁ + 1} (α :=
  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 i) (F₃.obj j))
  (((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
    eHomWhiskerLeft V (F₁.obj i) (F₃.map f))
  (((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
    eHomWhiskerRight V (F₁.map f) (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 : 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₃
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    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 i) (F₃.obj j))
    (((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
      eHomWhiskerLeft V (F₁.obj i) (F₃.map f))
    (((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      eHomWhiskerRight V (F₁.map f) (F₃.obj j))
have trans : Eq.{v₁ + 1} (α :=
  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 i) (F₃.obj j))
  (((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
    eHomWhiskerLeft V (F₁.obj i) (F₃.map f))
  ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
    Iso.inv (ρ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) i)) ▷
        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 i)) i ◁
            (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ▷
          obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (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 i))) (F₂.obj j) (F₃.obj j))
Tactic: trans (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ _).inv ▷ _ ≫ (_ ◁ (eHomEquiv V (F₂.map f))) ▷ _ ≫ eComp V _ (F₂.obj i) _ ▷ _ ≫
        eComp V _ (F₂.obj j) _
-- 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 : 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₃
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    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 i) (F₃.obj j))
    (((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
      eHomWhiskerLeft V (F₁.obj i) (F₃.map f))
    ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      Iso.inv (ρ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) i)) ▷
          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 i)) i ◁
              (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ▷
            obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (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 i))) (F₂.obj j) (F₃.obj j))
have this : Eq.{v₁ + 1} (α :=
  end_.{v₃, v₁, u₃, u₁} (diagram V F₂ F₃) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op i)) j)
  (end_.π (diagram V F₂ F₃) i ≫ map (obj (diagram V F₂ F₃) (Opposite.op i)) f)
  (end_.π (diagram V F₂ F₃) j ≫ NatTrans.app (map (diagram V F₂ F₃) f.op) j)
Tactic: have := end_.condition (diagram V F₂ F₃) f
-- 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 : 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₃
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    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 i) (F₃.obj j))
    ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      Iso.inv (ρ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) i)) ▷
          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 i)) i ◁
              (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ▷
            obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (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 i))) (F₂.obj j) (F₃.obj j))
    (((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      eHomWhiskerRight V (F₁.map f) (F₃.obj j))
have this : Eq.{v₁ + 1} (α :=
  end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) j)
  (end_.π (diagram V F₁ F₂) i ≫ map (obj (diagram V F₁ F₂) (Opposite.op i)) f)
  (end_.π (diagram V F₁ F₂) j ≫ NatTrans.app (map (diagram V F₁ F₂) f.op) j)
Tactic: have := end_.condition (diagram V F₁ F₂) 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
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
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₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
    ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
        (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₃))
          ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f ⊗ₘ
            (homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
          (enrichedComp V F₁ F₂ F₃)) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
have h : ∀ (j : J),
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ 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₃))
        ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g)) (end_.π (diagram V F₁ F₃) j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ 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₃))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
          (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
          (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₃))
            ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f ⊗ₘ
              (homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
            (enrichedComp V F₁ F₂ F₃)))
        (end_.π (diagram V F₁ F₃) j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) 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₂ : 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₂
⊢ Iso.inv (λ_ (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₂))
        (enrichedId V 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₂)
have h : ∀ (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₂)) ≫
        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₂))
          (enrichedId V F₁ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedComp V F₁ F₁ F₂))
      (end_.π (diagram V F₁ F₂) j) =
    𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V 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₂ : 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
⊢ CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂))
      (Iso.inv (λ_ (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₂))
          (enrichedId V F₁ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedComp V F₁ F₁ F₂))
      (end_.π (diagram V F₁ F₂) j) =
    𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
have h : Eq (α := 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 ≫
    Iso.inv (λ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)) ≫
      eId V (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)
Tactic: rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def, assoc,
    ← comp_whiskerRight_assoc, enrichedId_π, ← whisker_exchange_assoc,
    id_whiskerLeft, assoc, assoc, Iso.inv_hom_id_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₂ : 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 (α :=
    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 ≫
      Iso.inv (λ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)) ≫
        eId V (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)
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 ≫
    Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))) ≫
      eId V (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)
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₂ : 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))) ≫
        eId V (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)
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_id_comp, 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))) ≫
        eId V (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)
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_id_comp, 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₂
⊢ Iso.inv (ρ_ (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₂))
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedId V F₂) (enrichedComp V F₁ F₂ F₂) =
    𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
have h : ∀ (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₂)) ≫
        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₂ ◁ enrichedId V F₂) (enrichedComp V F₁ F₂ F₂))
      (end_.π (diagram V F₁ F₂) j) =
    𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V 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₂ : 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
⊢ CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂))
      (Iso.inv (ρ_ (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₂))
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedId V F₂) (enrichedComp V F₁ F₂ F₂))
      (end_.π (diagram V F₁ F₂) j) =
    𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
have h : Eq (α := 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 ≫
    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 ◁ eId V (F₂.obj j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j))
  (end_.π (diagram V F₁ F₂) j)
Tactic: rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def', assoc,
    ← MonoidalCategory.whiskerLeft_comp_assoc, enrichedId_π,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id, assoc, assoc,
    Iso.inv_hom_id_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₂ : 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 (α :=
    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 ≫
      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 ◁ eId V (F₂.obj j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op 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 ≫
    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)
Tactic: dsimp