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₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
m : s.pt ⟶ Cone.pt.{v₃, v₁, u₃, u₁} (F := functorEnrichedHom V F₁ F₂) (coneFunctorEnrichedHom V F₁ F₂)
hm : ∀ (j : J), m ≫ NatTrans.app (Cone.π (coneFunctorEnrichedHom V F₁ F₂)) j = s.π.app j
⊢ m = lift s
have h : ∀ (j : J),
  m ≫ end_.π (diagram V F₁ F₂) j =
    CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂)) (lift s) (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
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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
j j' : J
f : j ⟶ j'
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁} (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃)) j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j')
    (map (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃)) f ≫
      enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃))
    (CategoryStruct.comp (Y := obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j)
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
      (map (functorEnrichedHom V F₁ F₃) f))
have dsimp : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
      (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ⟶
    enrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃))
  (CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂))
      (enrichedHom V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)))
    (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
        (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)))
    (enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)))
  (CategoryStruct.comp (Y := enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
    (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
    (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
      (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))))
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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V)
      (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂)
        (tensorObj (𝒞 := category) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)))
      (functorEnrichedHom V F₁ F₄))
    (Iso.inv (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)) ≫
      CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₃) (functorEnrichedHom V F₃ F₄))
        (functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄) (functorEnrichedComp V F₁ F₃ F₄))
    (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₄))
      (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄) (functorEnrichedComp V F₁ F₂ F₄))
have w : ∀ (j : J),
  Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁}
        (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂)
          (tensorObj (𝒞 := category) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)))
        j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₄) j)
    (NatTrans.app
      (Iso.inv (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)) ≫
        CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₃) (functorEnrichedHom V F₃ F₄))
          (functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄) (functorEnrichedComp V F₁ F₃ F₄))
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₄))
        (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄) (functorEnrichedComp V F₁ 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
j : J
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁}
        (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂)
          (tensorObj (𝒞 := category) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)))
        j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₄) j)
    (NatTrans.app
      (Iso.inv (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)) ≫
        CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₃) (functorEnrichedHom V F₃ F₄))
          (functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄) (functorEnrichedComp V F₁ F₃ F₄))
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₄))
        (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄) (functorEnrichedComp V F₁ F₂ F₄))
      j)
have w : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
      (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
        (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))) ⟶
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₄))
  (Iso.inv
      (α_ (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
        (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
        (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))) ≫
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
        (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄)))
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ▷
        enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄)))
  (CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
      (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)))
    (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
      enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
    (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)))
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₃ : 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₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
      (functorEnrichedHom V F₁ F₃))
    ((functorHomEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₃) (f ≫ g) :
      Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
        (functorEnrichedHom V F₁ F₃))
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := category) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
          ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)))
        (Iso.inv (λ_ ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))))
        (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃))
          ((functorHomEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂) f ⊗ₘ
            (functorHomEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₂ F₃) g)
          (functorEnrichedComp V F₁ F₂ F₃)) :
      Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
        (functorEnrichedHom V F₁ F₃))
have w : ∀ (j : J),
  Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁} ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)) j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j)
    (NatTrans.app ((functorHomEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₃) (f ≫ g)) j)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := category) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
          ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)))
        (Iso.inv (λ_ ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))))
        (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃))
          ((functorHomEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂) f ⊗ₘ
            (functorHomEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₂ F₃) g)
          (functorEnrichedComp V F₁ 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₃ : 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₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁} ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)) j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j)
    (NatTrans.app ((functorHomEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₃) (f ≫ g)) j)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := category) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
          ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)))
        (Iso.inv (λ_ ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))))
        (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃))
          ((functorHomEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂) f ⊗ₘ
            (functorHomEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₂ F₃) g)
          (functorEnrichedComp V F₁ F₂ F₃)))
      j)
have w : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
  (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
      ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g))
      (precompEnrichedHom V F₁ F₃ (Under.forget j)) :
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ 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 (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)))
        (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
            ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f)
            (precompEnrichedHom V F₁ F₂ (Under.forget j)) ⊗ₘ
          CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
            ((homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g) (precompEnrichedHom V F₂ F₃ (Under.forget j)))
        (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))) :
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    ((eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom) ≫
      eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
have rw : Eq.{v' + 1} (α :=
  Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
  ((eHomWhiskerLeft V X β.hom ≫ eHomWhiskerRight V α.inv Y₁) ≫ eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv)
  (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
Tactic: rw [← eHom_whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerRight V α.inv Y₁ ≫ eHomWhiskerRight V α.hom Y₁
have a : eHomWhiskerRight V (α.hom ≫ α.inv) Y₁
Tactic: rw [← eHomWhiskerRight_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    ((eHomWhiskerLeft V X β.hom ≫ eHomWhiskerRight V α.inv Y₁) ≫
      eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
have slice_lhs : Eq.{v' + 1} (α :=
  Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
  (eHomWhiskerLeft V X β.hom ≫ eHomWhiskerRight V (α.hom ≫ α.inv) Y₁ ≫ eHomWhiskerLeft V X β.inv)
  (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
Tactic: slice_lhs 2 3 => rw [← eHomWhiskerRight_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
    ((eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv) ≫
      eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
have rw : Eq.{v' + 1} (α :=
  Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
  ((eHomWhiskerLeft V X₁ β.inv ≫ eHomWhiskerRight V α.hom Y) ≫ eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom)
  (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
Tactic: rw [← eHom_whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerRight V α.hom Y ≫ eHomWhiskerRight V α.inv Y
have a : eHomWhiskerRight V (α.inv ≫ α.hom) Y
Tactic: rw [← eHomWhiskerRight_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
    ((eHomWhiskerLeft V X₁ β.inv ≫ eHomWhiskerRight V α.hom Y) ≫
      eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
have slice_lhs : Eq.{v' + 1} (α :=
  Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
  (eHomWhiskerLeft V X₁ β.inv ≫ eHomWhiskerRight V (α.inv ≫ α.hom) Y ≫ eHomWhiskerLeft V X₁ β.hom)
  (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))
Tactic: slice_lhs 2 3 => rw [← eHomWhiskerRight_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ Eq.{v' + 1} (α :=
    Iso.{v', u'} (C := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₃ Y₃))
    (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)) (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂)
have w : Eq.{v' + 1} (α :=
  Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₃ Y₃))
  (hom (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂))) (hom (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.HomCongr (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
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v' + 1} (α := tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)
    ((eHomEquiv V : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) ≫ hom (eHomCongr V α γ) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst)) (tensorUnit.{v', u'} V (𝒞 := inst)))
        (inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f ≫ hom (eHomCongr V α β)) ▷
            tensorUnit.{v', u'} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁ ◁
              ((eHomEquiv V : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ≫ hom (eHomCongr V β γ)) ≫
            eComp V X₁ Y₁ Z₁)) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)
have simp : Eq.{v' + 1} (α := tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)
  ((eHomEquiv V : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom :
    tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)
  (inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst))) ≫
      hom (ρ_ (tensorUnit.{v', u'} V (𝒞 := inst))) ≫
        CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          ((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f)
          (eHomWhiskerRight V α.inv Y ≫
            eHomWhiskerLeft V X₁ β.hom ≫
              CategoryStruct.comp (Y :=
                tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
                  (tensorUnit.{v', u'} V (𝒞 := inst)))
                (inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)))
                (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁ ◁
                    (eHomEquiv V : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ≫
                  @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁ ◁ eHomWhiskerRight V β.inv Z ≫
                    @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁ ◁ eHomWhiskerLeft V Y₁ γ.hom ≫
                      eComp V X₁ Y₁ Z₁)) :
    tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)
Tactic: simp only [eHomCongr, MonoidalCategory.whiskerRight_id, assoc,
    MonoidalCategory.whiskerLeft_comp]