awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
    (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y)
    (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X : TransportEnrichment F C
⊢ Eq.{w' + 1} (α := tensorUnit.{w', v'} W (𝒞 := inst_3) ⟶ @EnrichedCategory.Hom.{w', v', u₁} _ inst_3 inst_4 _ _ X X)
    (eId W X) (ε F ≫ F.map (eId V X))

Tactic:
rfl

Premises used: rfl, CategoryTheory.eId
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y Z : TransportEnrichment F C
⊢ Eq.{w' + 1} (α :=
    Quiver.Hom.{w', v'} (V := W)
      (tensorObj.{w', v'} (𝒞 := inst_3) (@EnrichedCategory.Hom.{w', v', u₁} _ inst_3 inst_4 _ _ X Y)
        (@EnrichedCategory.Hom.{w', v', u₁} _ inst_3 inst_4 _ _ Y Z))
      (@EnrichedCategory.Hom.{w', v', u₁} _ inst_3 inst_4 _ _ X Z))
    (eComp W X Y Z)
    (μ F (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z) ≫
      F.map (eComp V X Y Z))

Tactic:
rfl

Premises used: CategoryTheory.eComp, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X : C
⊢ «to».{w, v, u₁} W (of W X) = X

Tactic:
rfl

Premises used: CategoryTheory.ForgetEnrichment.of, CategoryTheory.ForgetEnrichment.to, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X : ForgetEnrichment.{w, v, u₁} W C
⊢ of W («to» W X) = X

Tactic:
rfl

Premises used: CategoryTheory.ForgetEnrichment.of, CategoryTheory.ForgetEnrichment.to, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v
inst_3 : Category.{w, v} W
inst_4 : MonoidalCategory.{w, v} W
inst_5 : EnrichedCategory.{w, v, u₁} W C
X Y : ForgetEnrichment.{w, v, u₁} W C
⊢ (X ⟶ Y) =
    (tensorUnit.{w, v} W (𝒞 := inst_3) ⟶
      @EnrichedCategory.Hom.{w, v, u₁} _ inst_3 inst_4 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))

Tactic:
rfl

Premises used: CategoryTheory.ForgetEnrichment.to, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X Y : C
f : tensorUnit.{w, v} W (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y
⊢ homTo W (homOf W f) = f

Tactic:
rfl

Premises used: CategoryTheory.ForgetEnrichment.homOf, CategoryTheory.ForgetEnrichment.homTo, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X Y : ForgetEnrichment.{w, v, u₁} W C
f : X ⟶ Y
⊢ homOf W (homTo W f) = f

Tactic:
rfl

Premises used: CategoryTheory.ForgetEnrichment.homOf, CategoryTheory.ForgetEnrichment.homTo, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X : ForgetEnrichment.{w, v, u₁} W C
⊢ homTo W (𝟙 X) = eId W («to» W X)

Tactic:
Category.id_comp _

Premises used: CategoryTheory.ForgetEnrichment.to, CategoryTheory.ForgetEnrichment.homTo, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X : C
⊢ Eq.{w + 1} (α := Quiver.Hom (V := ForgetEnrichment.{w, v, u₁} W C) (of W X) (of W X)) (homOf W (eId W X)) (𝟙 (of W X))

Tactic:
(homTo_id W (ForgetEnrichment.of W X)).symm

Premises used: CategoryTheory.ForgetEnrichment.of, CategoryTheory.ForgetEnrichment.to, CategoryTheory.ForgetEnrichment.homOf, CategoryTheory.ForgetEnrichment.homTo, CategoryTheory.ForgetEnrichment.homTo_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X Y Z : ForgetEnrichment.{w, v, u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
⊢ homTo W (f ≫ g) =
    (Iso.inv (λ_ (tensorUnit.{w, v} W (𝒞 := inst))) ≫ (homTo W f ⊗ₘ homTo W g)) ≫
      eComp W («to» W X) («to» W Y) («to» W Z)

Tactic:
rfl

Premises used: CategoryTheory.ForgetEnrichment.to, CategoryTheory.ForgetEnrichment.homTo, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X Y Z : C
f : tensorUnit.{w, v} W (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y
g : tensorUnit.{w, v} W (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z
rw : homOf W ((Iso.inv (λ_ (tensorUnit.{w, v} W (𝒞 := inst))) ≫ (f ⊗ₘ g)) ≫ eComp W X Y Z) = homOf W f ≫ homOf W g
⊢ homOf W (Iso.inv (λ_ (tensorUnit.{w, v} W (𝒞 := inst))) ≫ (f ⊗ₘ g) ≫ eComp W X Y Z) = homOf W f ≫ homOf W g

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X Y Z : C
f : tensorUnit.{w, v} W (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y
g : tensorUnit.{w, v} W (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z
⊢ homOf W ((Iso.inv (λ_ (tensorUnit.{w, v} W (𝒞 := inst))) ≫ (f ⊗ₘ g)) ≫ eComp W X Y Z) = homOf W f ≫ homOf W g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
C : Type u₁
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₁} V C
inst_4 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
h_obj : ∀ (X : C), F.obj X = G.obj X
X Y : C
rw :
  Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (F.obj Y))
    (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
rw₁ rw₂ :
  Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
    (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
⊢ Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj X) (F.obj Y))
    (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))

Tactic:
rw [h_obj, h_obj]
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
D : Type u₂
inst_2 : EnrichedCategory.{w, v, u₁} V C
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
F_obj : C → D
F_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_obj : C → D
G_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G_obj X) (G_obj Y))
map_id_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (G_obj X)
map_comp_1 : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (G_obj X) (G_obj Y) (G_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X =
      { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 :
            EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.map X
          Y ≫
        eqToHom ⋯ =
      { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }.map X Y
⊢ F_obj = G_obj

Tactic:
funext fun X ↦ h_obj X

Premises used: funext
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
D : Type u₂
inst_2 : EnrichedCategory.{w, v, u₁} V C
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
F_obj : C → D
F_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_obj : C → D
G_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G_obj X) (G_obj Y))
map_id_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (G_obj X)
map_comp_1 : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (G_obj X) (G_obj Y) (G_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X =
      { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 :
            EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.map X
          Y ≫
        eqToHom ⋯ =
      { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }.map X Y
obtain :
  ∀
    (G_map :
      (X Y : C) →
        Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y)))
    (map_id_2 : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X))
    (map_comp_2 :
      ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z))
    (h_obj :
      ∀ (X : C),
        { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp :
                EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
            X =
          { obj := F_obj, map := G_map, map_id := map_id_2, map_comp := map_comp_2 :
                EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
            X)
    (h_map :
      ∀ (X Y : C),
        { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp :
                  EnrichedFunctor.{w, v, u₁, u₂} V C D }.map
              X Y ≫
            eqToHom ⋯ =
          { obj := F_obj, map := G_map, map_id := map_id_2, map_comp := map_comp_2 }.map X Y),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D } =
      { obj := F_obj, map := G_map, map_id := map_id_2, map_comp := map_comp_2 }
⊢ { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D } =
    { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }

Tactic:
obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X

Premises used: funext, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
D : Type u₂
inst_2 : EnrichedCategory.{w, v, u₁} V C
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
F_obj : C → D
F_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp_1 : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X =
      { obj := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 :
            EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.map X
          Y ≫
        eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }.map X Y
e_map : F_map = G_map
⊢ { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D } =
    { obj := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
D : Type u₂
inst_2 : EnrichedCategory.{w, v, u₁} V C
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
F_obj : C → D
F_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp_1 : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X =
      { obj := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 :
            EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.map X
          Y ≫
        eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }.map X Y
e_map : ∀ (X Y : C), F_map X Y = G_map X Y
⊢ F_map = G_map

Tactic:
ext X Y
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
D : Type u₂
inst_2 : EnrichedCategory.{w, v, u₁} V C
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
F_obj : C → D
F_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp_1 : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X =
      { obj := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 :
            EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.map X
          Y ≫
        eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }.map X Y
X Y : C
⊢ F_map X Y = G_map X Y

Tactic:
simpa using h_map X Y
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
D : Type u₂
inst_2 : EnrichedCategory.{w, v, u₁} V C
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C), F.map X Y ≫ eqToHom ⋯ = G.map X Y
⊢ F = G

Tactic:
match F, G with
  | mk F_obj F_map _ _, mk G_obj G_map _ _ =>
    obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X
    congr
    ext X Y
    simpa using h_map X Y
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
dsimp :
  ForgetEnrichment.homOf W
      (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
            (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
          eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z)) =
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
      ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))
⊢ ForgetEnrichment.homOf W
      (ForgetEnrichment.homTo W (f ≫ g) ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z)) =
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
      ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
apply_fun :
  ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
        (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
              (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
            eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
          F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z))) =
    ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
        ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)))
inj :
  Function.Injective.{w' + 1, w' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{w', v', u₂} W D) (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X)))
      (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z))))
    (ForgetEnrichment.homTo W)
⊢ ForgetEnrichment.homOf W
      (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
            (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
          eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z)) =
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
      ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))

Tactic:
apply_fun ForgetEnrichment.homTo W

Premises used: CategoryTheory.ForgetEnrichment.homTo
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
simp :
  (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
      (F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) ⊗ₘ
          F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        eComp W (F.obj (ForgetEnrichment.to W X)) (F.obj (ForgetEnrichment.to W Y)) (F.obj (ForgetEnrichment.to W Z)) =
    (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
      (F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) ⊗ₘ
          F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        eComp W (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X))))
          (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Y))))
          (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z))))
⊢ ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
        (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
              (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
            eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
          F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z))) =
    ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
        ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)))

Tactic:
simp only [Iso.cancel_iso_inv_left, Category.assoc, ← tensorHom_comp_tensorHom,
        ForgetEnrichment.homTo_homOf, EnrichedFunctor.map_comp, ForgetEnrichment.homTo_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Iso.cancel_iso_inv_left, CategoryTheory.ForgetEnrichment.homTo_comp, CategoryTheory.ForgetEnrichment.homTo_homOf, CategoryTheory.EnrichedFunctor.map_comp