[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limit F)).map f ≫ (fun j => Hom.mk (limit.π (F ⋙ forget C) j)) j' =
    (fun j => Hom.mk (limit.π (F ⋙ forget C) j)) j ≫ F.map f
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
j j' : J
f : j ⟶ j'
⊢ (((Functor.const J).obj (limit F)).map f ≫ (fun j => Hom.mk (limit.π (F ⋙ forget C) j)) j').hom =
    ((fun j => Hom.mk (limit.π (F ⋙ forget C) j)) j ≫ F.map f).hom
[PROOFSTEP]
exact (limit.cone (F ⋙ Mon_.forget C)).π.naturality f
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
⊢ ∀ (j : J),
    NatTrans.app ((forget C).mapCone (limitCone F)).π j =
      (Iso.refl ((forget C).mapCone (limitCone F)).pt).hom ≫ NatTrans.app (limit.cone (F ⋙ forget C)).π j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
⊢ s.pt.mul ≫ limit.lift (F ⋙ forget C) ((forget C).mapCone s) =
    MonoidalCategory.tensorHom (limit.lift (F ⋙ forget C) ((forget C).mapCone s))
        (limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫
      (limitCone F).pt.mul
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
⊢ s.pt.mul ≫ limit.lift (F ⋙ forget C) ((forget C).mapCone s) =
    MonoidalCategory.tensorHom (limit.lift (F ⋙ forget C) ((forget C).mapCone s))
        (limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫
      (limit F).mul
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
⊢ (s.pt.mul ≫ limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫ limit.π (F ⋙ forget C) j✝ =
    (MonoidalCategory.tensorHom (limit.lift (F ⋙ forget C) ((forget C).mapCone s))
          (limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫
        (limit F).mul) ≫
      limit.π (F ⋙ forget C) j✝
[PROOFSTEP]
simp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
⊢ MonoidalCategory.tensorHom (NatTrans.app s.π j✝).hom (NatTrans.app s.π j✝).hom ≫ (F.obj j✝).mul =
    MonoidalCategory.tensorHom (limit.lift (F ⋙ forget C) ((forget C).mapCone s))
        (limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫
      MonoidalCategory.tensorHom (limit.π (F ⋙ forget C) j✝) (limit.π (F ⋙ forget C) j✝) ≫ (F.obj j✝).mul
[PROOFSTEP]
slice_rhs 1 2 => rw [← MonoidalCategory.tensor_comp, limit.lift_π]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
| MonoidalCategory.tensorHom (limit.lift (F ⋙ forget C) ((forget C).mapCone s))
      (limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫
    MonoidalCategory.tensorHom (limit.π (F ⋙ forget C) j✝) (limit.π (F ⋙ forget C) j✝)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
| (F.obj j✝).mul
[PROOFSTEP]
rw [← MonoidalCategory.tensor_comp, limit.lift_π]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
| MonoidalCategory.tensorHom (limit.lift (F ⋙ forget C) ((forget C).mapCone s))
      (limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫
    MonoidalCategory.tensorHom (limit.π (F ⋙ forget C) j✝) (limit.π (F ⋙ forget C) j✝)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
| (F.obj j✝).mul
[PROOFSTEP]
rw [← MonoidalCategory.tensor_comp, limit.lift_π]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
| MonoidalCategory.tensorHom (limit.lift (F ⋙ forget C) ((forget C).mapCone s))
      (limit.lift (F ⋙ forget C) ((forget C).mapCone s)) ≫
    MonoidalCategory.tensorHom (limit.π (F ⋙ forget C) j✝) (limit.π (F ⋙ forget C) j✝)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
j✝ : J
| (F.obj j✝).mul
[PROOFSTEP]
rw [← MonoidalCategory.tensor_comp, limit.lift_π]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
h : J
⊢ (fun s => Hom.mk (limit.lift (F ⋙ forget C) ((forget C).mapCone s))) s ≫ NatTrans.app (limitCone F).π h =
    NatTrans.app s.π h
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
h : J
⊢ ((fun s => Hom.mk (limit.lift (F ⋙ forget C) ((forget C).mapCone s))) s ≫ NatTrans.app (limitCone F).π h).hom =
    (NatTrans.app s.π h).hom
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
⊢ m = (fun s => Hom.mk (limit.lift (F ⋙ forget C) ((forget C).mapCone s))) s
[PROOFSTEP]
ext1
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
⊢ m.hom = ((fun s => Hom.mk (limit.lift (F ⋙ forget C) ((forget C).mapCone s))) s).hom
[PROOFSTEP]
refine' limit.hom_ext (fun j => _)
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
j : J
⊢ m.hom ≫ limit.π (MonFunctorCategoryEquivalence.inverse.obj F).X j =
    ((fun s => Hom.mk (limit.lift (F ⋙ forget C) ((forget C).mapCone s))) s).hom ≫
      limit.π (MonFunctorCategoryEquivalence.inverse.obj F).X j
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
j : J
⊢ m.hom ≫ limit.π (F ⋙ forget C) j = limit.lift (F ⋙ forget C) ((forget C).mapCone s) ≫ limit.π (F ⋙ forget C) j
[PROOFSTEP]
simp only [Mon_.forget_map, limit.lift_π, Functor.mapCone_π_app]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F : J ⥤ Mon_ C
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
j : J
⊢ m.hom ≫ limit.π (F ⋙ forget C) j = (NatTrans.app s.π j).hom
[PROOFSTEP]
exact congr_arg Mon_.Hom.hom (w j)


[GOAL]
M : Type u
inst✝ : Monoid M
X x✝¹ x✝ : Discrete M
f : x✝¹ ⟶ x✝
⊢ (fun X Y => { as := X.as * Y.as }) X x✝¹ = (fun X Y => { as := X.as * Y.as }) X x✝
[PROOFSTEP]
dsimp
[GOAL]
M : Type u
inst✝ : Monoid M
X x✝¹ x✝ : Discrete M
f : x✝¹ ⟶ x✝
⊢ { as := X.as * x✝¹.as } = { as := X.as * x✝.as }
[PROOFSTEP]
rw [eq_of_hom f]
[GOAL]
M : Type u
inst✝ : Monoid M
X₁✝ X₂✝ : Discrete M
f : X₁✝ ⟶ X₂✝
X : Discrete M
⊢ (fun X Y => { as := X.as * Y.as }) X₁✝ X = (fun X Y => { as := X.as * Y.as }) X₂✝ X
[PROOFSTEP]
dsimp
[GOAL]
M : Type u
inst✝ : Monoid M
X₁✝ X₂✝ : Discrete M
f : X₁✝ ⟶ X₂✝
X : Discrete M
⊢ { as := X₁✝.as * X.as } = { as := X₂✝.as * X.as }
[PROOFSTEP]
rw [eq_of_hom f]
[GOAL]
M : Type u
inst✝ : Monoid M
X₁✝ Y₁✝ X₂✝ Y₂✝ : Discrete M
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
⊢ (fun X Y => { as := X.as * Y.as }) X₁✝ X₂✝ = (fun X Y => { as := X.as * Y.as }) Y₁✝ Y₂✝
[PROOFSTEP]
dsimp
[GOAL]
M : Type u
inst✝ : Monoid M
X₁✝ Y₁✝ X₂✝ Y₂✝ : Discrete M
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
⊢ { as := X₁✝.as * X₂✝.as } = { as := Y₁✝.as * Y₂✝.as }
[PROOFSTEP]
rw [eq_of_hom f, eq_of_hom g]