awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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 Y₁ Z : C
α : Y ≅ Y₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    ((eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
      eComp V X Y Z)
    (eComp V X Y Z)

Tactic:
simp [← eHomWhiskerLeft_comp]

Premises used: CategoryTheory.eHomWhiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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 Y₁ Z : C
α : Y ≅ Y₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y₁ Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eHomWhiskerLeft V X α.inv ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y₁ Z ≫
      @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁ eHomWhiskerRight V α.hom Z ≫ eComp V X Y Z)
    (eComp V X Y₁ Z)

Tactic:
eHom_whisker_cancel V α.symm

Premises used: CategoryTheory.eHom_whisker_cancel, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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 X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
dsimp :
  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'))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y')
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (Iso.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 ⟶ Y') → 𝟙_ V ⟶ Y ⟶[V] Y') g ≫
            eComp V X' Y Y'))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y'))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y')))
          ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
              @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y' ≫
            eComp V X X' Y')) :
      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'))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)))
          ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
              @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y ≫
            eComp V X X' Y))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (Iso.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 ⟶ Y') → 𝟙_ V ⟶ Y ⟶[V] Y') g ≫
            eComp V X Y Y')) :
      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'))
⊢ 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' g ≫ eHomWhiskerRight V f Y') (eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g)

Tactic:
dsimp [eHomWhiskerLeft, eHomWhiskerRight]

Premises used: CategoryTheory.eHomWhiskerLeft, CategoryTheory.eHomWhiskerRight
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
D : Type u''
inst_4 : Category.{v'', u''} D
inst_5 : EnrichedOrdinaryCategory.{v', v'', u'', u'} V D
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v' + 1} (α := Quiver.Hom (V := ForgetEnrichment.{v', u', u''} V D) (of V X) (of V Z))
    (homOf V ((eHomEquiv V : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g)))
    (CategoryStruct.comp (Y := of V Y) (homOf V ((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f))
      (homOf V ((eHomEquiv V : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g)))

Tactic:
simp [eHomEquiv_comp]

Premises used: CategoryTheory.eHomEquiv_comp
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
D : Type u''
inst_4 : Category.{v'', u''} D
inst_5 : EnrichedOrdinaryCategory.{v', v'', u'', u'} V D
X : ForgetEnrichment.{v', u', u''} V D
rw :
  Eq.{v'' + 1} (α := «to» V X ⟶ «to» V X)
    ((Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ «to» V X ⟶[V] «to» V X) → «to» V X ⟶ «to» V X) (eId V («to» V X)) :
      «to» V X ⟶ «to» V X)
    (𝟙 («to» V X) : «to» V X ⟶ «to» V X)
rw₁ :
  Eq.{v'' + 1} (α := «to» V X ⟶ «to» V X)
    ((Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ «to» V X ⟶[V] «to» V X) → «to» V X ⟶ «to» V X)
        ((eHomEquiv V : (a : «to» V X ⟶ «to» V X) → 𝟙_ V ⟶ «to» V X ⟶[V] «to» V X) (𝟙 («to» V X))) :
      «to» V X ⟶ «to» V X)
    (𝟙 («to» V X) : «to» V X ⟶ «to» V X)
rw₂ rw₃ : Eq.{v'' + 1} (α := «to» V X ⟶ «to» V X) (𝟙 («to» V X)) (𝟙 («to» V X))
⊢ Eq.{v'' + 1} (α := «to» V X ⟶ «to» V X)
    ((Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ «to» V X ⟶[V] «to» V X) → «to» V X ⟶ «to» V X) (homTo V (𝟙 X)) :
      «to» V X ⟶ «to» V X)
    (𝟙 («to» V X) : «to» V X ⟶ «to» V X)

Tactic:
rw [ForgetEnrichment.homTo_id, ← eHomEquiv_id, Equiv.symm_apply_apply]

Premises used: CategoryTheory.eHomEquiv_id, Equiv.symm_apply_apply, CategoryTheory.ForgetEnrichment.homTo_id
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
D : Type u''
inst_4 : Category.{v'', u''} D
inst_5 : EnrichedOrdinaryCategory.{v', v'', u'', u'} V D
X Y Z : ForgetEnrichment.{v', u', u''} V D
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u''} _ inst inst_1 _ _ («to» V X) («to» V Z))
    ((eHomEquiv V : (a : «to» V X ⟶ «to» V Z) → 𝟙_ V ⟶ «to» V X ⟶[V] «to» V Z)
        ((Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ «to» V X ⟶[V] «to» V Z) → «to» V X ⟶ «to» V Z) (homTo V (f ≫ g))) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u''} _ inst inst_1 _ _ («to» V X) («to» V Z))
    ((eHomEquiv V : (a : «to» V X ⟶ «to» V Z) → 𝟙_ V ⟶ «to» V X ⟶[V] «to» V Z)
        (CategoryStruct.comp (Y := «to» V Y)
          ((Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ «to» V X ⟶[V] «to» V Y) → «to» V X ⟶ «to» V Y) (homTo V f))
          ((Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ «to» V Y ⟶[V] «to» V Z) → «to» V Y ⟶ «to» V Z) (homTo V g))) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u''} _ inst inst_1 _ _ («to» V X) («to» V Z))

Tactic:
simp [eHomEquiv_comp]

Premises used: CategoryTheory.eHomEquiv_comp
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
D : Type u''
inst_4 : Category.{v'', u''} D
inst_5 : EnrichedOrdinaryCategory.{v', v'', u'', u'} V D
X : ForgetEnrichment.{v', u', u''} V D
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u''} _ inst inst_1 _ _ («to» V X) («to» V X))
    ((eHomEquiv V : (a : «to» V X ⟶ «to» V X) → 𝟙_ V ⟶ «to» V X ⟶[V] «to» V X)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v', v'', u'', u''} (C := ForgetEnrichment.{v', u', u''} V D) (equivFunctor V D)
            (Functor.obj (equivInverse V D) (Functor.obj (equivFunctor V D) X)))
          (Functor.map (equivFunctor V D)
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (X : ForgetEnrichment.{v', u', u''} V D) ↦
                    Iso.refl (Functor.obj.{v', v', u'', u''} (𝟭 (ForgetEnrichment.{v', u', u''} V D)) X))
                  ⋯))
              X))
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : D) ↦
                  Iso.refl
                    (Functor.obj.{v'', v'', u'', u''}
                      (Functor.comp.{v'', v', v'', u'', u'', u''} (D := ForgetEnrichment.{v', u', u''} V D)
                        (equivInverse V D) (equivFunctor V D))
                      X))
                ⋯))
            (Functor.obj (equivFunctor V D) X))) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u''} _ inst inst_1 _ _ («to» V X) («to» V X))
    ((eHomEquiv V : (a : «to» V X ⟶ «to» V X) → 𝟙_ V ⟶ «to» V X ⟶[V] «to» V X) (𝟙 (Functor.obj (equivFunctor V D) X)) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u''} _ inst inst_1 _ _ («to» V X) («to» V X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
W : Type u''
inst_4 : Category.{v'', u''} W
inst_5 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_6 : F.LaxMonoidal
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
X : TransportEnrichment F C
⊢ Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X X)
    ((Equiv.trans (eHomEquiv V) (e (@Hom.{v', u', u} _ inst inst_1 _ _ X X)) : (a : X ⟶ X) → 𝟙_ W ⟶ X ⟶[W] X) (𝟙 X) :
      tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X X)
    (eId W X : tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X X)

Tactic:
simpa using h _ (eId V _)

Premises used: CategoryTheory.eId
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)
rw :
  Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W X))
    (ForgetEnrichment.homOf W (eId W (ForgetEnrichment.to V X))) (𝟙 (ForgetEnrichment.of W X))
⊢ Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W X))
    (ForgetEnrichment.homOf W
      ((e (@Hom.{v', u', u} _ inst inst_1 _ _ X X) : (a : 𝟙_ V ⟶ X ⟶[V] X) → 𝟙_ W ⟶ F.obj (X ⟶[V] X))
        (ForgetEnrichment.homTo V (𝟙 X))))
    (𝟙 (ForgetEnrichment.of W X))

Tactic:
rw [h, ForgetEnrichment.homTo_id, ← TransportEnrichment.eId_eq]

Premises used: CategoryTheory.TransportEnrichment.eId_eq, CategoryTheory.ForgetEnrichment.homTo_id
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)
⊢ Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W X))
    (ForgetEnrichment.homOf W (eId W (ForgetEnrichment.to V X))) (𝟙 (ForgetEnrichment.of W X))

Tactic:
simp [ForgetEnrichment.to]

Premises used: CategoryTheory.ForgetEnrichment.to
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X Y Z : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W Z))
    (ForgetEnrichment.homOf W
      (CategoryStruct.comp (Y :=
        tensorObj.{v'', u''} (𝒞 := inst_7) (tensorUnit.{v'', u''} W (𝒞 := inst_7))
          (tensorUnit.{v'', u''} W (𝒞 := inst_7)))
        (Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_7))))
        ((Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W (ForgetEnrichment.to V X) (ForgetEnrichment.to V Y) (ForgetEnrichment.to V Z))))
    (ForgetEnrichment.homOf W
      (CategoryStruct.comp (Y :=
        tensorObj.{v'', u''} (𝒞 := inst_7) (tensorUnit.{v'', u''} W (𝒞 := inst_7))
          (tensorUnit.{v'', u''} W (𝒞 := inst_7)))
        (Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_7))))
        ((Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X Y Z)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)
rw :
  Eq.{v' + 1} (α :=
    Quiver.Hom (V := TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))
      (ForgetEnrichment.of V (ForgetEnrichment.to W X) : ForgetEnrichment.{v', u', u} V D)
      (ForgetEnrichment.of V (ForgetEnrichment.to W X)))
    (ForgetEnrichment.homOf V
      ((Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))) :
          (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) →
            𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)
        (ForgetEnrichment.homTo W (𝟙 X))))
    (ForgetEnrichment.homOf V (eId V (ForgetEnrichment.to W X)))
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))
      (ForgetEnrichment.of V (ForgetEnrichment.to W X) : ForgetEnrichment.{v', u', u} V D)
      (ForgetEnrichment.of V (ForgetEnrichment.to W X)))
    (ForgetEnrichment.homOf V
      ((Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))) :
          (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) →
            𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)
        (ForgetEnrichment.homTo W (𝟙 X))))
    (𝟙 (ForgetEnrichment.of V (ForgetEnrichment.to W X)))

Tactic:
rw [← ForgetEnrichment.homOf_eId]

Premises used: CategoryTheory.ForgetEnrichment.homOf_eId
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
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
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)
e_f :
  Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst) ⟶
      @Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))
    ((Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))) :
          (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) →
            𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)
        (ForgetEnrichment.homTo W (𝟙 X)) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶
        @Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))
    (eId V (ForgetEnrichment.to W X) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶
        @Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))
      (ForgetEnrichment.of V (ForgetEnrichment.to W X) : ForgetEnrichment.{v', u', u} V D)
      (ForgetEnrichment.of V (ForgetEnrichment.to W X)))
    (ForgetEnrichment.homOf V
      ((Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))) :
          (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) →
            𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)
        (ForgetEnrichment.homTo W (𝟙 X))))
    (ForgetEnrichment.homOf V (eId V (ForgetEnrichment.to W X)))

Tactic:
congr 1