mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
h2✝ : (f ≫ g ≫ h) ≫ i = f ≫ g ≫ h ≫ i
h4✝ : (f ≫ g ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
⊢ hComp (eqToIso ⋯).hom (𝟙 i) ≫ (eqToIso h2✝).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = (eqToIso h4✝).hom ≫ (eqToIso pf✝).hom

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
h2✝ : (f ≫ g ≫ h) ≫ i = f ≫ g ≫ h ≫ i
h4✝ : (f ≫ g ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
⊢ hComp (eqToIso ⋯).hom (𝟙 i) ≫ (eqToIso h2✝).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = (eqToIso h4✝).hom ≫ (eqToIso pf✝).hom
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h1 : (f ≫ 𝟙 b✝) ≫ g = f ≫ 𝟙 b✝ ≫ g
h2 : 𝟙 b✝ ≫ g = g
h3 : f ≫ 𝟙 b✝ = f
⊢ (eqToIso h1).hom ≫ hComp (𝟙 f) (eqToIso h2).hom = hComp (eqToIso h3).hom (𝟙 g)

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h1 : (f ≫ 𝟙 b✝) ≫ g = f ≫ 𝟙 b✝ ≫ g
h2 : 𝟙 b✝ ≫ g = g
h3 : f ≫ 𝟙 b✝ = f
⊢ (eqToIso h1).hom ≫ hComp (𝟙 f) (eqToIso h2).hom = hComp (eqToIso h3).hom (𝟙 g)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
g : b✝ ⟶ c✝
f : a✝ ⟶ b✝
h1✝ : f ≫ g = f ≫ g
⊢ (eqToIso h1✝).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = hComp (eqToIso ⋯).hom (𝟙 g)

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
g : b✝ ⟶ c✝
f : a✝ ⟶ b✝
h1✝ : f ≫ g = f ≫ g
⊢ (eqToIso h1✝).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = hComp (eqToIso ⋯).hom (𝟙 g)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ eHomWhiskerRight V (f ≫ f') Y = eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y

Tactic:
dsimp [eHomWhiskerRight]

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫ ((eHomEquiv V) (f ≫ f') ▷ X'' ⟶[V] Y) ≫ eComp V X X'' Y =
    ((λ_ (X'' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫ eComp V X' X'' Y) ≫
      (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case mk'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
β : f ⟶ g
base'✝ : homEquiv f ⟶ homEquiv g
H : { base' := base'✝ }.base = base β
⊢ { base' := base'✝ } = β

Tactic:
;

Goal state after:
case mk'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
β : f ⟶ g
base'✝ : homEquiv f ⟶ homEquiv g
H : { base' := base'✝ }.base = base β
⊢ { base' := base'✝ } = β
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case mk'.mk'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
base'✝¹ base'✝ : homEquiv f ⟶ homEquiv g
H : { base' := base'✝¹ }.base = { base' := base'✝ }.base
⊢ { base' := base'✝¹ } = { base' := base'✝ }

Tactic:
;

Goal state after:
case mk'.mk'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
base'✝¹ base'✝ : homEquiv f ⟶ homEquiv g
H : { base' := base'✝¹ }.base = { base' := base'✝ }.base
⊢ { base' := base'✝¹ } = { base' := base'✝ }
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case mk'.mk'.refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
base'✝ : homEquiv f ⟶ homEquiv g
⊢ { base' := base'✝ } = { base' := base'✝ }

Tactic:
;

Goal state after:
case mk'.mk'.refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
base'✝ : homEquiv f ⟶ homEquiv g
⊢ { base' := base'✝ } = { base' := base'✝ }
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f : X ⟶ Y
⊢ base (eqToHom ⋯) = eqToHom ⋯

Tactic:
;

Goal state after:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f : X ⟶ Y
⊢ base (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯

Tactic:
;

Goal state after:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case refl.refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯

Tactic:
;

Goal state after:
case refl.refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (𝟙 (𝟙 a.toBase)) (Hom.base η) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (𝟙 (𝟙 a.toBase)) (Hom.base η) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base κ

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base κ
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base η

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base η
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ eHomWhiskerRight V f Z = (eHomWhiskerRight V f Y ▷ Y ⟶[V] Z) ≫ eComp V X Y Z

Tactic:
dsimp [eHomWhiskerRight]

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ (λ_ (X' ⟶[V] Z)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Z) ≫ eComp V X X' Z =
    (((λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
g : X ⟶ Y
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝, comm := comm✝ }.f = g.f
⊢ { f := f✝, comm := comm✝ } = g

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
g : X ⟶ Y
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝, comm := comm✝ }.f = g.f
⊢ { f := f✝, comm := comm✝ } = g
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f✝¹ : X.fst ⟶ Y.fst
comm✝¹ : ∀ (U : C), f✝¹ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝¹
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝¹, comm := comm✝¹ }.f = { f := f✝, comm := comm✝ }.f
⊢ { f := f✝¹, comm := comm✝¹ } = { f := f✝, comm := comm✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f✝¹ : X.fst ⟶ Y.fst
comm✝¹ : ∀ (U : C), f✝¹ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝¹
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝¹, comm := comm✝¹ }.f = { f := f✝, comm := comm✝ }.f
⊢ { f := f✝¹, comm := comm✝¹ } = { f := f✝, comm := comm✝ }
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.snd.β U).hom ▷ (Y.fst ⊗ U') ≫ (U ⊗ X.fst) ◁ (Y.snd.β U').hom) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst) =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ X.fst Y.fst U).hom ≫
            X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ▷
          U' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              ((α_ X.fst Y.fst U').hom ≫
                X.fst ◁ (Y.snd.β U').hom ≫
                  (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom) ≫
            (α_ U U' (X.fst ⊗ Y.fst)).inv

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.snd.β U).hom ▷ (Y.fst ⊗ U') ≫ (U ⊗ X.fst) ◁ (Y.snd.β U').hom) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst) =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ X.fst Y.fst U).hom ≫
            X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ▷
          U' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              ((α_ X.fst Y.fst U').hom ≫
                X.fst ◁ (Y.snd.β U').hom ≫
                  (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom) ≫
            (α_ U U' (X.fst ⊗ Y.fst)).inv
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type w
f : F.HomObj G A
X : C
a : A.obj X
⊢ f.app X a = f.app X a

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type w
f : F.HomObj G A
X : C
a : A.obj X
⊢ f.app X a = f.app X a
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
x✝¹ : C
x✝ : (Opposite.unop (coyoneda.rightOp.obj X)).obj x✝¹
⊢ x.app x✝¹ x✝ = y.app x✝¹ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
x✝¹ : C
x✝ : (Opposite.unop (coyoneda.rightOp.obj X)).obj x✝¹
⊢ x.app x✝¹ x✝ = y.app x✝¹ x✝
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y.snd.β U).hom ≫ f ▷ Y.fst) ⊗≫ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst) =
    𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y.snd.β U).hom ⊗≫ (X.fst ◁ f ≫ (X.snd.β U').hom) ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y.snd.β U).hom ≫ f ▷ Y.fst) ⊗≫ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst) =
    𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y.snd.β U).hom ⊗≫ (X.fst ◁ f ≫ (X.snd.β U').hom) ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y.snd.β U).hom ⊗≫ ((X.snd.β U).hom ≫ f ▷ X.fst) ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst) =
    ((α_ X.fst Y.fst U).hom ≫
        X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ≫
      f ▷ (X.fst ⊗ Y.fst)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y.snd.β U).hom ⊗≫ ((X.snd.β U).hom ≫ f ▷ X.fst) ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst) =
    ((α_ X.fst Y.fst U).hom ≫
        X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ≫
      f ▷ (X.fst ⊗ Y.fst)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y₁.snd.β U).hom ≫ U ◁ f.f) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y₁.snd.β U).hom ≫ U ◁ f.f) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W g
⊢ f = g

Tactic:
;

Goal state after:
case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W g
⊢ f = g
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
⊢ f = g

Tactic:
;

Goal state after:
case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
⊢ f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: x✝³ : SSet
x✝² : x✝³ ⟶ Δ[0]
n : SimplexCategory
x✝¹ : x✝³.obj (Opposite.op n)
x✝ : Fin ((Opposite.unop (Opposite.op n)).len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom (objEquiv ((ConcreteCategory.hom (x✝².app (Opposite.op n))).toFun x✝¹))) x✝) =
    ↑((SimplexCategory.Hom.toOrderHom
          (objEquiv ((ConcreteCategory.hom ((SSet.const (obj₀Equiv.symm 0)).app (Opposite.op n))).toFun x✝¹)))
        x✝)

Tactic:
;

Goal state after:
x✝³ : SSet
x✝² : x✝³ ⟶ Δ[0]
n : SimplexCategory
x✝¹ : x✝³.obj (Opposite.op n)
x✝ : Fin ((Opposite.unop (Opposite.op n)).len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom (objEquiv ((ConcreteCategory.hom (x✝².app (Opposite.op n))).toFun x✝¹))) x✝) =
    ↑((SimplexCategory.Hom.toOrderHom
          (objEquiv ((ConcreteCategory.hom ((SSet.const (obj₀Equiv.symm 0)).app (Opposite.op n))).toFun x✝¹)))
        x✝)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.snd.β U).hom ▷ Y₁.fst ≫ (U ⊗ X.fst) ◁ f.f) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.snd.β U).hom ▷ Y₁.fst ≫ (U ⊗ X.fst) ◁ f.f) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ (ConcreteCategory.hom (eId (Type v) X ≫ ↾fun f ↦ F.map f)).toFun PUnit.unit =
    (ConcreteCategory.hom (eId (Type v) (F.obj X))).toFun PUnit.unit

Tactic:
;

Goal state after:
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ (ConcreteCategory.hom (eId (Type v) X ≫ ↾fun f ↦ F.map f)).toFun PUnit.unit =
    (ConcreteCategory.hom (eId (Type v) (F.obj X))).toFun PUnit.unit
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
f : X ⟶[Type v] Y
g : Y ⟶[Type v] Z
⊢ (ConcreteCategory.hom (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f)).toFun (f, g) =
    (ConcreteCategory.hom
          (((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z))).toFun
      (f, g)

Tactic:
;

Goal state after:
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
f : X ⟶[Type v] Y
g : Y ⟶[Type v] Z
⊢ (ConcreteCategory.hom (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f)).toFun (f, g) =
    (ConcreteCategory.hom
          (((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z))).toFun
      (f, g)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
x : ((Center.ofBraided (Type v)).obj (unop α)).fst
f : X ⟶[Type v] Y
⊢ (ConcreteCategory.hom
          ((((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
            (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y))).toFun
      (x, f) =
    (ConcreteCategory.hom
          (((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫
            eComp (Type v) (F.obj X) (G.obj X) (G.obj Y))).toFun
      (x, f)

Tactic:
;

Goal state after:
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
x : ((Center.ofBraided (Type v)).obj (unop α)).fst
f : X ⟶[Type v] Y
⊢ (ConcreteCategory.hom
          ((((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
            (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y))).toFun
      (x, f) =
    (ConcreteCategory.hom
          (((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫
            eComp (Type v) (F.obj X) (G.obj X) (G.obj Y))).toFun
      (x, f)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
⊢ (((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
      (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y) =
    ((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫ eComp (Type v) (F.obj X) (G.obj X) (G.obj Y)

Tactic:
by ext ⟨x, f⟩; exact (σ.hom x).naturality f

Goal state after: