[GOAL]
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
F : LaxMonoidalFunctor V W
X Y : TransportEnrichment F C
⊢ (λ_ ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)).inv ≫
      ((fun X => F.ε ≫ F.map (eId V X)) X ⊗ 𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)) ≫
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          X X Y =
    𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)
[PROOFSTEP]
rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_id,
  F.left_unitality_inv_assoc, ← F.toFunctor.map_comp, ← F.toFunctor.map_comp, e_id_comp, F.toFunctor.map_id]
[GOAL]
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
F : LaxMonoidalFunctor V W
X Y : TransportEnrichment F C
⊢ (ρ_ ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)).inv ≫
      (𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y) ⊗ (fun X => F.ε ≫ F.map (eId V X)) Y) ≫
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          X Y Y =
    𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)
[PROOFSTEP]
rw [id_tensor_comp, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_id,
  F.right_unitality_inv_assoc, ← F.toFunctor.map_comp, ← F.toFunctor.map_comp, e_comp_id, F.toFunctor.map_id]
[GOAL]
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
F : LaxMonoidalFunctor V W
P Q R S : TransportEnrichment F C
⊢ (α_ ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) P Q) ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) Q R)
          ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) R S)).inv ≫
      ((fun X Y Z =>
              LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
            P Q R ⊗
          𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) R S)) ≫
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          P R S =
    (𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) P Q) ⊗
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          Q R S) ≫
      (fun X Y Z =>
          LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
        P Q S
[PROOFSTEP]
rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_id, ←
  F.associativity_inv_assoc, ← F.toFunctor.map_comp, ← F.toFunctor.map_comp, e_assoc, id_tensor_comp, Category.assoc, ←
  F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_comp]
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
⊢ (λ_ (X ⟶ Y)).inv ≫ ((fun X x => 𝟙 X) X ⊗ 𝟙 (X ⟶ Y)) ≫ (fun X Y Z p => p.fst ≫ p.snd) X X Y = 𝟙 (X ⟶ Y)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
a✝ : X ⟶ Y
⊢ ((λ_ (X ⟶ Y)).inv ≫ ((fun X x => 𝟙 X) X ⊗ 𝟙 (X ⟶ Y)) ≫ (fun X Y Z p => p.fst ≫ p.snd) X X Y) a✝ = 𝟙 (X ⟶ Y) a✝
[PROOFSTEP]
simp
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
⊢ (ρ_ (X ⟶ Y)).inv ≫ (𝟙 (X ⟶ Y) ⊗ (fun X x => 𝟙 X) Y) ≫ (fun X Y Z p => p.fst ≫ p.snd) X Y Y = 𝟙 (X ⟶ Y)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
a✝ : X ⟶ Y
⊢ ((ρ_ (X ⟶ Y)).inv ≫ (𝟙 (X ⟶ Y) ⊗ (fun X x => 𝟙 X) Y) ≫ (fun X Y Z p => p.fst ≫ p.snd) X Y Y) a✝ = 𝟙 (X ⟶ Y) a✝
[PROOFSTEP]
simp
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
W X Y Z : C
⊢ (α_ (W ⟶ X) (X ⟶ Y) (Y ⟶ Z)).inv ≫
      ((fun X Y Z p => p.fst ≫ p.snd) W X Y ⊗ 𝟙 (Y ⟶ Z)) ≫ (fun X Y Z p => p.fst ≫ p.snd) W Y Z =
    (𝟙 (W ⟶ X) ⊗ (fun X Y Z p => p.fst ≫ p.snd) X Y Z) ≫ (fun X Y Z p => p.fst ≫ p.snd) W X Z
[PROOFSTEP]
ext ⟨f, g, h⟩
[GOAL]
case h.mk.mk
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ ((α_ (W ⟶ X) (X ⟶ Y) (Y ⟶ Z)).inv ≫
        ((fun X Y Z p => p.fst ≫ p.snd) W X Y ⊗ 𝟙 (Y ⟶ Z)) ≫ (fun X Y Z p => p.fst ≫ p.snd) W Y Z)
      (f, g, h) =
    ((𝟙 (W ⟶ X) ⊗ (fun X Y Z p => p.fst ≫ p.snd) X Y Z) ≫ (fun X Y Z p => p.fst ≫ p.snd) W X Z) (f, g, h)
[PROOFSTEP]
simp
[GOAL]
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type (v + 1)
inst✝² : Category.{v, v + 1} W
inst✝¹ : MonoidalCategory W
inst✝ : EnrichedCategory W C
⊢ Category.{?u.96214, u₁} (ForgetEnrichment W C)
[PROOFSTEP]
let I : EnrichedCategory (Type v) (TransportEnrichment (coyonedaTensorUnit W) C) := inferInstance
[GOAL]
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type (v + 1)
inst✝² : Category.{v, v + 1} W
inst✝¹ : MonoidalCategory W
inst✝ : EnrichedCategory W C
I : EnrichedCategory (Type v) (TransportEnrichment (coyonedaTensorUnit W) C) := inferInstance
⊢ Category.{?u.96214, u₁} (ForgetEnrichment W C)
[PROOFSTEP]
exact enrichedCategoryTypeEquivCategory C I
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X)),
          map := fun {X Y} f =>
            ForgetEnrichment.homOf W
              (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) }.map
      (f ≫ g) =
    { obj := fun X => ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X)),
            map := fun {X Y} f =>
              ForgetEnrichment.homOf W
                (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) }.map
        f ≫
      { obj := fun X => ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X)),
            map := fun {X Y} f =>
              ForgetEnrichment.homOf W
                (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) }.map
        g
[PROOFSTEP]
dsimp
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((((λ_ (𝟙_ W)).inv ≫ (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g)) ≫
          eComp W (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
        map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Z✝)) =
    ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)) ≫
      ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W g ≫ map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))
[PROOFSTEP]
apply_fun ForgetEnrichment.homTo W
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
        ((((λ_ (𝟙_ W)).inv ≫ (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g)) ≫
            eComp W (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
          map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Z✝))) =
    ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)) ≫
        ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W g ≫ map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)))
[PROOFSTEP]
simp only [Iso.cancel_iso_inv_left, Category.assoc, tensor_comp, ForgetEnrichment.homTo_homOf, EnrichedFunctor.map_comp,
  forgetEnrichment_comp]
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g) ≫
      (map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) ⊗
          map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
        eComp W (obj F (ForgetEnrichment.to W X✝)) (obj F (ForgetEnrichment.to W Y✝))
          (obj F (ForgetEnrichment.to W Z✝)) =
    (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g) ≫
      (map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) ⊗
          map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
        eComp W (ForgetEnrichment.to W (ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X✝))))
          (ForgetEnrichment.to W (ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Y✝))))
          (ForgetEnrichment.to W (ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Z✝))))
[PROOFSTEP]
rfl
[GOAL]
case inj
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Function.Injective (ForgetEnrichment.homTo W)
[PROOFSTEP]
intro f g w
[GOAL]
case inj
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W g
⊢ f = g
[PROOFSTEP]
apply_fun ForgetEnrichment.homOf W at w 
[GOAL]
case inj
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
⊢ f = g
[PROOFSTEP]
simpa using w
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : (fun A => GradedNatTrans ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj A.unop) F G) X✝
X Y : C
⊢ (HalfBraiding.β ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj Y✝.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ (fun X => f.unop ≫ GradedNatTrans.app σ X) Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    ((fun X => f.unop ≫ GradedNatTrans.app σ X) X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
have p := σ.naturality X Y
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : (fun A => GradedNatTrans ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj A.unop) F G) X✝
X Y : C
p :
  (HalfBraiding.β ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj X✝.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ GradedNatTrans.app σ Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    (GradedNatTrans.app σ X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
⊢ (HalfBraiding.β ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj Y✝.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ (fun X => f.unop ≫ GradedNatTrans.app σ X) Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    ((fun X => f.unop ≫ GradedNatTrans.app σ X) X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
dsimp at p ⊢
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : (fun A => GradedNatTrans ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj A.unop) F G) X✝
X Y : C
p :
  (β_ X✝.unop (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ GradedNatTrans.app σ Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    (GradedNatTrans.app σ X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
⊢ (β_ Y✝.unop (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ f.unop ≫ GradedNatTrans.app σ Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    (f.unop ≫ GradedNatTrans.app σ X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc, Category.assoc, ←
  braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p, ← tensor_comp_assoc, Category.id_comp]
[GOAL]
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
⊢ eId (Type v) X ≫ (fun X Y f => F.map f) X X = eId (Type v) ((fun X => F.obj X) X)
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.unit
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
⊢ (eId (Type v) X ≫ (fun X Y f => F.map f) X X) PUnit.unit = eId (Type v) ((fun X => F.obj X) X) PUnit.unit
[PROOFSTEP]
exact F.map_id X
[GOAL]
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
⊢ eComp (Type v) X Y Z ≫ (fun X Y f => F.map f) X Z =
    ((fun X Y f => F.map f) X Y ⊗ (fun X Y f => F.map f) Y Z) ≫
      eComp (Type v) ((fun X => F.obj X) X) ((fun X => F.obj X) Y) ((fun X => F.obj X) Z)
[PROOFSTEP]
ext ⟨f, g⟩
[GOAL]
case h.mk
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 : EnrichedCategory.Hom X Y
g : EnrichedCategory.Hom Y Z
⊢ (eComp (Type v) X Y Z ≫ (fun X Y f => F.map f) X Z) (f, g) =
    (((fun X Y f => F.map f) X Y ⊗ (fun X Y f => F.map f) Y Z) ≫
        eComp (Type v) ((fun X => F.obj X) X) ((fun X => F.obj X) Y) ((fun X => F.obj X) Z))
      (f, g)
[PROOFSTEP]
exact F.map_comp f g
[GOAL]
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
⊢ (HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
        eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    ((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
ext ⟨x, f⟩
[GOAL]
case h.mk
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)).toLaxMonoidalFunctor.toFunctor.obj α.unop).fst
f : EnrichedCategory.Hom X Y
⊢ ((HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
            (EnrichedCategory.Hom X Y)).hom ≫
        (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
          eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y))
      (x, f) =
    (((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
        eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y))
      (x, f)
[PROOFSTEP]
exact (σ x).naturality f
[GOAL]
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
⊢ ∀ {X Y : Type vᵒᵖ} (f : X ⟶ Y),
    (enrichedNatTransYoneda F G).map f ≫
        ((fun α =>
              Iso.mk (fun σ x => NatTrans.mk fun X => GradedNatTrans.app σ X x) fun σ =>
                { app := fun X x => NatTrans.app (σ x) X,
                  naturality :=
                    (_ :
                      ∀ (X Y : C),
                        (HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
                                (EnrichedCategory.Hom X Y)).hom ≫
                            (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
                              eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y)
                                (EnrichedFunctor.obj G Y) =
                          ((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
                            eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X)
                              (EnrichedFunctor.obj G Y)) })
            Y).hom =
      ((fun α =>
              Iso.mk (fun σ x => NatTrans.mk fun X => GradedNatTrans.app σ X x) fun σ =>
                { app := fun X x => NatTrans.app (σ x) X,
                  naturality :=
                    (_ :
                      ∀ (X Y : C),
                        (HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
                                (EnrichedCategory.Hom X Y)).hom ≫
                            (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
                              eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y)
                                (EnrichedFunctor.obj G Y) =
                          ((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
                            eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X)
                              (EnrichedFunctor.obj G Y)) })
            X).hom ≫
        (yoneda.obj (↑enrichedFunctorTypeEquivFunctor F ⟶ ↑enrichedFunctorTypeEquivFunctor G)).map f
[PROOFSTEP]
aesop_cat
