[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
j : J
⊢ Monoid ((F ⋙ forget MonCat).obj j)
[PROOFSTEP]
change Monoid (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
j : J
⊢ Monoid ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
a b : (j : J) → ↑(F.obj j)
ah : a ∈ Functor.sections (F ⋙ forget MonCat)
bh : b ∈ Functor.sections (F ⋙ forget MonCat)
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget MonCat).map f ((a * b) j) = (a * b) j'
[PROOFSTEP]
simp only [Functor.comp_map, MonoidHom.map_mul, Pi.mul_apply]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
a b : (j : J) → ↑(F.obj j)
ah : a ∈ Functor.sections (F ⋙ forget MonCat)
bh : b ∈ Functor.sections (F ⋙ forget MonCat)
j j' : J
f : j ⟶ j'
⊢ (forget MonCat).map (F.map f) (a j * b j) = a j' * b j'
[PROOFSTEP]
dsimp [Functor.sections] at ah bh 
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
a b : (j : J) → ↑(F.obj j)
ah : a ∈ {u | ∀ {j j' : J} (f : j ⟶ j'), ↑(F.map f) (u j) = u j'}
bh : b ∈ {u | ∀ {j j' : J} (f : j ⟶ j'), ↑(F.map f) (u j) = u j'}
j j' : J
f : j ⟶ j'
⊢ (forget MonCat).map (F.map f) (a j * b j) = a j' * b j'
[PROOFSTEP]
rw [← ah f, ← bh f, forget_map, map_mul]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget MonCat).map f (OfNat.ofNat 1 j) = OfNat.ofNat 1 j'
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
⊢ IsLimit (limitCone F)
[PROOFSTEP]
refine IsLimit.ofFaithful (forget MonCatMax) (Types.limitConeIsLimit.{v, u} _) (fun s => ⟨⟨_, ?_⟩, ?_⟩) (fun s => rfl)
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
s : Cone F
⊢ { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
      property :=
        (_ :
          ∀ {j j' : J} (f : j ⟶ j'),
            (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
              NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
    1
[PROOFSTEP]
aesop_cat
[GOAL]
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCatMax
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    OneHom.toFun
        {
          toFun := fun v =>
            { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j v,
              property :=
                (_ :
                  ∀ {j j' : J} (f : j ⟶ j'),
                    (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) v =
                      NatTrans.app ((forget MonCatMax).mapCone s).π j' v) },
          map_one' :=
            (_ :
              { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
                  property :=
                    (_ :
                      ∀ {j j' : J} (f : j ⟶ j'),
                        (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
                          NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
                1) }
        (x * y) =
      OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j v,
                property :=
                  (_ :
                    ∀ {j j' : J} (f : j ⟶ j'),
                      (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) v =
                        NatTrans.app ((forget MonCatMax).mapCone s).π j' v) },
            map_one' :=
              (_ :
                { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
                    property :=
                      (_ :
                        ∀ {j j' : J} (f : j ⟶ j'),
                          (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
                            NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
                  1) }
          x *
        OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j v,
                property :=
                  (_ :
                    ∀ {j j' : J} (f : j ⟶ j'),
                      (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) v =
                        NatTrans.app ((forget MonCatMax).mapCone s).π j' v) },
            map_one' :=
              (_ :
                { val := fun j => NatTrans.app ((forget MonCatMax).mapCone s).π j 1,
                    property :=
                      (_ :
                        ∀ {j j' : J} (f : j ⟶ j'),
                          (NatTrans.app ((forget MonCatMax).mapCone s).π j ≫ (F ⋙ forget MonCatMax).map f) 1 =
                            NatTrans.app ((forget MonCatMax).mapCone s).π j' 1) } =
                  1) }
          y
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommMonCatMax
j : J
⊢ CommMonoid ((F ⋙ forget CommMonCatMax).obj j)
[PROOFSTEP]
change CommMonoid (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommMonCatMax
j : J
⊢ CommMonoid ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommMonCatMax
c' : Cone (F ⋙ forget₂ CommMonCat MonCatMax)
t : IsLimit c'
⊢ (forget₂ CommMonCat MonCatMax).mapCone
      { pt := of (Types.limitCone (F ⋙ forget CommMonCat)).pt,
        π := NatTrans.mk (limitπMonoidHom (F ⋙ forget₂ CommMonCatMax MonCatMax)) } ≅
    c'
[PROOFSTEP]
apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit _) t
[GOAL]
J✝ : Type v
inst✝ : SmallCategory J✝
J : Type v
𝒥 : Category.{v, v} J
F : J ⥤ CommMonCatMax
⊢ PreservesLimit F (forget₂ CommMonCatMax MonCatMax)
[PROOFSTEP]
infer_instance
