awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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 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))
    (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₁) α.hom ≫
                eComp V X Y 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) α.inv ≫
                eComp V X Y₁ Y)) ▷
          @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
        eComp V X Y Z :
      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))
    (eComp V X Y Z :
      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))
have change : 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: change (eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ _ ≫ _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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 X' Y Y' : C
f : X ⟶ X'
g : 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' g ≫ eHomWhiskerRight V f Y') (eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g)
have 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'))
Tactic: dsimp [eHomWhiskerLeft, eHomWhiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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} (α := «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)
have 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)
Tactic: rw [ForgetEnrichment.homTo_id, ← eHomEquiv_id, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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)
⊢ 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)
have 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)
Tactic: rw [ForgetEnrichment.homTo_id, ← eHomEquiv_id, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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)
⊢ 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)
have rw₂ : Eq.{v'' + 1} (α := «to» V X ⟶ «to» V X) (𝟙 («to» V X)) (𝟙 («to» V X))
Tactic: rw [ForgetEnrichment.homTo_id, ← eHomEquiv_id, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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 Y Z : TransportEnrichment F C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X Z)
    ((Equiv.trans (eHomEquiv V) (e (@Hom.{v', u', u} _ inst inst_1 _ _ X Z)) : (a : X ⟶ Z) → 𝟙_ W ⟶ X ⟶[W] Z) (f ≫ g) :
      tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X Z)
    (CategoryStruct.comp (Y :=
        tensorObj.{v'', u''} (𝒞 := inst_4) (tensorUnit.{v'', u''} W (𝒞 := inst_4))
          (tensorUnit.{v'', u''} W (𝒞 := inst_4)))
        (Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_4))))
        (((Equiv.trans (eHomEquiv V) (e (@Hom.{v', u', u} _ inst inst_1 _ _ X Y)) : (a : X ⟶ Y) → 𝟙_ W ⟶ X ⟶[W] Y) f ⊗ₘ
            (Equiv.trans (eHomEquiv V) (e (@Hom.{v', u', u} _ inst inst_1 _ _ Y Z)) : (a : Y ⟶ Z) → 𝟙_ W ⟶ Y ⟶[W] Z)
              g) ≫
          eComp W X Y Z) :
      tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X Z)
have dsimp : Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Z))
  ((e (@Hom.{v', u', u} _ inst inst_1 _ _ X Z) : (a : 𝟙_ V ⟶ X ⟶[V] Z) → 𝟙_ W ⟶ F.obj (X ⟶[V] Z))
      ((eHomEquiv V : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g)) :
    tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Z))
  (CategoryStruct.comp (Y :=
      tensorObj.{v'', u''} (𝒞 := inst_4) (tensorUnit.{v'', u''} W (𝒞 := inst_4))
        (tensorUnit.{v'', u''} W (𝒞 := inst_4)))
      (Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_4))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v'', u''} (𝒞 := inst_4) (F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Y))
          (F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
        ((e (@Hom.{v', u', u} _ inst inst_1 _ _ X Y) : (a : 𝟙_ V ⟶ X ⟶[V] Y) → 𝟙_ W ⟶ F.obj (X ⟶[V] Y))
            ((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f) ⊗ₘ
          (e (@Hom.{v', u', u} _ inst inst_1 _ _ Y Z) : (a : 𝟙_ V ⟶ Y ⟶[V] Z) → 𝟙_ W ⟶ F.obj (Y ⟶[V] Z))
            ((eHomEquiv V : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g))
        (eComp W X Y Z)) :
    tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Z))
Tactic: dsimp +instances [instEnrichedCategoryTransportEnrichment]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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
      ((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))
have 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))
Tactic: rw [h, ForgetEnrichment.homTo_id, ← TransportEnrichment.eId_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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)
⊢ 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)))
have 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)))
Tactic: rw [← ForgetEnrichment.homOf_eId]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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)
⊢ 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)))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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 (α := Functor.obj (forgetEnrichmentEquivFunctor F D e h) X ⟶ Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)
    (CategoryStruct.comp (Y :=
        Functor.obj (forgetEnrichmentEquivFunctor F D e h)
          (Functor.obj (forgetEnrichmentEquivInverse F D e h) (Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)))
        (Functor.map (forgetEnrichmentEquivFunctor F D e h)
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (x : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)) ↦
                  Iso.refl
                    (Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x))
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (x : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) ↦
                Iso.refl (Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x))
              ⋯))
          (Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)) :
      Functor.obj (forgetEnrichmentEquivFunctor F D e h) X ⟶ Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)
    (𝟙 (Functor.obj (forgetEnrichmentEquivFunctor F D e h) X) :
      Functor.obj (forgetEnrichmentEquivFunctor F D e h) X ⟶ Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)
have simp : 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 (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))))
  (𝟙 (ForgetEnrichment.of W X))
Tactic: simp only [Functor.id_obj, forgetEnrichmentEquivFunctor_obj, Functor.comp_obj,
      forgetEnrichmentEquivInverse_obj, ForgetEnrichment.to_of, NatIso.ofComponents_hom_app,
      Iso.refl_hom, forgetEnrichmentEquivFunctor_map, h, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (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
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 (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))))
    (𝟙 (ForgetEnrichment.of W X))
have 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 (Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to V X))))
  (ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V X)))
Tactic: rw [← ForgetEnrichment.homOf_eId, TransportEnrichment.eId_eq, ForgetEnrichment.homTo_id]