[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((fun d =>
                Functor.mk
                  { obj := fun t => ∐ fun x => d,
                    map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
              x✝).map
          f_1 ≫
        (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) Y =
      (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) X ≫
        ((fun d =>
                Functor.mk
                  { obj := fun t => ∐ fun x => d,
                    map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
              d₂).map
          f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((fun d =>
              Functor.mk
                { obj := fun t => ∐ fun x => d,
                  map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
            x✝).map
        f✝ ≫
      (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) Y✝ =
    (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) X✝ ≫
      ((fun d =>
              Functor.mk
                { obj := fun t => ∐ fun x => d,
                  map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
            d₂).map
        f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((Sigma.desc fun g => Sigma.ι (fun x => x✝) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) =
    (Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) ≫ Sigma.desc fun g => Sigma.ι (fun x => d₂) (g ≫ f✝)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : c ⟶ X✝
⊢ (Sigma.ι (fun x => x✝) b✝ ≫
      (Sigma.desc fun g => Sigma.ι (fun x => x✝) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) =
    Sigma.ι (fun x => x✝) b✝ ≫
      (Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) ≫ Sigma.desc fun g => Sigma.ι (fun x => d₂) (g ≫ f✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((evaluationLeftAdjoint D c).obj d).map f_1 ≫ (fun e => Sigma.desc fun h => f ≫ F.map h) Y =
      (fun e => Sigma.desc fun h => f ≫ F.map h) X ≫ F.map f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((evaluationLeftAdjoint D c).obj d).map f✝ ≫ (fun e => Sigma.desc fun h => f ≫ F.map h) Y✝ =
    (fun e => Sigma.desc fun h => f ≫ F.map h) X✝ ≫ F.map f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ F.map h) =
    (Sigma.desc fun h => f ≫ F.map h) ≫ F.map f✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : c ⟶ X✝
⊢ (Sigma.ι (fun x => d) b✝ ≫ (Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ F.map h) =
    Sigma.ι (fun x => d) b✝ ≫ (Sigma.desc fun h => f ≫ F.map h) ≫ F.map f✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
⊢ Function.LeftInverse (fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h) fun f =>
    Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c
[PROOFSTEP]
intro f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
⊢ (fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h)
      ((fun f => Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
⊢ NatTrans.app
      ((fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h)
        ((fun f => Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) f))
      x =
    NatTrans.app f x
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
⊢ (Sigma.desc fun h => (Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) ≫ F.map h) = NatTrans.app f x
[PROOFSTEP]
ext g
[GOAL]
case w.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
g : c ⟶ x
⊢ (Sigma.ι (fun x => d) g ≫ Sigma.desc fun h => (Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) ≫ F.map h) =
    Sigma.ι (fun x => d) g ≫ NatTrans.app f x
[PROOFSTEP]
simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ← f.naturality, evaluationLeftAdjoint_obj_map,
  colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Discrete.natTrans_app, Category.id_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ (fun f => Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c)
      ((fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h) f) =
    f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ (Sigma.ι (fun x => d) (𝟙 c) ≫ Sigma.desc fun h => f ≫ F.map h) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η ↔ ∀ (c : C), Mono (app η c)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η → ∀ (c : C), Mono (app η c)
[PROOFSTEP]
intro h c
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Mono η
c : C
⊢ Mono (app η c)
[PROOFSTEP]
exact (inferInstance : Mono (((evaluation _ _).obj c).map η))
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Mono (app η c)) → Mono η
[PROOFSTEP]
intro _
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Mono (app η c)
⊢ Mono η
[PROOFSTEP]
apply NatTrans.mono_of_mono_app
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((fun d =>
                Functor.mk
                  { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
              X✝).map
          f_1 ≫
        (fun t => Pi.lift fun g => Pi.π (fun x => X✝) g ≫ f) Y =
      (fun t => Pi.lift fun g => Pi.π (fun x => X✝) g ≫ f) X ≫
        ((fun d =>
                Functor.mk
                  { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
              Y✝).map
          f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((fun d =>
              Functor.mk
                { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
            X✝¹).map
        f✝ ≫
      (fun t => Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) Y✝ =
    (fun t => Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) X✝ ≫
      ((fun d =>
              Functor.mk
                { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
            Y✝¹).map
        f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((Pi.lift fun g => Pi.π (fun x => X✝¹) (f✝ ≫ g)) ≫ Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) =
    (Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => Y✝¹) (f✝ ≫ g)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : Y✝ ⟶ c
⊢ ((Pi.lift fun g => Pi.π (fun x => X✝¹) (f✝ ≫ g)) ≫ Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) ≫
      Pi.π (fun x => Y✝¹) b✝ =
    ((Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => Y✝¹) (f✝ ≫ g)) ≫
      Pi.π (fun x => Y✝¹) b✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    F.map f_1 ≫ (fun t => Pi.lift fun g => F.map g ≫ f) Y =
      (fun t => Pi.lift fun g => F.map g ≫ f) X ≫ ((evaluationRightAdjoint D c).obj d).map f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (fun t => Pi.lift fun g => F.map g ≫ f) Y✝ =
    (fun t => Pi.lift fun g => F.map g ≫ f) X✝ ≫ ((evaluationRightAdjoint D c).obj d).map f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (F.map f✝ ≫ Pi.lift fun g => F.map g ≫ f) =
    (Pi.lift fun g => F.map g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => d) (f✝ ≫ g)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : Y✝ ⟶ c
⊢ (F.map f✝ ≫ Pi.lift fun g => F.map g ≫ f) ≫ Pi.π (fun x => d) b✝ =
    ((Pi.lift fun g => F.map g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => d) (f✝ ≫ g)) ≫ Pi.π (fun x => d) b✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ (fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c))
      ((fun f => NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f) f) =
    f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ (Pi.lift fun g => F.map g ≫ f) ≫ Pi.π (fun x => d) (𝟙 c) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
⊢ Function.RightInverse (fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) fun f =>
    NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f
[PROOFSTEP]
intro f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
⊢ (fun f => NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f)
      ((fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
⊢ NatTrans.app
      ((fun f => NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f)
        ((fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) f))
      x =
    NatTrans.app f x
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
⊢ (Pi.lift fun g => F.map g ≫ NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) = NatTrans.app f x
[PROOFSTEP]
ext g
[GOAL]
case w.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
g : x ⟶ c
⊢ (Pi.lift fun g => F.map g ≫ NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) ≫ Pi.π (fun x => d) g =
    NatTrans.app f x ≫ Pi.π (fun x => d) g
[PROOFSTEP]
simp only [Discrete.functor_obj, NatTrans.naturality_assoc, evaluationRightAdjoint_obj_obj,
  evaluationRightAdjoint_obj_map, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Discrete.natTrans_app, Category.comp_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η ↔ ∀ (c : C), Epi (app η c)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η → ∀ (c : C), Epi (app η c)
[PROOFSTEP]
intro h c
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Epi η
c : C
⊢ Epi (app η c)
[PROOFSTEP]
exact (inferInstance : Epi (((evaluation _ _).obj c).map η))
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Epi (app η c)) → Epi η
[PROOFSTEP]
intros
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Epi (app η c)
⊢ Epi η
[PROOFSTEP]
apply NatTrans.epi_of_epi_app


[GOAL]
X : Type u
inst✝¹ : Preorder X
inst✝ : OrderTop X
x : X
a : x ⟶ ⊤
⊢ a = default
[PROOFSTEP]
rfl
[GOAL]
X : Type u
inst✝¹ : Preorder X
inst✝ : OrderBot X
x : X
a : ⊥ ⟶ x
⊢ a = default
[PROOFSTEP]
rfl


[GOAL]
C : Type u
X Y Z : F C
⊢ Discrete.functor (normalizeObj (tensor (tensor X Y) Z)) ⟶ Discrete.functor (normalizeObj (tensor X (tensor Y Z)))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
X Y Z : F C
⊢ (Discrete.functor fun x => normalizeObj Z (normalizeObj Y (normalizeObj X x).as).as) ⟶
    Discrete.functor fun x => normalizeObj Z (normalizeObj Y (normalizeObj X x).as).as
[PROOFSTEP]
exact Discrete.natTrans (fun _ => 𝟙 _)
[GOAL]
C : Type u
X✝ Y✝ Z✝ : F C
⊢ Discrete.functor (normalizeObj (tensor X✝ (tensor Y✝ Z✝))) ⟶
    Discrete.functor (normalizeObj (tensor (tensor X✝ Y✝) Z✝))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
X✝ Y✝ Z✝ : F C
⊢ (Discrete.functor fun x => normalizeObj Z✝ (normalizeObj Y✝ (normalizeObj X✝ x).as).as) ⟶
    Discrete.functor fun x => normalizeObj Z✝ (normalizeObj Y✝ (normalizeObj X✝ x).as).as
[PROOFSTEP]
exact Discrete.natTrans (fun _ => 𝟙 _)
[GOAL]
C : Type u
a✝ : F C
⊢ Discrete.functor (normalizeObj (tensor Unit a✝)) ⟶ Discrete.functor (normalizeObj a✝)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
a✝ : F C
⊢ (Discrete.functor fun x => normalizeObj a✝ x) ⟶ Discrete.functor (normalizeObj a✝)
[PROOFSTEP]
exact Discrete.natTrans (fun _ => 𝟙 _)
[GOAL]
C : Type u
a✝ : F C
⊢ Discrete.functor (normalizeObj a✝) ⟶ Discrete.functor (normalizeObj (tensor Unit a✝))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
a✝ : F C
⊢ Discrete.functor (normalizeObj a✝) ⟶ Discrete.functor fun x => normalizeObj a✝ x
[PROOFSTEP]
exact Discrete.natTrans (fun _ => 𝟙 _)
[GOAL]
C : Type u
a✝ : F C
⊢ Discrete.functor (normalizeObj (tensor a✝ Unit)) ⟶ Discrete.functor (normalizeObj a✝)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
a✝ : F C
⊢ (Discrete.functor fun x => { as := (normalizeObj a✝ x).as }) ⟶ Discrete.functor (normalizeObj a✝)
[PROOFSTEP]
exact Discrete.natTrans (fun _ => 𝟙 _)
[GOAL]
C : Type u
a✝ : F C
⊢ Discrete.functor (normalizeObj a✝) ⟶ Discrete.functor (normalizeObj (tensor a✝ Unit))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
a✝ : F C
⊢ Discrete.functor (normalizeObj a✝) ⟶ Discrete.functor fun x => { as := (normalizeObj a✝ x).as }
[PROOFSTEP]
exact Discrete.natTrans (fun _ => 𝟙 _)
[GOAL]
C : Type u
T X✝ Y✝ W : F C
f : T ⟶ᵐ Y✝
g : X✝ ⟶ᵐ W
⊢ Discrete.functor (normalizeObj (tensor T X✝)) ⟶ Discrete.functor (normalizeObj (tensor Y✝ W))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
T X✝ Y✝ W : F C
f : T ⟶ᵐ Y✝
g : X✝ ⟶ᵐ W
⊢ (Discrete.functor fun x => normalizeObj X✝ (normalizeObj T x).as) ⟶
    Discrete.functor fun x => normalizeObj W (normalizeObj Y✝ x).as
[PROOFSTEP]
exact
  Discrete.natTrans
    (fun ⟨X⟩ =>
      (normalizeMapAux g).app (normalizeObj T X) ≫
        (Discrete.functor (normalizeObj W) : _ ⥤ N C).map ((normalizeMapAux f).app ⟨X⟩))
[GOAL]
C : Type u
X Y : F C
⊢ ∀ (a b : X ⟶ᵐ Y), a ≈ b → normalizeMapAux a = normalizeMapAux b
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
Z : F C
n n' : (Discrete ∘ NormalMonoidalObject) C
f : n ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
[PROOFSTEP]
cases n
[GOAL]
case mk
C : Type u
Z : F C
n' : (Discrete ∘ NormalMonoidalObject) C
as✝ : NormalMonoidalObject C
f : { as := as✝ } ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
[PROOFSTEP]
cases n'
[GOAL]
case mk.mk
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
[PROOFSTEP]
rcases f with ⟨⟨h⟩⟩
[GOAL]
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : { as := as✝¹ }.as = { as := as✝ }.as
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ⊗ 𝟙 Z
[PROOFSTEP]
dsimp at h
[GOAL]
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : as✝¹ = as✝
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ⊗ 𝟙 Z
[PROOFSTEP]
subst h
[GOAL]
case mk.mk.up.up
C : Type u
Z : F C
as✝ : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map { down := { down := (_ : as✝ = as✝) } } =
    inclusion.map { down := { down := (_ : as✝ = as✝) } } ⊗ 𝟙 Z
[PROOFSTEP]
simp
[GOAL]
C : Type u
X : F C
⊢ ∀ {X_1 Y : (Discrete ∘ NormalMonoidalObject) C} (f : X_1 ⟶ Y),
    ((tensorFunc C).obj X).map f ≫ (normalizeIsoApp C X Y).hom =
      (normalizeIsoApp C X X_1).hom ≫ ((normalize' C).obj X).map f
[PROOFSTEP]
rintro ⟨X⟩ ⟨Y⟩ ⟨⟨f⟩⟩
[GOAL]
case mk.mk.up.up
C : Type u
X✝ : F C
X Y : NormalMonoidalObject C
f : { as := X }.as = { as := Y }.as
⊢ ((tensorFunc C).obj X✝).map { down := { down := f } } ≫ (normalizeIsoApp C X✝ { as := Y }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ ((normalize' C).obj X✝).map { down := { down := f } }
[PROOFSTEP]
dsimp at f
[GOAL]
case mk.mk.up.up
C : Type u
X✝ : F C
X Y : NormalMonoidalObject C
f : X = Y
⊢ ((tensorFunc C).obj X✝).map { down := { down := f } } ≫ (normalizeIsoApp C X✝ { as := Y }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ ((normalize' C).obj X✝).map { down := { down := f } }
[PROOFSTEP]
subst f
[GOAL]
case mk.mk.up.up
C : Type u
X✝ : F C
X : NormalMonoidalObject C
⊢ ((tensorFunc C).obj X✝).map { down := { down := (_ : X = X) } } ≫ (normalizeIsoApp C X✝ { as := X }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ ((normalize' C).obj X✝).map { down := { down := (_ : X = X) } }
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.up.up
C : Type u
X✝ : F C
X : NormalMonoidalObject C
⊢ (Discrete.functor fun n => inclusionObj n ⊗ X✝).map { down := { down := (_ : X = X) } } ≫
      (normalizeIsoApp C X✝ { as := X }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫
      (((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
                (Discrete.functor inclusionObj)).obj
            (Discrete.functor (normalizeObj X✝))).map
        { down := { down := (_ : X = X) } }
[PROOFSTEP]
simp
[GOAL]
C : Type u
⊢ ∀ {X Y : F C} (f : X ⟶ Y),
    (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f
[PROOFSTEP]
rintro X Y f
[GOAL]
C : Type u
X Y : F C
f : X ⟶ Y
⊢ (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f
[PROOFSTEP]
induction' f using Quotient.recOn with f
[GOAL]
case f
C : Type u
X Y : F C
f : X ⟶ᵐ Y
⊢ (tensorFunc C).map (Quotient.mk (setoidHom X Y) f) ≫ (normalizeIsoAux C Y).hom =
    (normalizeIsoAux C X).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X Y) f)
case h
C : Type u
X Y : F C
f : X ⟶ Y
a✝ b✝ : X ⟶ᵐ Y
p✝ : a✝ ≈ b✝
⊢ (_ :
      (tensorFunc C).map (Quotient.mk (setoidHom X Y) b✝) ≫ (normalizeIsoAux C Y).hom =
        (normalizeIsoAux C X).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X Y) b✝)) =
    (_ :
      (tensorFunc C).map (Quotient.mk (setoidHom X Y) b✝) ≫ (normalizeIsoAux C Y).hom =
        (normalizeIsoAux C X).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X Y) b✝))
[PROOFSTEP]
swap
[GOAL]
case h
C : Type u
X Y : F C
f : X ⟶ Y
a✝ b✝ : X ⟶ᵐ Y
p✝ : a✝ ≈ b✝
⊢ (_ :
      (tensorFunc C).map (Quotient.mk (setoidHom X Y) b✝) ≫ (normalizeIsoAux C Y).hom =
        (normalizeIsoAux C X).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X Y) b✝)) =
    (_ :
      (tensorFunc C).map (Quotient.mk (setoidHom X Y) b✝) ≫ (normalizeIsoAux C Y).hom =
        (normalizeIsoAux C X).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X Y) b✝))
case f
C : Type u
X Y : F C
f : X ⟶ᵐ Y
⊢ (tensorFunc C).map (Quotient.mk (setoidHom X Y) f) ≫ (normalizeIsoAux C Y).hom =
    (normalizeIsoAux C X).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X Y) f)
[PROOFSTEP]
rfl
[GOAL]
case f
C : Type u
X Y : F C
f : X ⟶ᵐ Y
⊢ (tensorFunc C).map (Quotient.mk (setoidHom X Y) f) ≫ (normalizeIsoAux C Y).hom =
    (normalizeIsoAux C X).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X Y) f)
[PROOFSTEP]
induction' f with _ X₁ X₂ X₃ _ _ _ _ _ _ _ _ _ _ _ _ h₁ h₂ X₁ X₂ Y₁ Y₂ f g h₁ h₂
[GOAL]
case f.id
C : Type u
X Y X✝ : F C
⊢ (tensorFunc C).map (Quotient.mk (setoidHom X✝ X✝) (Hom.id X✝)) ≫ (normalizeIsoAux C X✝).hom =
    (normalizeIsoAux C X✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X✝ X✝) (Hom.id X✝))
[PROOFSTEP]
simp only [mk_id, Functor.map_id, Category.comp_id, Category.id_comp]
[GOAL]
case f.α_hom
C : Type u
X Y X₁ X₂ X₃ : F C
⊢ (tensorFunc C).map
        (Quotient.mk (setoidHom (tensor (tensor X₁ X₂) X₃) (tensor X₁ (tensor X₂ X₃))) (Hom.α_hom X₁ X₂ X₃)) ≫
      (normalizeIsoAux C (tensor X₁ (tensor X₂ X₃))).hom =
    (normalizeIsoAux C (tensor (tensor X₁ X₂) X₃)).hom ≫
      (normalize' C).map
        (Quotient.mk (setoidHom (tensor (tensor X₁ X₂) X₃) (tensor X₁ (tensor X₂ X₃))) (Hom.α_hom X₁ X₂ X₃))
[PROOFSTEP]
ext n
[GOAL]
case f.α_hom.w.h
C : Type u
X Y X₁ X₂ X₃ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((tensorFunc C).map
          (Quotient.mk (setoidHom (tensor (tensor X₁ X₂) X₃) (tensor X₁ (tensor X₂ X₃))) (Hom.α_hom X₁ X₂ X₃)) ≫
        (normalizeIsoAux C (tensor X₁ (tensor X₂ X₃))).hom)
      n =
    NatTrans.app
      ((normalizeIsoAux C (tensor (tensor X₁ X₂) X₃)).hom ≫
        (normalize' C).map
          (Quotient.mk (setoidHom (tensor (tensor X₁ X₂) X₃) (tensor X₁ (tensor X₂ X₃))) (Hom.α_hom X₁ X₂ X₃)))
      n
[PROOFSTEP]
dsimp
[GOAL]
case f.α_hom.w.h
C : Type u
X Y X₁ X₂ X₃ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((Discrete.natTrans fun n =>
          𝟙 (inclusionObj n.as) ⊗ Quotient.mk (setoidHom ((X₁ ⊗ X₂) ⊗ X₃) (X₁ ⊗ X₂ ⊗ X₃)) (Hom.α_hom X₁ X₂ X₃)) ≫
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X₁ (X₂ ⊗ X₃)).symm ≪≫
              (normalizeIsoApp C X₁ x ⊗ Iso.refl (X₂ ⊗ X₃)) ≪≫
                (α_ (inclusionObj (normalizeObj X₁ x.as).as) X₂ X₃).symm ≪≫
                  (normalizeIsoApp C X₂ (normalizeObj X₁ x.as) ⊗ Iso.refl X₃) ≪≫
                    normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ x.as).as)).hom)
      n =
    NatTrans.app
      ((NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (X₁ ⊗ X₂) X₃).symm ≪≫
              ((α_ (inclusionObj x.as) X₁ X₂).symm ≪≫
                    (normalizeIsoApp C X₁ x ⊗ Iso.refl X₂) ≪≫ normalizeIsoApp C X₂ (normalizeObj X₁ x.as) ⊗
                  Iso.refl X₃) ≪≫
                normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ x.as).as)).hom ≫
        ((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x =>
            𝟙 ((Discrete.functor fun x => normalizeObj X₃ (normalizeObj X₂ (normalizeObj X₁ x).as).as).obj x)))
      n
[PROOFSTEP]
rw [mk_α_hom, NatTrans.comp_app, NatTrans.comp_app]
[GOAL]
case f.α_hom.w.h
C : Type u
X Y X₁ X₂ X₃ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app (Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).hom) n ≫
      NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X₁ (X₂ ⊗ X₃)).symm ≪≫
              (normalizeIsoApp C X₁ x ⊗ Iso.refl (X₂ ⊗ X₃)) ≪≫
                (α_ (inclusionObj (normalizeObj X₁ x.as).as) X₂ X₃).symm ≪≫
                  (normalizeIsoApp C X₂ (normalizeObj X₁ x.as) ⊗ Iso.refl X₃) ≪≫
                    normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ x.as).as)).hom
        n =
    NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (X₁ ⊗ X₂) X₃).symm ≪≫
              ((α_ (inclusionObj x.as) X₁ X₂).symm ≪≫
                    (normalizeIsoApp C X₁ x ⊗ Iso.refl X₂) ≪≫ normalizeIsoApp C X₂ (normalizeObj X₁ x.as) ⊗
                  Iso.refl X₃) ≪≫
                normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ x.as).as)).hom
        n ≫
      NatTrans.app
        (((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x =>
            𝟙 ((Discrete.functor fun x => normalizeObj X₃ (normalizeObj X₂ (normalizeObj X₁ x).as).as).obj x)))
        n
[PROOFSTEP]
dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
[GOAL]
case f.α_hom.w.h
C : Type u
X Y X₁ X₂ X₃ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).hom) ≫
      (α_ (inclusionObj n.as) X₁ (X₂ ⊗ X₃)).inv ≫
        ((normalizeIsoApp C X₁ n).hom ⊗ 𝟙 (X₂ ⊗ X₃)) ≫
          (α_ (inclusionObj (normalizeObj X₁ n.as).as) X₂ X₃).inv ≫
            ((normalizeIsoApp C X₂ (normalizeObj X₁ n.as)).hom ⊗ 𝟙 X₃) ≫
              (normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ n.as).as)).hom =
    ((α_ (inclusionObj n.as) (X₁ ⊗ X₂) X₃).inv ≫
        ((α_ (inclusionObj n.as) X₁ X₂).inv ≫
              ((normalizeIsoApp C X₁ n).hom ⊗ 𝟙 X₂) ≫ (normalizeIsoApp C X₂ (normalizeObj X₁ n.as)).hom ⊗
            𝟙 X₃) ≫
          (normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ n.as).as)).hom) ≫
      𝟙
        (inclusionObj
          ((Discrete.functor fun x => normalizeObj X₃ (normalizeObj X₂ (normalizeObj X₁ x).as).as).obj n).as)
[PROOFSTEP]
simp only [comp_tensor_id, associator_conjugation, tensor_id, Category.comp_id]
[GOAL]
case f.α_hom.w.h
C : Type u
X Y X₁ X₂ X₃ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).hom) ≫
      (α_ (inclusionObj n.as) X₁ (X₂ ⊗ X₃)).inv ≫
        ((normalizeIsoApp C X₁ n).hom ⊗ 𝟙 (X₂ ⊗ X₃)) ≫
          (α_ (inclusionObj (normalizeObj X₁ n.as).as) X₂ X₃).inv ≫
            ((normalizeIsoApp C X₂ (normalizeObj X₁ n.as)).hom ⊗ 𝟙 X₃) ≫
              (normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ n.as).as)).hom =
    (α_ (inclusionObj n.as) (X₁ ⊗ X₂) X₃).inv ≫
      (((α_ (inclusionObj n.as) X₁ X₂).inv ⊗ 𝟙 X₃) ≫
          ((α_ (inclusionObj n.as ⊗ X₁) X₂ X₃).hom ≫
              ((normalizeIsoApp C X₁ n).hom ⊗ 𝟙 (X₂ ⊗ X₃)) ≫
                (α_ (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj n).as) X₂ X₃).inv) ≫
            ((normalizeIsoApp C X₂ (normalizeObj X₁ n.as)).hom ⊗ 𝟙 X₃)) ≫
        (normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ n.as).as)).hom
[PROOFSTEP]
simp only [← Category.assoc]
[GOAL]
case f.α_hom.w.h
C : Type u
X Y X₁ X₂ X₃ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (((((𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).hom) ≫ (α_ (inclusionObj n.as) X₁ (X₂ ⊗ X₃)).inv) ≫
            ((normalizeIsoApp C X₁ n).hom ⊗ 𝟙 (X₂ ⊗ X₃))) ≫
          (α_ (inclusionObj (normalizeObj X₁ n.as).as) X₂ X₃).inv) ≫
        ((normalizeIsoApp C X₂ (normalizeObj X₁ n.as)).hom ⊗ 𝟙 X₃)) ≫
      (normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ n.as).as)).hom =
    ((((((α_ (inclusionObj n.as) (X₁ ⊗ X₂) X₃).inv ≫ ((α_ (inclusionObj n.as) X₁ X₂).inv ⊗ 𝟙 X₃)) ≫
              (α_ (inclusionObj n.as ⊗ X₁) X₂ X₃).hom) ≫
            ((normalizeIsoApp C X₁ n).hom ⊗ 𝟙 (X₂ ⊗ X₃))) ≫
          (α_ (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj n).as) X₂ X₃).inv) ≫
        ((normalizeIsoApp C X₂ (normalizeObj X₁ n.as)).hom ⊗ 𝟙 X₃)) ≫
      (normalizeIsoApp C X₃ (normalizeObj X₂ (normalizeObj X₁ n.as).as)).hom
[PROOFSTEP]
congr 4
[GOAL]
case f.α_hom.w.h.e_a.e_a.e_a.e_a
C : Type u
X Y X₁ X₂ X₃ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).hom) ≫ (α_ (inclusionObj n.as) X₁ (X₂ ⊗ X₃)).inv =
    ((α_ (inclusionObj n.as) (X₁ ⊗ X₂) X₃).inv ≫ ((α_ (inclusionObj n.as) X₁ X₂).inv ⊗ 𝟙 X₃)) ≫
      (α_ (inclusionObj n.as ⊗ X₁) X₂ X₃).hom
[PROOFSTEP]
simp only [Category.assoc, ← cancel_epi (𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).inv),
  pentagon_inv_assoc (inclusionObj n.as) X₁ X₂ X₃, tensor_inv_hom_id_assoc, tensor_id, Category.id_comp, Iso.inv_hom_id,
  Category.comp_id]
[GOAL]
case f.α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ (tensorFunc C).map
        (Quotient.mk (setoidHom (tensor X✝ (tensor Y✝ Z✝)) (tensor (tensor X✝ Y✝) Z✝)) (Hom.α_inv X✝ Y✝ Z✝)) ≫
      (normalizeIsoAux C (tensor (tensor X✝ Y✝) Z✝)).hom =
    (normalizeIsoAux C (tensor X✝ (tensor Y✝ Z✝))).hom ≫
      (normalize' C).map
        (Quotient.mk (setoidHom (tensor X✝ (tensor Y✝ Z✝)) (tensor (tensor X✝ Y✝) Z✝)) (Hom.α_inv X✝ Y✝ Z✝))
[PROOFSTEP]
ext n
[GOAL]
case f.α_inv.w.h
C : Type u
X Y X✝ Y✝ Z✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((tensorFunc C).map
          (Quotient.mk (setoidHom (tensor X✝ (tensor Y✝ Z✝)) (tensor (tensor X✝ Y✝) Z✝)) (Hom.α_inv X✝ Y✝ Z✝)) ≫
        (normalizeIsoAux C (tensor (tensor X✝ Y✝) Z✝)).hom)
      n =
    NatTrans.app
      ((normalizeIsoAux C (tensor X✝ (tensor Y✝ Z✝))).hom ≫
        (normalize' C).map
          (Quotient.mk (setoidHom (tensor X✝ (tensor Y✝ Z✝)) (tensor (tensor X✝ Y✝) Z✝)) (Hom.α_inv X✝ Y✝ Z✝)))
      n
[PROOFSTEP]
dsimp
[GOAL]
case f.α_inv.w.h
C : Type u
X Y X✝ Y✝ Z✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((Discrete.natTrans fun n =>
          𝟙 (inclusionObj n.as) ⊗ Quotient.mk (setoidHom (X✝ ⊗ Y✝ ⊗ Z✝) ((X✝ ⊗ Y✝) ⊗ Z✝)) (Hom.α_inv X✝ Y✝ Z✝)) ≫
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (X✝ ⊗ Y✝) Z✝).symm ≪≫
              ((α_ (inclusionObj x.as) X✝ Y✝).symm ≪≫
                    (normalizeIsoApp C X✝ x ⊗ Iso.refl Y✝) ≪≫ normalizeIsoApp C Y✝ (normalizeObj X✝ x.as) ⊗
                  Iso.refl Z✝) ≪≫
                normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ x.as).as)).hom)
      n =
    NatTrans.app
      ((NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X✝ (Y✝ ⊗ Z✝)).symm ≪≫
              (normalizeIsoApp C X✝ x ⊗ Iso.refl (Y✝ ⊗ Z✝)) ≪≫
                (α_ (inclusionObj (normalizeObj X✝ x.as).as) Y✝ Z✝).symm ≪≫
                  (normalizeIsoApp C Y✝ (normalizeObj X✝ x.as) ⊗ Iso.refl Z✝) ≪≫
                    normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ x.as).as)).hom ≫
        ((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x =>
            𝟙 ((Discrete.functor fun x => normalizeObj Z✝ (normalizeObj Y✝ (normalizeObj X✝ x).as).as).obj x)))
      n
[PROOFSTEP]
rw [mk_α_inv, NatTrans.comp_app, NatTrans.comp_app]
[GOAL]
case f.α_inv.w.h
C : Type u
X Y X✝ Y✝ Z✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app (Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ (α_ X✝ Y✝ Z✝).inv) n ≫
      NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (X✝ ⊗ Y✝) Z✝).symm ≪≫
              ((α_ (inclusionObj x.as) X✝ Y✝).symm ≪≫
                    (normalizeIsoApp C X✝ x ⊗ Iso.refl Y✝) ≪≫ normalizeIsoApp C Y✝ (normalizeObj X✝ x.as) ⊗
                  Iso.refl Z✝) ≪≫
                normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ x.as).as)).hom
        n =
    NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X✝ (Y✝ ⊗ Z✝)).symm ≪≫
              (normalizeIsoApp C X✝ x ⊗ Iso.refl (Y✝ ⊗ Z✝)) ≪≫
                (α_ (inclusionObj (normalizeObj X✝ x.as).as) Y✝ Z✝).symm ≪≫
                  (normalizeIsoApp C Y✝ (normalizeObj X✝ x.as) ⊗ Iso.refl Z✝) ≪≫
                    normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ x.as).as)).hom
        n ≫
      NatTrans.app
        (((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x =>
            𝟙 ((Discrete.functor fun x => normalizeObj Z✝ (normalizeObj Y✝ (normalizeObj X✝ x).as).as).obj x)))
        n
[PROOFSTEP]
dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
[GOAL]
case f.α_inv.w.h
C : Type u
X Y X✝ Y✝ Z✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (α_ X✝ Y✝ Z✝).inv) ≫
      (α_ (inclusionObj n.as) (X✝ ⊗ Y✝) Z✝).inv ≫
        ((α_ (inclusionObj n.as) X✝ Y✝).inv ≫
              ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 Y✝) ≫ (normalizeIsoApp C Y✝ (normalizeObj X✝ n.as)).hom ⊗
            𝟙 Z✝) ≫
          (normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ n.as).as)).hom =
    ((α_ (inclusionObj n.as) X✝ (Y✝ ⊗ Z✝)).inv ≫
        ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 (Y✝ ⊗ Z✝)) ≫
          (α_ (inclusionObj (normalizeObj X✝ n.as).as) Y✝ Z✝).inv ≫
            ((normalizeIsoApp C Y✝ (normalizeObj X✝ n.as)).hom ⊗ 𝟙 Z✝) ≫
              (normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ n.as).as)).hom) ≫
      𝟙
        (inclusionObj
          ((Discrete.functor fun x => normalizeObj Z✝ (normalizeObj Y✝ (normalizeObj X✝ x).as).as).obj n).as)
[PROOFSTEP]
simp only [Category.assoc, comp_tensor_id, tensor_id, Category.comp_id, pentagon_inv_assoc, ←
  associator_inv_naturality_assoc]
[GOAL]
case f.α_inv.w.h
C : Type u
X Y X✝ Y✝ Z✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusionObj n.as) X✝ (Y✝ ⊗ Z✝)).inv ≫
      ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 (Y✝ ⊗ Z✝)) ≫
        (α_ (inclusionObj ((Discrete.functor (normalizeObj X✝)).obj n).as) Y✝ Z✝).inv ≫
          ((normalizeIsoApp C Y✝ (normalizeObj X✝ n.as)).hom ⊗ 𝟙 Z✝) ≫
            (normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ n.as).as)).hom =
    (α_ (inclusionObj n.as) X✝ (Y✝ ⊗ Z✝)).inv ≫
      ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 (Y✝ ⊗ Z✝)) ≫
        (α_ (inclusionObj (normalizeObj X✝ n.as).as) Y✝ Z✝).inv ≫
          ((normalizeIsoApp C Y✝ (normalizeObj X✝ n.as)).hom ⊗ 𝟙 Z✝) ≫
            (normalizeIsoApp C Z✝ (normalizeObj Y✝ (normalizeObj X✝ n.as).as)).hom
[PROOFSTEP]
rfl
[GOAL]
case f.l_hom
C : Type u
X Y X✝ : F C
⊢ (tensorFunc C).map (Quotient.mk (setoidHom (tensor Unit X✝) X✝) (Hom.l_hom X✝)) ≫ (normalizeIsoAux C X✝).hom =
    (normalizeIsoAux C (tensor Unit X✝)).hom ≫
      (normalize' C).map (Quotient.mk (setoidHom (tensor Unit X✝) X✝) (Hom.l_hom X✝))
[PROOFSTEP]
ext n
[GOAL]
case f.l_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom (tensor Unit X✝) X✝) (Hom.l_hom X✝)) ≫ (normalizeIsoAux C X✝).hom) n =
    NatTrans.app
      ((normalizeIsoAux C (tensor Unit X✝)).hom ≫
        (normalize' C).map (Quotient.mk (setoidHom (tensor Unit X✝) X✝) (Hom.l_hom X✝)))
      n
[PROOFSTEP]
dsimp [Functor.comp]
[GOAL]
case f.l_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ Quotient.mk (setoidHom (𝟙_ (F C) ⊗ X✝) X✝) (Hom.l_hom X✝)) ≫
        (NatIso.ofComponents (normalizeIsoApp C X✝)).hom)
      n =
    NatTrans.app
      ((NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (𝟙_ (F C)) X✝).symm ≪≫
              (ρ_ (inclusionObj x.as) ⊗ Iso.refl X✝) ≪≫ normalizeIsoApp C X✝ { as := x.as }).hom ≫
        ((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor fun x => normalizeObj X✝ x).obj x)))
      n
[PROOFSTEP]
rw [mk_l_hom, NatTrans.comp_app, NatTrans.comp_app]
[GOAL]
case f.l_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app (Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ (λ_ X✝).hom) n ≫
      NatTrans.app (NatIso.ofComponents (normalizeIsoApp C X✝)).hom n =
    NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (𝟙_ (F C)) X✝).symm ≪≫
              (ρ_ (inclusionObj x.as) ⊗ Iso.refl X✝) ≪≫ normalizeIsoApp C X✝ { as := x.as }).hom
        n ≫
      NatTrans.app
        (((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor fun x => normalizeObj X✝ x).obj x)))
        n
[PROOFSTEP]
dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
[GOAL]
case f.l_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (λ_ X✝).hom) ≫ (normalizeIsoApp C X✝ n).hom =
    ((α_ (inclusionObj n.as) (𝟙_ (F C)) X✝).inv ≫
        ((ρ_ (inclusionObj n.as)).hom ⊗ 𝟙 X✝) ≫ (normalizeIsoApp C X✝ { as := n.as }).hom) ≫
      𝟙 (inclusionObj ((Discrete.functor fun x => normalizeObj X✝ x).obj n).as)
[PROOFSTEP]
simp only [triangle_assoc_comp_right_assoc, Category.assoc, Category.comp_id]
[GOAL]
case f.l_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (λ_ X✝).hom) ≫ (normalizeIsoApp C X✝ n).hom =
    (𝟙 (inclusionObj n.as) ⊗ (λ_ X✝).hom) ≫ (normalizeIsoApp C X✝ { as := n.as }).hom
[PROOFSTEP]
rfl
[GOAL]
case f.l_inv
C : Type u
X Y X✝ : F C
⊢ (tensorFunc C).map (Quotient.mk (setoidHom X✝ (tensor Unit X✝)) (Hom.l_inv X✝)) ≫
      (normalizeIsoAux C (tensor Unit X✝)).hom =
    (normalizeIsoAux C X✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X✝ (tensor Unit X✝)) (Hom.l_inv X✝))
[PROOFSTEP]
ext n
[GOAL]
case f.l_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom X✝ (tensor Unit X✝)) (Hom.l_inv X✝)) ≫
        (normalizeIsoAux C (tensor Unit X✝)).hom)
      n =
    NatTrans.app
      ((normalizeIsoAux C X✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X✝ (tensor Unit X✝)) (Hom.l_inv X✝))) n
[PROOFSTEP]
dsimp [Functor.comp]
[GOAL]
case f.l_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ Quotient.mk (setoidHom X✝ (𝟙_ (F C) ⊗ X✝)) (Hom.l_inv X✝)) ≫
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (𝟙_ (F C)) X✝).symm ≪≫
              (ρ_ (inclusionObj x.as) ⊗ Iso.refl X✝) ≪≫ normalizeIsoApp C X✝ { as := x.as }).hom)
      n =
    NatTrans.app
      ((NatIso.ofComponents (normalizeIsoApp C X✝)).hom ≫
        ((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor (normalizeObj X✝)).obj x)))
      n
[PROOFSTEP]
rw [mk_l_inv, NatTrans.comp_app, NatTrans.comp_app]
[GOAL]
case f.l_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app (Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ (λ_ X✝).inv) n ≫
      NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) (𝟙_ (F C)) X✝).symm ≪≫
              (ρ_ (inclusionObj x.as) ⊗ Iso.refl X✝) ≪≫ normalizeIsoApp C X✝ { as := x.as }).hom
        n =
    NatTrans.app (NatIso.ofComponents (normalizeIsoApp C X✝)).hom n ≫
      NatTrans.app
        (((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor (normalizeObj X✝)).obj x)))
        n
[PROOFSTEP]
dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
[GOAL]
case f.l_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (λ_ X✝).inv) ≫
      (α_ (inclusionObj n.as) (𝟙_ (F C)) X✝).inv ≫
        ((ρ_ (inclusionObj n.as)).hom ⊗ 𝟙 X✝) ≫ (normalizeIsoApp C X✝ { as := n.as }).hom =
    (normalizeIsoApp C X✝ n).hom ≫ 𝟙 (inclusionObj ((Discrete.functor (normalizeObj X✝)).obj n).as)
[PROOFSTEP]
simp only [triangle_assoc_comp_left_inv_assoc, inv_hom_id_tensor_assoc, tensor_id, Category.id_comp, Category.comp_id]
[GOAL]
case f.l_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (normalizeIsoApp C X✝ { as := n.as }).hom = (normalizeIsoApp C X✝ n).hom
[PROOFSTEP]
rfl
[GOAL]
case f.ρ_hom
C : Type u
X Y X✝ : F C
⊢ (tensorFunc C).map (Quotient.mk (setoidHom (tensor X✝ Unit) X✝) (Hom.ρ_hom X✝)) ≫ (normalizeIsoAux C X✝).hom =
    (normalizeIsoAux C (tensor X✝ Unit)).hom ≫
      (normalize' C).map (Quotient.mk (setoidHom (tensor X✝ Unit) X✝) (Hom.ρ_hom X✝))
[PROOFSTEP]
ext n
[GOAL]
case f.ρ_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom (tensor X✝ Unit) X✝) (Hom.ρ_hom X✝)) ≫ (normalizeIsoAux C X✝).hom) n =
    NatTrans.app
      ((normalizeIsoAux C (tensor X✝ Unit)).hom ≫
        (normalize' C).map (Quotient.mk (setoidHom (tensor X✝ Unit) X✝) (Hom.ρ_hom X✝)))
      n
[PROOFSTEP]
dsimp
[GOAL]
case f.ρ_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ Quotient.mk (setoidHom (X✝ ⊗ 𝟙_ (F C)) X✝) (Hom.ρ_hom X✝)) ≫
        (NatIso.ofComponents (normalizeIsoApp C X✝)).hom)
      n =
    NatTrans.app
      ((NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X✝ (𝟙_ (F C))).symm ≪≫
              (normalizeIsoApp C X✝ x ⊗ Iso.refl (𝟙_ (F C))) ≪≫ ρ_ (inclusionObj (normalizeObj X✝ x.as).as)).hom ≫
        ((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor fun x => { as := (normalizeObj X✝ x).as }).obj x)))
      n
[PROOFSTEP]
rw [mk_ρ_hom, NatTrans.comp_app, NatTrans.comp_app]
[GOAL]
case f.ρ_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app (Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ (ρ_ X✝).hom) n ≫
      NatTrans.app (NatIso.ofComponents (normalizeIsoApp C X✝)).hom n =
    NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X✝ (𝟙_ (F C))).symm ≪≫
              (normalizeIsoApp C X✝ x ⊗ Iso.refl (𝟙_ (F C))) ≪≫ ρ_ (inclusionObj (normalizeObj X✝ x.as).as)).hom
        n ≫
      NatTrans.app
        (((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor fun x => { as := (normalizeObj X✝ x).as }).obj x)))
        n
[PROOFSTEP]
dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
[GOAL]
case f.ρ_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (ρ_ X✝).hom) ≫ (normalizeIsoApp C X✝ n).hom =
    ((α_ (inclusionObj n.as) X✝ (𝟙_ (F C))).inv ≫
        ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 (𝟙_ (F C))) ≫ (ρ_ (inclusionObj (normalizeObj X✝ n.as).as)).hom) ≫
      𝟙 (inclusionObj ((Discrete.functor fun x => { as := (normalizeObj X✝ x).as }).obj n).as)
[PROOFSTEP]
simp only [← (Iso.inv_comp_eq _).2 (rightUnitor_tensor _ _), Category.assoc, ← rightUnitor_naturality, Category.comp_id]
[GOAL]
case f.ρ_hom.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusionObj n.as) X✝ (𝟙_ (F C))).inv ≫
      ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 tensorUnit') ≫
        (ρ_ (inclusionObj ((Discrete.functor (normalizeObj X✝)).obj n).as)).hom =
    (α_ (inclusionObj n.as) X✝ (𝟙_ (F C))).inv ≫
      ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 (𝟙_ (F C))) ≫ (ρ_ (inclusionObj (normalizeObj X✝ n.as).as)).hom
[PROOFSTEP]
rfl
[GOAL]
case f.ρ_inv
C : Type u
X Y X✝ : F C
⊢ (tensorFunc C).map (Quotient.mk (setoidHom X✝ (tensor X✝ Unit)) (Hom.ρ_inv X✝)) ≫
      (normalizeIsoAux C (tensor X✝ Unit)).hom =
    (normalizeIsoAux C X✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X✝ (tensor X✝ Unit)) (Hom.ρ_inv X✝))
[PROOFSTEP]
ext n
[GOAL]
case f.ρ_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom X✝ (tensor X✝ Unit)) (Hom.ρ_inv X✝)) ≫
        (normalizeIsoAux C (tensor X✝ Unit)).hom)
      n =
    NatTrans.app
      ((normalizeIsoAux C X✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X✝ (tensor X✝ Unit)) (Hom.ρ_inv X✝))) n
[PROOFSTEP]
dsimp
[GOAL]
case f.ρ_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app
      ((Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ Quotient.mk (setoidHom X✝ (X✝ ⊗ 𝟙_ (F C))) (Hom.ρ_inv X✝)) ≫
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X✝ (𝟙_ (F C))).symm ≪≫
              (normalizeIsoApp C X✝ x ⊗ Iso.refl (𝟙_ (F C))) ≪≫ ρ_ (inclusionObj (normalizeObj X✝ x.as).as)).hom)
      n =
    NatTrans.app
      ((NatIso.ofComponents (normalizeIsoApp C X✝)).hom ≫
        ((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor (normalizeObj X✝)).obj x)))
      n
[PROOFSTEP]
rw [mk_ρ_inv, NatTrans.comp_app, NatTrans.comp_app]
[GOAL]
case f.ρ_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ NatTrans.app (Discrete.natTrans fun n => 𝟙 (inclusionObj n.as) ⊗ (ρ_ X✝).inv) n ≫
      NatTrans.app
        (NatIso.ofComponents fun x =>
            (α_ (inclusionObj x.as) X✝ (𝟙_ (F C))).symm ≪≫
              (normalizeIsoApp C X✝ x ⊗ Iso.refl (𝟙_ (F C))) ≪≫ ρ_ (inclusionObj (normalizeObj X✝ x.as).as)).hom
        n =
    NatTrans.app (NatIso.ofComponents (normalizeIsoApp C X✝)).hom n ≫
      NatTrans.app
        (((whiskeringRight (Discrete (NormalMonoidalObject C)) (Discrete (NormalMonoidalObject C)) (F C)).obj
              (Discrete.functor inclusionObj)).map
          (Discrete.natTrans fun x => 𝟙 ((Discrete.functor (normalizeObj X✝)).obj x)))
        n
[PROOFSTEP]
dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
[GOAL]
case f.ρ_inv.w.h
C : Type u
X Y X✝ : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (𝟙 (inclusionObj n.as) ⊗ (ρ_ X✝).inv) ≫
      (α_ (inclusionObj n.as) X✝ (𝟙_ (F C))).inv ≫
        ((normalizeIsoApp C X✝ n).hom ⊗ 𝟙 (𝟙_ (F C))) ≫ (ρ_ (inclusionObj (normalizeObj X✝ n.as).as)).hom =
    (normalizeIsoApp C X✝ n).hom ≫ 𝟙 (inclusionObj ((Discrete.functor (normalizeObj X✝)).obj n).as)
[PROOFSTEP]
simp only [← (Iso.eq_comp_inv _).1 (rightUnitor_tensor_inv _ _), rightUnitor_conjugation, Category.assoc,
  Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, Iso.inv_hom_id, Discrete.functor, Category.comp_id, Function.comp]
[GOAL]
case f.comp
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
h₁ :
  (tensorFunc C).map (Quotient.mk (setoidHom X✝ Y✝) f✝) ≫ (normalizeIsoAux C Y✝).hom =
    (normalizeIsoAux C X✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X✝ Y✝) f✝)
h₂ :
  (tensorFunc C).map (Quotient.mk (setoidHom Y✝ Z✝) g✝) ≫ (normalizeIsoAux C Z✝).hom =
    (normalizeIsoAux C Y✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom Y✝ Z✝) g✝)
⊢ (tensorFunc C).map (Quotient.mk (setoidHom X✝ Z✝) (Hom.comp f✝ g✝)) ≫ (normalizeIsoAux C Z✝).hom =
    (normalizeIsoAux C X✝).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X✝ Z✝) (Hom.comp f✝ g✝))
[PROOFSTEP]
rw [mk_comp, Functor.map_comp, Functor.map_comp, Category.assoc, h₂, reassoc_of% h₁]
[GOAL]
case f.tensor
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
h₁ :
  (tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom =
    (normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)
h₂ :
  (tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom =
    (normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g)
⊢ (tensorFunc C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)) ≫
      (normalizeIsoAux C (tensor Y₁ Y₂)).hom =
    (normalizeIsoAux C (tensor X₁ X₂)).hom ≫
      (normalize' C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g))
[PROOFSTEP]
ext ⟨n⟩
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
h₁ :
  (tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom =
    (normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)
h₂ :
  (tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom =
    (normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g)
n : NormalMonoidalObject C
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)) ≫
        (normalizeIsoAux C (tensor Y₁ Y₂)).hom)
      { as := n } =
    NatTrans.app
      ((normalizeIsoAux C (tensor X₁ X₂)).hom ≫
        (normalize' C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)))
      { as := n }
[PROOFSTEP]
replace h₁ := NatTrans.congr_app h₁ ⟨n⟩
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
h₂ :
  (tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom =
    (normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g)
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)) ≫
        (normalizeIsoAux C (tensor Y₁ Y₂)).hom)
      { as := n } =
    NatTrans.app
      ((normalizeIsoAux C (tensor X₁ X₂)).hom ≫
        (normalize' C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)))
      { as := n }
[PROOFSTEP]
replace h₂ := NatTrans.congr_app h₂ ((Discrete.functor (normalizeObj X₁)).obj ⟨n⟩)
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom)
      ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app ((normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
      ((Discrete.functor (normalizeObj X₁)).obj { as := n })
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)) ≫
        (normalizeIsoAux C (tensor Y₁ Y₂)).hom)
      { as := n } =
    NatTrans.app
      ((normalizeIsoAux C (tensor X₁ X₂)).hom ≫
        (normalize' C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)))
      { as := n }
[PROOFSTEP]
have h₃ := (normalizeIsoAux _ Y₂).hom.naturality ((normalizeMapAux f).app ⟨n⟩)
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom)
      ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app ((normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
      ((Discrete.functor (normalizeObj X₁)).obj { as := n })
h₃ :
  ((tensorFunc C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj Y₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      ((normalize' C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)) ≫
        (normalizeIsoAux C (tensor Y₁ Y₂)).hom)
      { as := n } =
    NatTrans.app
      ((normalizeIsoAux C (tensor X₁ X₂)).hom ≫
        (normalize' C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)))
      { as := n }
[PROOFSTEP]
have h₄ :
  ∀ (X₃ Y₃ : N C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n ↦ inclusionObj n ⊗ Y₂).map φ :=
  by
  rintro ⟨X₃⟩ ⟨Y₃⟩ φ
  obtain rfl : X₃ = Y₃ := φ.1.1
  simp only [discrete_functor_map_eq_id, tensor_id]
  rfl
[GOAL]
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom)
      ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app ((normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
      ((Discrete.functor (normalizeObj X₁)).obj { as := n })
h₃ :
  ((tensorFunc C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj Y₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      ((normalize' C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })
⊢ ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
[PROOFSTEP]
rintro ⟨X₃⟩ ⟨Y₃⟩ φ
[GOAL]
case mk.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom)
      ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app ((normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
      ((Discrete.functor (normalizeObj X₁)).obj { as := n })
h₃ :
  ((tensorFunc C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj Y₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      ((normalize' C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })
X₃ Y₃ : NormalMonoidalObject C
φ : { as := X₃ } ⟶ { as := Y₃ }
⊢ (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
[PROOFSTEP]
obtain rfl : X₃ = Y₃ := φ.1.1
[GOAL]
case mk.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom)
      ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app ((normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
      ((Discrete.functor (normalizeObj X₁)).obj { as := n })
h₃ :
  ((tensorFunc C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj Y₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      ((normalize' C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })
X₃ : NormalMonoidalObject C
φ : { as := X₃ } ⟶ { as := X₃ }
⊢ (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
[PROOFSTEP]
simp only [discrete_functor_map_eq_id, tensor_id]
[GOAL]
case mk.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom)
      ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app ((normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
      ((Discrete.functor (normalizeObj X₁)).obj { as := n })
h₃ :
  ((tensorFunc C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj Y₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      ((normalize' C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })
X₃ : NormalMonoidalObject C
φ : { as := X₃ } ⟶ { as := X₃ }
⊢ 𝟙 ((Discrete.functor inclusionObj).obj { as := X₃ } ⊗ Y₂) =
    𝟙 ((Discrete.functor fun n => inclusionObj n ⊗ Y₂).obj { as := X₃ })
[PROOFSTEP]
rfl
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoAux C Y₁).hom) { as := n } =
    NatTrans.app ((normalizeIsoAux C X₁).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g) ≫ (normalizeIsoAux C Y₂).hom)
      ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app ((normalizeIsoAux C X₂).hom ≫ (normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
      ((Discrete.functor (normalizeObj X₁)).obj { as := n })
h₃ :
  ((tensorFunc C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj Y₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      ((normalize' C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })
h₄ :
  ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
⊢ NatTrans.app
      ((tensorFunc C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)) ≫
        (normalizeIsoAux C (tensor Y₁ Y₂)).hom)
      { as := n } =
    NatTrans.app
      ((normalizeIsoAux C (tensor X₁ X₂)).hom ≫
        (normalize' C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)))
      { as := n }
[PROOFSTEP]
rw [NatTrans.comp_app, NatTrans.comp_app] at h₁ h₂ ⊢
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n } ≫
      NatTrans.app (normalizeIsoAux C Y₁).hom { as := n } =
    NatTrans.app (normalizeIsoAux C X₁).hom { as := n } ≫
      NatTrans.app ((normalize' C).map (Quotient.mk (setoidHom X₁ Y₁) f)) { as := n }
h₂ :
  NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom X₂ Y₂) g))
        ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C X₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      NatTrans.app ((normalize' C).map (Quotient.mk (setoidHom X₂ Y₂) g))
        ((Discrete.functor (normalizeObj X₁)).obj { as := n })
h₃ :
  ((tensorFunc C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj Y₁)).obj { as := n }) =
    NatTrans.app (normalizeIsoAux C Y₂).hom ((Discrete.functor (normalizeObj X₁)).obj { as := n }) ≫
      ((normalize' C).obj Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })
h₄ :
  ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
⊢ NatTrans.app ((tensorFunc C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)))
        { as := n } ≫
      NatTrans.app (normalizeIsoAux C (tensor Y₁ Y₂)).hom { as := n } =
    NatTrans.app (normalizeIsoAux C (tensor X₁ X₂)).hom { as := n } ≫
      NatTrans.app ((normalize' C).map (Quotient.mk (setoidHom (tensor X₁ X₂) (tensor Y₁ Y₂)) (Hom.tensor f g)))
        { as := n }
[PROOFSTEP]
dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp, Discrete.natTrans] at h₁ h₂ h₃
  ⊢
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  (𝟙 (inclusionObj n) ⊗ Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoApp C Y₁ { as := n }).hom =
    (normalizeIsoApp C X₁ { as := n }).hom ≫
      (Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n })
h₂ :
  (𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom =
    (normalizeIsoApp C X₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        (NatTrans.app (normalizeMapAux g) ((Discrete.functor (normalizeObj X₁)).obj { as := n }))
h₃ :
  (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj Y₁)).obj { as := n })).hom =
    (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
h₄ :
  ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
⊢ (𝟙 (inclusionObj n) ⊗ Quotient.mk (setoidHom (X₁ ⊗ X₂) (Y₁ ⊗ Y₂)) (Hom.tensor f g)) ≫
      (α_ (inclusionObj n) Y₁ Y₂).inv ≫
        ((normalizeIsoApp C Y₁ { as := n }).hom ⊗ 𝟙 Y₂) ≫ (normalizeIsoApp C Y₂ (normalizeObj Y₁ n)).hom =
    ((α_ (inclusionObj n) X₁ X₂).inv ≫
        ((normalizeIsoApp C X₁ { as := n }).hom ⊗ 𝟙 X₂) ≫ (normalizeIsoApp C X₂ (normalizeObj X₁ n)).hom) ≫
      (Discrete.functor inclusionObj).map
        (NatTrans.app (normalizeMapAux g) (normalizeObj X₁ n) ≫
          (Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
[PROOFSTEP]
rw [mk_tensor, associator_inv_naturality_assoc, ← tensor_comp_assoc, h₁, Category.assoc, Category.comp_id, ←
  @Category.id_comp (F C) _ _ _ (@Quotient.mk _ _ g), tensor_comp, Category.assoc, Category.assoc, Functor.map_comp]
[GOAL]
case f.tensor.w.h.mk
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  (𝟙 (inclusionObj n) ⊗ Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoApp C Y₁ { as := n }).hom =
    (normalizeIsoApp C X₁ { as := n }).hom ≫
      (Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n })
h₂ :
  (𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom =
    (normalizeIsoApp C X₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        (NatTrans.app (normalizeMapAux g) ((Discrete.functor (normalizeObj X₁)).obj { as := n }))
h₃ :
  (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj Y₁)).obj { as := n })).hom =
    (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
h₄ :
  ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
⊢ (α_ (inclusionObj n) X₁ X₂).inv ≫
      ((normalizeIsoApp C X₁ { as := n }).hom ⊗ 𝟙 X₂) ≫
        ((Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n }) ⊗
            Quotient.mk (setoidHom X₂ Y₂) g) ≫
          (normalizeIsoApp C Y₂ (normalizeObj Y₁ n)).hom =
    (α_ (inclusionObj n) X₁ X₂).inv ≫
      ((normalizeIsoApp C X₁ { as := n }).hom ⊗ 𝟙 X₂) ≫
        (normalizeIsoApp C X₂ (normalizeObj X₁ n)).hom ≫
          (Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux g) (normalizeObj X₁ n)) ≫
            (Discrete.functor inclusionObj).map
              ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
[PROOFSTEP]
congr 2
[GOAL]
case f.tensor.w.h.mk.e_a.e_a
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  (𝟙 (inclusionObj n) ⊗ Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoApp C Y₁ { as := n }).hom =
    (normalizeIsoApp C X₁ { as := n }).hom ≫
      (Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n })
h₂ :
  (𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom =
    (normalizeIsoApp C X₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        (NatTrans.app (normalizeMapAux g) ((Discrete.functor (normalizeObj X₁)).obj { as := n }))
h₃ :
  (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj Y₁)).obj { as := n })).hom =
    (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
h₄ :
  ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
⊢ ((Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n }) ⊗
        Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ (normalizeObj Y₁ n)).hom =
    (normalizeIsoApp C X₂ (normalizeObj X₁ n)).hom ≫
      (Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux g) (normalizeObj X₁ n)) ≫
        (Discrete.functor inclusionObj).map
          ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
[PROOFSTEP]
erw [← reassoc_of% h₂]
[GOAL]
case f.tensor.w.h.mk.e_a.e_a
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  (𝟙 (inclusionObj n) ⊗ Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoApp C Y₁ { as := n }).hom =
    (normalizeIsoApp C X₁ { as := n }).hom ≫
      (Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n })
h₂ :
  (𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom =
    (normalizeIsoApp C X₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        (NatTrans.app (normalizeMapAux g) ((Discrete.functor (normalizeObj X₁)).obj { as := n }))
h₃ :
  (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj Y₁)).obj { as := n })).hom =
    (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
h₄ :
  ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
⊢ ((Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n }) ⊗
        Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ (normalizeObj Y₁ n)).hom =
    (𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
        (Discrete.functor inclusionObj).map
          ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
[PROOFSTEP]
rw [← h₃, ← Category.assoc, ← id_tensor_comp_tensor_id, h₄]
[GOAL]
case f.tensor.w.h.mk.e_a.e_a
C : Type u
X Y X₁ X₂ Y₁ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
n : NormalMonoidalObject C
h₁ :
  (𝟙 (inclusionObj n) ⊗ Quotient.mk (setoidHom X₁ Y₁) f) ≫ (normalizeIsoApp C Y₁ { as := n }).hom =
    (normalizeIsoApp C X₁ { as := n }).hom ≫
      (Discrete.functor inclusionObj).map (NatTrans.app (normalizeMapAux f) { as := n })
h₂ :
  (𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom =
    (normalizeIsoApp C X₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        (NatTrans.app (normalizeMapAux g) ((Discrete.functor (normalizeObj X₁)).obj { as := n }))
h₃ :
  (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map (NatTrans.app (normalizeMapAux f) { as := n }) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj Y₁)).obj { as := n })).hom =
    (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj X₁)).obj { as := n })).hom ≫
      (Discrete.functor inclusionObj).map
        ((Discrete.functor (normalizeObj Y₂)).map (NatTrans.app (normalizeMapAux f) { as := n }))
h₄ :
  ∀ (X₃ Y₃ : (Discrete ∘ NormalMonoidalObject) C) (φ : X₃ ⟶ Y₃),
    (Discrete.functor inclusionObj).map φ ⊗ 𝟙 Y₂ = (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map φ
⊢ ((𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
        (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })) ≫
      (normalizeIsoApp C Y₂ (normalizeObj Y₁ n)).hom =
    ((𝟙 (inclusionObj ((Discrete.functor (normalizeObj X₁)).obj { as := n }).as) ⊗ Quotient.mk (setoidHom X₂ Y₂) g) ≫
        (Discrete.functor fun n => inclusionObj n ⊗ Y₂).map (NatTrans.app (normalizeMapAux f) { as := n })) ≫
      (normalizeIsoApp C Y₂ ((Discrete.functor (normalizeObj Y₁)).obj { as := n })).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
⊢ ∀ {X Y : F C} (f : X ⟶ Y),
    (𝟭 (F C)).map f ≫
        ((fun X => (λ_ X).symm ≪≫ ((normalizeIso C).app X).app { as := NormalMonoidalObject.Unit }) Y).hom =
      ((fun X => (λ_ X).symm ≪≫ ((normalizeIso C).app X).app { as := NormalMonoidalObject.Unit }) X).hom ≫
        (fullNormalize C ⋙ inclusion).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u
X Y : F C
f : X ⟶ Y
⊢ (𝟭 (F C)).map f ≫ ((fun X => (λ_ X).symm ≪≫ ((normalizeIso C).app X).app { as := NormalMonoidalObject.Unit }) Y).hom =
    ((fun X => (λ_ X).symm ≪≫ ((normalizeIso C).app X).app { as := NormalMonoidalObject.Unit }) X).hom ≫
      (fullNormalize C ⋙ inclusion).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
X Y : F C
f : X ⟶ Y
⊢ f ≫ (λ_ Y).inv ≫ (((normalizeIso C).app Y).app { as := NormalMonoidalObject.Unit }).hom =
    ((λ_ X).inv ≫ (((normalizeIso C).app X).app { as := NormalMonoidalObject.Unit }).hom) ≫
      (fullNormalize C ⋙ Discrete.functor inclusionObj).map f
[PROOFSTEP]
rw [leftUnitor_inv_naturality_assoc, Category.assoc, Iso.cancel_iso_inv_left]
[GOAL]
C : Type u
X Y : F C
f : X ⟶ Y
⊢ (𝟙 tensorUnit' ⊗ f) ≫ (((normalizeIso C).app Y).app { as := NormalMonoidalObject.Unit }).hom =
    (((normalizeIso C).app X).app { as := NormalMonoidalObject.Unit }).hom ≫
      (fullNormalize C ⋙ Discrete.functor inclusionObj).map f
[PROOFSTEP]
exact
  congr_arg (fun f => NatTrans.app f (Discrete.mk NormalMonoidalObject.Unit)) ((normalizeIso.{u} C).hom.naturality f)
[GOAL]
C : Type u
X Y : F C
f g : X ⟶ Y
⊢ f = g
[PROOFSTEP]
have hfg : (fullNormalize C).map f = (fullNormalize C).map g := Subsingleton.elim _ _
[GOAL]
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
⊢ f = g
[PROOFSTEP]
have hf := NatIso.naturality_2 (fullNormalizeIso.{u} C) f
[GOAL]
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  NatTrans.app (fullNormalizeIso C).hom X ≫
      (fullNormalize C ⋙ inclusion).map f ≫ NatTrans.app (fullNormalizeIso C).inv Y =
    (𝟭 (F C)).map f
⊢ f = g
[PROOFSTEP]
have hg := NatIso.naturality_2 (fullNormalizeIso.{u} C) g
[GOAL]
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  NatTrans.app (fullNormalizeIso C).hom X ≫
      (fullNormalize C ⋙ inclusion).map f ≫ NatTrans.app (fullNormalizeIso C).inv Y =
    (𝟭 (F C)).map f
hg :
  NatTrans.app (fullNormalizeIso C).hom X ≫
      (fullNormalize C ⋙ inclusion).map g ≫ NatTrans.app (fullNormalizeIso C).inv Y =
    (𝟭 (F C)).map g
⊢ f = g
[PROOFSTEP]
exact hf.symm.trans (Eq.trans (by simp only [Functor.comp_map, hfg]) hg)
[GOAL]
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  NatTrans.app (fullNormalizeIso C).hom X ≫
      (fullNormalize C ⋙ inclusion).map f ≫ NatTrans.app (fullNormalizeIso C).inv Y =
    (𝟭 (F C)).map f
hg :
  NatTrans.app (fullNormalizeIso C).hom X ≫
      (fullNormalize C ⋙ inclusion).map g ≫ NatTrans.app (fullNormalizeIso C).inv Y =
    (𝟭 (F C)).map g
⊢ NatTrans.app (fullNormalizeIso C).hom X ≫
      (fullNormalize C ⋙ inclusion).map f ≫ NatTrans.app (fullNormalizeIso C).inv Y =
    NatTrans.app (fullNormalizeIso C).hom X ≫
      (fullNormalize C ⋙ inclusion).map g ≫ NatTrans.app (fullNormalizeIso C).inv Y
[PROOFSTEP]
simp only [Functor.comp_map, hfg]
[GOAL]
C : Type u
src✝ : Category.{u, u} (F C) := inferInstance
X✝ Y✝ : F C
⊢ ∀ (a b : X✝ ⟶ᵐ Y✝),
    a ≈ b →
      (fun f => Quotient.mk (setoidHom Y✝ X✝) (inverseAux f)) a =
        (fun f => Quotient.mk (setoidHom Y✝ X✝) (inverseAux f)) b
[PROOFSTEP]
aesop_cat