[GOAL]
A : Mon_ (Type u)
x y z : A.X
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
convert congr_fun A.mul_assoc ((x, y), z)
[GOAL]
A : Mon_ (Type u)
x : A.X
⊢ 1 * x = x
[PROOFSTEP]
convert congr_fun A.one_mul (PUnit.unit, x)
[GOAL]
A : Mon_ (Type u)
x : A.X
⊢ x * 1 = x
[PROOFSTEP]
convert congr_fun A.mul_one (x, PUnit.unit)
[GOAL]
A : MonCat
⊢ (MonoidalCategory.tensorHom (fun x => 1) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) = (MonoidalCategory.leftUnitor ↑A).hom
[PROOFSTEP]
ext ⟨_, _⟩
[GOAL]
case h.mk
A : MonCat
fst✝ : MonoidalCategory.tensorUnit (Type u)
snd✝ : ↑A
⊢ (MonoidalCategory.tensorHom (fun x => 1) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) (fst✝, snd✝) =
    (MonoidalCategory.leftUnitor ↑A).hom (fst✝, snd✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk
A : MonCat
fst✝ : MonoidalCategory.tensorUnit (Type u)
snd✝ : ↑A
⊢ 1 * snd✝ = snd✝
[PROOFSTEP]
simp
[GOAL]
A : MonCat
⊢ ((MonoidalCategory.tensorHom (𝟙 ↑A) fun x => 1) ≫ fun p => p.fst * p.snd) = (MonoidalCategory.rightUnitor ↑A).hom
[PROOFSTEP]
ext ⟨_, _⟩
[GOAL]
case h.mk
A : MonCat
fst✝ : ↑A
snd✝ : MonoidalCategory.tensorUnit (Type u)
⊢ ((MonoidalCategory.tensorHom (𝟙 ↑A) fun x => 1) ≫ fun p => p.fst * p.snd) (fst✝, snd✝) =
    (MonoidalCategory.rightUnitor ↑A).hom (fst✝, snd✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk
A : MonCat
fst✝ : ↑A
snd✝ : MonoidalCategory.tensorUnit (Type u)
⊢ fst✝ * 1 = fst✝
[PROOFSTEP]
simp
[GOAL]
A : MonCat
⊢ (MonoidalCategory.tensorHom (fun p => p.fst * p.snd) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) =
    (MonoidalCategory.associator ↑A ↑A ↑A).hom ≫
      (MonoidalCategory.tensorHom (𝟙 ↑A) fun p => p.fst * p.snd) ≫ fun p => p.fst * p.snd
[PROOFSTEP]
ext ⟨⟨x, y⟩, z⟩
[GOAL]
case h.mk.mk
A : MonCat
z x y : ↑A
⊢ (MonoidalCategory.tensorHom (fun p => p.fst * p.snd) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) ((x, y), z) =
    ((MonoidalCategory.associator ↑A ↑A ↑A).hom ≫
        (MonoidalCategory.tensorHom (𝟙 ↑A) fun p => p.fst * p.snd) ≫ fun p => p.fst * p.snd)
      ((x, y), z)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
⊢ ∀ {X Y : Mon_ (Type u)} (f : X ⟶ Y),
    (𝟭 (Mon_ (Type u))).map f ≫
        ((fun A =>
              Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (Mon_ (Type u))).obj A).X)) (Mon_.Hom.mk (𝟙 ((functor ⋙ inverse).obj A).X)))
            Y).hom =
      ((fun A => Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (Mon_ (Type u))).obj A).X)) (Mon_.Hom.mk (𝟙 ((functor ⋙ inverse).obj A).X)))
            X).hom ≫
        (functor ⋙ inverse).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : MonCat} (f : X ⟶ Y),
    (inverse ⋙ functor).map f ≫
        ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((inverse ⋙ functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 MonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            Y).hom =
      ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((inverse ⋙ functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 MonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            X).hom ≫
        (𝟭 MonCat).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : Mon_ (Type u)} (f : X ⟶ Y),
    (functor ⋙ forget MonCat).map f ≫ ((fun A => Iso.refl ((functor ⋙ forget MonCat).obj A)) Y).hom =
      ((fun A => Iso.refl ((functor ⋙ forget MonCat).obj A)) X).hom ≫ (Mon_.forget (Type u)).map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : CommMon_ (Type u)
src✝ : Monoid A.X := monMonoid A.toMon_
x y : A.X
⊢ x * y = y * x
[PROOFSTEP]
convert congr_fun A.mul_comm (y, x)
[GOAL]
A : CommMonCat
src✝ : Mon_ (Type u) := MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)
⊢ (β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
      (Mon_.mk src✝.X src✝.one src✝.mul).mul =
    (Mon_.mk src✝.X src✝.one src✝.mul).mul
[PROOFSTEP]
ext ⟨x : A, y : A⟩
[GOAL]
case h.mk
A : CommMonCat
src✝ : Mon_ (Type u) := MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)
x y : ↑A
⊢ ((β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
        (Mon_.mk src✝.X src✝.one src✝.mul).mul)
      (x, y) =
    Mon_.mul (Mon_.mk src✝.X src✝.one src✝.mul) (x, y)
[PROOFSTEP]
exact CommMonoid.mul_comm y x
[GOAL]
⊢ ∀ {X Y : CommMon_ (Type u)} (f : X ⟶ Y),
    (𝟭 (CommMon_ (Type u))).map f ≫
        ((fun A =>
              Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (CommMon_ (Type u))).obj A).X))
                (Mon_.Hom.mk
                  (𝟙 ((CommMonTypeEquivalenceCommMon.functor ⋙ CommMonTypeEquivalenceCommMon.inverse).obj A).X)))
            Y).hom =
      ((fun A =>
              Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (CommMon_ (Type u))).obj A).X))
                (Mon_.Hom.mk
                  (𝟙 ((CommMonTypeEquivalenceCommMon.functor ⋙ CommMonTypeEquivalenceCommMon.inverse).obj A).X)))
            X).hom ≫
        (CommMonTypeEquivalenceCommMon.functor ⋙ CommMonTypeEquivalenceCommMon.inverse).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : CommMonCat} (f : X ⟶ Y),
    (CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).map f ≫
        ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀
                        (x y :
                          ↑((CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 CommMonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            Y).hom =
      ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀
                        (x y :
                          ↑((CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 CommMonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            X).hom ≫
        (𝟭 CommMonCat).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : CommMon_ (Type u)} (f : X ⟶ Y),
    (CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat).map f ≫
        ((fun A => Iso.refl ((CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat).obj A)) Y).hom =
      ((fun A => Iso.refl ((CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat).obj A)) X).hom ≫
        (CommMon_.forget₂Mon_ (Type u) ⋙ MonTypeEquivalenceMon.functor).map f
[PROOFSTEP]
aesop_cat
