awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (λ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      id (Opposite.unop x) ▷ @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ≫
        Iso.hom
            (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x) (Opposite.unop x))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
          comp (Opposite.unop x_1) (Opposite.unop x) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
have simp : Eq.{v₁ + 1} (α :=
  Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
    (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
  (Iso.inv (ρ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
    @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁ id (Opposite.unop x) ≫
      comp (Opposite.unop x_1) (Opposite.unop x) (Opposite.unop x))
  (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
Tactic: simp only [braiding_naturality_left_assoc, braiding_tensorUnit_left,
      Category.assoc, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (ρ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁ id (Opposite.unop x_1) ≫
        Iso.hom
            (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x_1))) ≫
          comp (Opposite.unop x_1) (Opposite.unop x_1) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
have simp : Eq.{v₁ + 1} (α :=
  Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
    (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
  (Iso.inv (λ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
    id (Opposite.unop x_1) ▷ @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ≫
      comp (Opposite.unop x_1) (Opposite.unop x_1) (Opposite.unop x))
  (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
Tactic: simp only [braiding_naturality_right_assoc, braiding_tensorUnit_right,
      Category.assoc, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ z y
g : w ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ y x
⊢ (f ⊗ₘ g) ≫ eComp V z y x = Iso.hom (β_ v w) ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)
have rw : (f ⊗ₘ g) ≫
    Iso.hom
        (β_ (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop y) (Opposite.unop z))
          (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x) (Opposite.unop y))) ≫
      eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
  Iso.hom (β_ v w) ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)
Tactic: rw [eComp_op_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (hypothesis)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : ForgetEnrichment.{v₁, u₁, u} V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).op = f.op ≫ g.op
have this : f ≫ g = homTo V (f ≫ g)
Tactic: have : (f ≫ g) = homTo V (f ≫ g) := rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : ForgetEnrichment.{v₁, u₁, u} V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ (f ≫ g).op = f.op ≫ g.op
have rw : ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫ (homTo V g ⊗ₘ homTo V f)) ≫
      eComp V (Opposite.unop («to» V z)) (Opposite.unop («to» V y)) (Opposite.unop («to» V x))).op =
  f.op ≫ g.op
Tactic: rw [this, ForgetEnrichment.homTo_comp, Category.assoc, tensorHom_eComp_op_eq,
      leftUnitor_inv_braiding_assoc, ← unitors_inv_equal, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (hypothesis)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).unop = f.unop ≫ g.unop
have this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
Tactic: have : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop) := rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ g.unop ≫ f.unop = f.unop ≫ g.unop
have rw : Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
    Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
  f.unop ≫ g.unop
Tactic: rw [this, ForgetEnrichment.homTo_comp, Category.assoc, unitors_inv_equal,
      ← leftUnitor_inv_braiding_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (hypothesis)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop
have this₁ : Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
    (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
      eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
  (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
Tactic: have : (β_ _ _).hom ≫ (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
      eComp V («to» V z.unop) («to» V y.unop) («to» V x.unop) =
      ((homTo V f.unop) ⊗ₘ (homTo V g.unop)) ≫ eComp V x y z := (tensorHom_eComp_op_eq V _ _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this_1 : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop
have rw : Eq (α := x ⟶ z)
  ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫ (homTo V f.unop ⊗ₘ homTo V g.unop)) ≫ eComp V x y z :
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ («to» V (Opposite.unop z)) («to» V (Opposite.unop x)))
  (f.unop ≫ g.unop : x ⟶ z)
Tactic: rw [this, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{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} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) :
      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)))
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
        (((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f ⊗ₘ
            (Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g) ≫
          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)
  ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) :
    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)))
      (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ Y Z)
          (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Y))
        ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ⊗ₘ
          (Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f)
        (eComp V (Opposite.unop Z) (Opposite.unop Y) (Opposite.unop X))) :
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
Tactic: simp only [tensorHom_eComp_op_eq, leftUnitor_inv_braiding_assoc, ← unitors_inv_equal]
-- 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' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ 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 (f ≫ f') Y) (eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y)
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 :=
      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 ≫ 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) (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))
Tactic: dsimp [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
X X' : C
f : X ⟶ X'
Y Z : C
⊢ 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))
    (eComp V X' Y Z ≫ eHomWhiskerRight V f Z)
    (eHomWhiskerRight V f Y ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫ eComp V X Y Z)
have dsimp : 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))
  (eComp V X' Y Z ≫
    CategoryStruct.comp (Y :=
      tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z))
      (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z)))
      ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z ≫
        eComp V X X' Z))
  (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) ▷
      @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
    eComp V X Y Z)
Tactic: dsimp [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
X Y Y' Y'' : C
g : Y ⟶ Y'
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 ≫ g')) (eHomWhiskerLeft V X g ≫ 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 :=
      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 ≫ 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''))
  (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) (@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]
-- 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 Z Z' : C
g : Z ⟶ Z'
⊢ 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'))
    (eComp V X Y Z ≫ eHomWhiskerLeft V X g)
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁ eHomWhiskerLeft V Y g ≫ eComp V X Y Z')
have dsimp : 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'))
  (eComp V X Y Z ≫
    CategoryStruct.comp (Y :=
      tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)
        (tensorUnit.{v', u'} V (𝒞 := inst)))
      (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z ◁ (eHomEquiv V : (a : Z ⟶ Z') → 𝟙_ V ⟶ Z ⟶[V] Z') g ≫
        eComp V X Z Z'))
  (@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 _ _ Y Z)
          (tensorUnit.{v', u'} V (𝒞 := inst)))
        (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ◁ (eHomEquiv V : (a : Z ⟶ Z') → 𝟙_ V ⟶ Z ⟶[V] Z') g ≫
          eComp V Y Z Z') ≫
    eComp V X Y Z')
Tactic: dsimp [eHomWhiskerLeft]
-- 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))
    (eHomWhiskerLeft V X α.hom ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
      @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁ ◁ eHomWhiskerRight V α.inv Z ≫ eComp V X Y₁ Z)
    (eComp V X Y Z)
have dsimp : 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 :=
      tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (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₁) ▷
        @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)
      (@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 _ _ Y Z))
            (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
            ((eHomEquiv V : (a : Y₁ ⟶ Y) → 𝟙_ V ⟶ Y₁ ⟶[V] Y) α.inv ▷
                @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
              eComp V Y₁ 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))
Tactic: dsimp [eHomWhiskerLeft, eHomWhiskerRight]