Documentation

Mathlib.GroupTheory.Coprod.Basic

Coproduct (free product) of two monoids or groups #

In this file we define Monoid.Coprod M N (notation: M ∗ N) to be the coproduct (a.k.a. free product) of two monoids. The same type is used for the coproduct of two monoids and for the coproduct of two groups.

The coproduct M ∗ N has the following universal property: for any monoid P and homomorphisms f : M →* P, g : N →* P, there exists a unique homomorphism fg : M ∗ N →* P such that fg ∘ Monoid.Coprod.inl = f and fg ∘ Monoid.Coprod.inr = g, where Monoid.Coprod.inl : M →* M ∗ N and Monoid.Coprod.inr : N →* M ∗ N are canonical embeddings. This homomorphism fg is given by Monoid.Coprod.lift f g.

We also define some homomorphisms and isomorphisms about M ∗ N, and provide additive versions of all definitions and theorems.

Main definitions #

Types #

In other sections, we only list multiplicative definitions.

Instances #

Monoid homomorphisms #

Monoid isomorphisms #

Main results #

The universal property of the coproduct is given by the definition Monoid.Coprod.lift and the lemma Monoid.Coprod.lift_unique.

We also prove a slightly more general extensionality lemma Monoid.Coprod.hom_ext for homomorphisms M ∗ N →* P and prove lots of basic lemmas like Monoid.Coprod.fst_comp_inl.

Implementation details #

The definition of the coproduct of an indexed family of monoids is formalized in Monoid.CoprodI. While mathematically M ∗ N is a particular case of the coproduct of an indexed family of monoids, it is easier to build API from scratch instead of using something like

def Monoid.Coprod M N := Monoid.CoprodI ![M, N]

or

def Monoid.Coprod M N := Monoid.CoprodI (fun b : Bool => cond b M N)

There are several reasons to build an API from scratch.

TODO #

Tags #

group, monoid, coproduct, free product

The minimal additive congruence relation c on FreeAddMonoid (M ⊕ N) such that FreeAddMonoid.ofSum.inl and FreeAddMonoid.ofSum.inr are additive monoid homomorphisms to the quotient by c.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Monoid.coprodCon (M : Type u_1) (N : Type u_2) [MulOneClass M] [MulOneClass N] :

    The minimal congruence relation c on FreeMonoid (M ⊕ N) such that FreeMonoid.ofSum.inl and FreeMonoid.ofSum.inr are monoid homomorphisms to the quotient by c.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def AddMonoid.Coprod (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] :
      Type (max u_1 u_2)

      Coproduct of two additive monoids or groups.

      Equations
      Instances For
        def Monoid.Coprod (M : Type u_1) (N : Type u_2) [MulOneClass M] [MulOneClass N] :
        Type (max u_1 u_2)

        Coproduct of two monoids or groups.

        Equations
        Instances For

          Coproduct of two monoids or groups.

          Equations
          Instances For
            Equations
            Equations

            The natural projection FreeAddMonoid (M ⊕ N) →+ AddMonoid.Coprod M N.

            Equations
            Instances For
              def Monoid.Coprod.mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

              The natural projection FreeMonoid (M ⊕ N) →* M ∗ N.

              Equations
              Instances For
                @[simp]
                theorem AddMonoid.Coprod.con_ker_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                AddCon.ker AddMonoid.Coprod.mk = AddMonoid.coprodCon M N
                @[simp]
                theorem Monoid.Coprod.con_ker_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                Con.ker Monoid.Coprod.mk = Monoid.coprodCon M N
                theorem AddMonoid.Coprod.mk_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                Function.Surjective AddMonoid.Coprod.mk
                theorem Monoid.Coprod.mk_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                Function.Surjective Monoid.Coprod.mk
                @[simp]
                theorem AddMonoid.Coprod.mrange_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                AddMonoidHom.mrange AddMonoid.Coprod.mk =
                @[simp]
                theorem Monoid.Coprod.mrange_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                MonoidHom.mrange Monoid.Coprod.mk =
                theorem AddMonoid.Coprod.mk_eq_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {w₁ : FreeAddMonoid (M N)} {w₂ : FreeAddMonoid (M N)} :
                AddMonoid.Coprod.mk w₁ = AddMonoid.Coprod.mk w₂ (AddMonoid.coprodCon M N) w₁ w₂
                theorem Monoid.Coprod.mk_eq_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {w₁ : FreeMonoid (M N)} {w₂ : FreeMonoid (M N)} :
                Monoid.Coprod.mk w₁ = Monoid.Coprod.mk w₂ (Monoid.coprodCon M N) w₁ w₂

                The natural embedding M →+ AddMonoid.Coprod M N.

                Equations
                • AddMonoid.Coprod.inl = { toFun := fun (x : M) => AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl x)), map_zero' := , map_add' := }
                Instances For
                  theorem AddMonoid.Coprod.inl.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                  AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl 0)) = AddMonoid.Coprod.mk 0
                  theorem AddMonoid.Coprod.inl.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (x : M) (y : M) :
                  AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl (x + y))) = AddMonoid.Coprod.mk ((fun (x x_1 : FreeAddMonoid (M N)) => x + x_1) (FreeAddMonoid.of (Sum.inl x)) (FreeAddMonoid.of (Sum.inl y)))
                  def Monoid.Coprod.inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

                  The natural embedding M →* M ∗ N.

                  Equations
                  • Monoid.Coprod.inl = { toFun := fun (x : M) => Monoid.Coprod.mk (FreeMonoid.of (Sum.inl x)), map_one' := , map_mul' := }
                  Instances For
                    theorem AddMonoid.Coprod.inr.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (x : N) (y : N) :
                    AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr (x + y))) = AddMonoid.Coprod.mk ((fun (x x_1 : FreeAddMonoid (M N)) => x + x_1) (FreeAddMonoid.of (Sum.inr x)) (FreeAddMonoid.of (Sum.inr y)))

                    The natural embedding N →+ AddMonoid.Coprod M N.

                    Equations
                    • AddMonoid.Coprod.inr = { toFun := fun (x : N) => AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr x)), map_zero' := , map_add' := }
                    Instances For
                      theorem AddMonoid.Coprod.inr.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                      AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr 0)) = AddMonoid.Coprod.mk 0
                      def Monoid.Coprod.inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

                      The natural embedding N →* M ∗ N.

                      Equations
                      • Monoid.Coprod.inr = { toFun := fun (x : N) => Monoid.Coprod.mk (FreeMonoid.of (Sum.inr x)), map_one' := , map_mul' := }
                      Instances For
                        @[simp]
                        theorem AddMonoid.Coprod.mk_of_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (x : M) :
                        AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl x)) = AddMonoid.Coprod.inl x
                        @[simp]
                        theorem Monoid.Coprod.mk_of_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (x : M) :
                        Monoid.Coprod.mk (FreeMonoid.of (Sum.inl x)) = Monoid.Coprod.inl x
                        @[simp]
                        theorem AddMonoid.Coprod.mk_of_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (x : N) :
                        AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr x)) = AddMonoid.Coprod.inr x
                        @[simp]
                        theorem Monoid.Coprod.mk_of_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (x : N) :
                        Monoid.Coprod.mk (FreeMonoid.of (Sum.inr x)) = Monoid.Coprod.inr x
                        theorem AddMonoid.Coprod.induction_on' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {C : AddMonoid.Coprod M NProp} (m : AddMonoid.Coprod M N) (one : C 0) (inl_mul : ∀ (m : M) (x : AddMonoid.Coprod M N), C xC (AddMonoid.Coprod.inl m + x)) (inr_mul : ∀ (n : N) (x : AddMonoid.Coprod M N), C xC (AddMonoid.Coprod.inr n + x)) :
                        C m
                        theorem Monoid.Coprod.induction_on' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {C : Monoid.Coprod M NProp} (m : Monoid.Coprod M N) (one : C 1) (inl_mul : ∀ (m : M) (x : Monoid.Coprod M N), C xC (Monoid.Coprod.inl m * x)) (inr_mul : ∀ (n : N) (x : Monoid.Coprod M N), C xC (Monoid.Coprod.inr n * x)) :
                        C m
                        theorem AddMonoid.Coprod.induction_on {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {C : AddMonoid.Coprod M NProp} (m : AddMonoid.Coprod M N) (inl : ∀ (m : M), C (AddMonoid.Coprod.inl m)) (inr : ∀ (n : N), C (AddMonoid.Coprod.inr n)) (mul : ∀ (x y : AddMonoid.Coprod M N), C xC yC (x + y)) :
                        C m
                        theorem Monoid.Coprod.induction_on {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {C : Monoid.Coprod M NProp} (m : Monoid.Coprod M N) (inl : ∀ (m : M), C (Monoid.Coprod.inl m)) (inr : ∀ (n : N), C (Monoid.Coprod.inr n)) (mul : ∀ (x y : Monoid.Coprod M N), C xC yC (x * y)) :
                        C m
                        theorem AddMonoid.Coprod.clift.proof_1 {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0) (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) :
                        def AddMonoid.Coprod.clift {M : Type u_1} {N : Type u_2} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0) (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) :

                        Lift an additive monoid homomorphism FreeAddMonoid (M ⊕ N) →+ P satisfying additional properties to AddMonoid.Coprod M N →+ P.

                        Compared to AddMonoid.Coprod.lift, this definition allows a user to provide a custom computational behavior. Also, it only needs AddZeroclass assumptions while AddMonoid.Coprod.lift needs an AddMonoid structure.

                        Equations
                        Instances For
                          def Monoid.Coprod.clift {M : Type u_1} {N : Type u_2} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : FreeMonoid (M N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) :

                          Lift a monoid homomorphism FreeMonoid (M ⊕ N) →* P satisfying additional properties to M ∗ N →* P. In many cases, Coprod.lift is more convenient.

                          Compared to Coprod.lift, this definition allows a user to provide a custom computational behavior. Also, it only needs MulOneclass assumptions while Coprod.lift needs a Monoid structure.

                          Equations
                          Instances For
                            @[simp]
                            theorem AddMonoid.Coprod.clift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0) (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) (x : M) :
                            (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inl x) = f (FreeAddMonoid.of (Sum.inl x))
                            @[simp]
                            theorem Monoid.Coprod.clift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : FreeMonoid (M N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) (x : M) :
                            (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inl x) = f (FreeMonoid.of (Sum.inl x))
                            @[simp]
                            theorem AddMonoid.Coprod.clift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0) (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) (x : N) :
                            (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inr x) = f (FreeAddMonoid.of (Sum.inr x))
                            @[simp]
                            theorem Monoid.Coprod.clift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : FreeMonoid (M N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) (x : N) :
                            (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inr x) = f (FreeMonoid.of (Sum.inr x))
                            @[simp]
                            theorem AddMonoid.Coprod.clift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0) (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) (w : FreeAddMonoid (M N)) :
                            (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.mk w) = f w
                            @[simp]
                            theorem Monoid.Coprod.clift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : FreeMonoid (M N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) (w : FreeMonoid (M N)) :
                            (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.mk w) = f w
                            @[simp]
                            theorem AddMonoid.Coprod.clift_comp_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0) (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) :
                            (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN).comp AddMonoid.Coprod.mk = f
                            @[simp]
                            theorem Monoid.Coprod.clift_comp_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : FreeMonoid (M N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) :
                            (Monoid.Coprod.clift f hM₁ hN₁ hM hN).comp Monoid.Coprod.mk = f
                            @[simp]
                            theorem AddMonoid.Coprod.mclosure_range_inl_union_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                            AddSubmonoid.closure (Set.range AddMonoid.Coprod.inl Set.range AddMonoid.Coprod.inr) =
                            @[simp]
                            theorem Monoid.Coprod.mclosure_range_inl_union_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                            Submonoid.closure (Set.range Monoid.Coprod.inl Set.range Monoid.Coprod.inr) =
                            @[simp]
                            theorem AddMonoid.Coprod.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                            AddMonoidHom.mrange AddMonoid.Coprod.inl AddMonoidHom.mrange AddMonoid.Coprod.inr =
                            @[simp]
                            theorem Monoid.Coprod.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                            MonoidHom.mrange Monoid.Coprod.inl MonoidHom.mrange Monoid.Coprod.inr =
                            theorem AddMonoid.Coprod.codisjoint_mrange_inl_mrange_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                            Codisjoint (AddMonoidHom.mrange AddMonoid.Coprod.inl) (AddMonoidHom.mrange AddMonoid.Coprod.inr)
                            theorem Monoid.Coprod.codisjoint_mrange_inl_mrange_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                            Codisjoint (MonoidHom.mrange Monoid.Coprod.inl) (MonoidHom.mrange Monoid.Coprod.inr)
                            theorem AddMonoid.Coprod.mrange_eq {M : Type u_1} {N : Type u_2} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : AddMonoid.Coprod M N →+ P) :
                            AddMonoidHom.mrange f = AddMonoidHom.mrange (f.comp AddMonoid.Coprod.inl) AddMonoidHom.mrange (f.comp AddMonoid.Coprod.inr)
                            theorem Monoid.Coprod.mrange_eq {M : Type u_1} {N : Type u_2} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : Monoid.Coprod M N →* P) :
                            MonoidHom.mrange f = MonoidHom.mrange (f.comp Monoid.Coprod.inl) MonoidHom.mrange (f.comp Monoid.Coprod.inr)
                            theorem AddMonoid.Coprod.hom_ext {M : Type u_1} {N : Type u_2} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] {f : AddMonoid.Coprod M N →+ P} {g : AddMonoid.Coprod M N →+ P} (h₁ : f.comp AddMonoid.Coprod.inl = g.comp AddMonoid.Coprod.inl) (h₂ : f.comp AddMonoid.Coprod.inr = g.comp AddMonoid.Coprod.inr) :
                            f = g

                            Extensionality lemma for additive monoid homomorphisms AddMonoid.Coprod M N →+ P. If two homomorphisms agree on the ranges of AddMonoid.Coprod.inl and AddMonoid.Coprod.inr, then they are equal.

                            theorem Monoid.Coprod.hom_ext {M : Type u_1} {N : Type u_2} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] {f : Monoid.Coprod M N →* P} {g : Monoid.Coprod M N →* P} (h₁ : f.comp Monoid.Coprod.inl = g.comp Monoid.Coprod.inl) (h₂ : f.comp Monoid.Coprod.inr = g.comp Monoid.Coprod.inr) :
                            f = g

                            Extensionality lemma for monoid homomorphisms M ∗ N →* P. If two homomorphisms agree on the ranges of Monoid.Coprod.inl and Monoid.Coprod.inr, then they are equal.

                            @[simp]
                            theorem AddMonoid.Coprod.clift_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                            AddMonoid.Coprod.clift AddMonoid.Coprod.mk = AddMonoidHom.id (AddMonoid.Coprod M N)
                            @[simp]
                            theorem Monoid.Coprod.clift_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                            Monoid.Coprod.clift Monoid.Coprod.mk = MonoidHom.id (Monoid.Coprod M N)
                            theorem AddMonoid.Coprod.map.proof_4 {M : Type u_4} {N : Type u_3} {M' : Type u_1} {N' : Type u_2} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : N) (y : N) :
                            AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr (g (x + y)))) = (AddMonoid.Coprod.mk.comp (FreeAddMonoid.map (Sum.map f g))) (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))
                            def AddMonoid.Coprod.map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') :

                            Map AddMonoid.Coprod M N to AddMonoid.Coprod M' N' by applying Sum.map f g to each element of the underlying list.

                            Equations
                            Instances For
                              theorem AddMonoid.Coprod.map.proof_2 {N : Type u_3} {M' : Type u_1} {N' : Type u_2} [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (g : N →+ N') :
                              AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr (g 0))) = 0
                              theorem AddMonoid.Coprod.map.proof_1 {M : Type u_3} {M' : Type u_1} {N' : Type u_2} [AddZeroClass M] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') :
                              AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl (f 0))) = 0
                              theorem AddMonoid.Coprod.map.proof_3 {M : Type u_3} {N : Type u_4} {M' : Type u_1} {N' : Type u_2} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : M) (y : M) :
                              AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl (f (x + y)))) = (AddMonoid.Coprod.mk.comp (FreeAddMonoid.map (Sum.map f g))) (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))
                              def Monoid.Coprod.map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') :

                              Map M ∗ N to M' ∗ N' by applying Sum.map f g to each element of the underlying list.

                              Equations
                              Instances For
                                @[simp]
                                theorem AddMonoid.Coprod.map_mk_ofList {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (l : List (M N)) :
                                (AddMonoid.Coprod.map f g) (AddMonoid.Coprod.mk (FreeAddMonoid.ofList l)) = AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map f g) l))
                                @[simp]
                                theorem Monoid.Coprod.map_mk_ofList {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') (l : List (M N)) :
                                (Monoid.Coprod.map f g) (Monoid.Coprod.mk (FreeMonoid.ofList l)) = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map f g) l))
                                @[simp]
                                theorem AddMonoid.Coprod.map_apply_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : M) :
                                (AddMonoid.Coprod.map f g) (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inl (f x)
                                @[simp]
                                theorem Monoid.Coprod.map_apply_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') (x : M) :
                                (Monoid.Coprod.map f g) (Monoid.Coprod.inl x) = Monoid.Coprod.inl (f x)
                                @[simp]
                                theorem AddMonoid.Coprod.map_apply_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : N) :
                                (AddMonoid.Coprod.map f g) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inr (g x)
                                @[simp]
                                theorem Monoid.Coprod.map_apply_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') (x : N) :
                                (Monoid.Coprod.map f g) (Monoid.Coprod.inr x) = Monoid.Coprod.inr (g x)
                                @[simp]
                                theorem AddMonoid.Coprod.map_comp_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') :
                                (AddMonoid.Coprod.map f g).comp AddMonoid.Coprod.inl = AddMonoid.Coprod.inl.comp f
                                @[simp]
                                theorem Monoid.Coprod.map_comp_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') :
                                (Monoid.Coprod.map f g).comp Monoid.Coprod.inl = Monoid.Coprod.inl.comp f
                                @[simp]
                                theorem AddMonoid.Coprod.map_comp_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') :
                                (AddMonoid.Coprod.map f g).comp AddMonoid.Coprod.inr = AddMonoid.Coprod.inr.comp g
                                @[simp]
                                theorem Monoid.Coprod.map_comp_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') :
                                (Monoid.Coprod.map f g).comp Monoid.Coprod.inr = Monoid.Coprod.inr.comp g
                                theorem AddMonoid.Coprod.map_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] {M'' : Type u_6} {N'' : Type u_7} [AddZeroClass M''] [AddZeroClass N''] (f' : M' →+ M'') (g' : N' →+ N'') (f : M →+ M') (g : N →+ N') :
                                (AddMonoid.Coprod.map f' g').comp (AddMonoid.Coprod.map f g) = AddMonoid.Coprod.map (f'.comp f) (g'.comp g)
                                theorem Monoid.Coprod.map_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] {M'' : Type u_6} {N'' : Type u_7} [MulOneClass M''] [MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M') (g : N →* N') :
                                (Monoid.Coprod.map f' g').comp (Monoid.Coprod.map f g) = Monoid.Coprod.map (f'.comp f) (g'.comp g)
                                theorem AddMonoid.Coprod.map_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] {M'' : Type u_6} {N'' : Type u_7} [AddZeroClass M''] [AddZeroClass N''] (f' : M' →+ M'') (g' : N' →+ N'') (f : M →+ M') (g : N →+ N') (x : AddMonoid.Coprod M N) :
                                (AddMonoid.Coprod.map f' g') ((AddMonoid.Coprod.map f g) x) = (AddMonoid.Coprod.map (f'.comp f) (g'.comp g)) x
                                theorem Monoid.Coprod.map_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] {M'' : Type u_6} {N'' : Type u_7} [MulOneClass M''] [MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M') (g : N →* N') (x : Monoid.Coprod M N) :
                                (Monoid.Coprod.map f' g') ((Monoid.Coprod.map f g) x) = (Monoid.Coprod.map (f'.comp f) (g'.comp g)) x

                                Map AddMonoid.Coprod M N to AddMonoid.Coprod N M by applying Sum.swap to each element of the underlying list.

                                See also AddEquiv.coprodComm for an AddEquiv version.

                                Equations
                                Instances For
                                  theorem AddMonoid.Coprod.swap.proof_4 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] (x : N) (y : N) :
                                  AddMonoid.Coprod.inl (x + y) = (AddMonoid.Coprod.mk.comp (FreeAddMonoid.map Sum.swap)) (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))
                                  theorem AddMonoid.Coprod.swap.proof_3 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] (x : M) (y : M) :
                                  AddMonoid.Coprod.inr (x + y) = (AddMonoid.Coprod.mk.comp (FreeAddMonoid.map Sum.swap)) (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))
                                  theorem AddMonoid.Coprod.swap.proof_2 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] :
                                  AddMonoid.Coprod.inl 0 = 0
                                  theorem AddMonoid.Coprod.swap.proof_1 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] :
                                  AddMonoid.Coprod.inr 0 = 0

                                  Map M ∗ N to N ∗ M by applying Sum.swap to each element of the underlying list.

                                  See also MulEquiv.coprodComm for a MulEquiv version.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Monoid.Coprod.swap_swap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (x : Monoid.Coprod M N) :
                                    theorem AddMonoid.Coprod.swap_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') :
                                    theorem Monoid.Coprod.swap_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') :
                                    theorem AddMonoid.Coprod.swap_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : AddMonoid.Coprod M N) :
                                    theorem Monoid.Coprod.swap_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') (x : Monoid.Coprod M N) :
                                    @[simp]
                                    theorem AddMonoid.Coprod.swap_comp_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                                    (AddMonoid.Coprod.swap M N).comp AddMonoid.Coprod.inl = AddMonoid.Coprod.inr
                                    @[simp]
                                    theorem Monoid.Coprod.swap_comp_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                                    (Monoid.Coprod.swap M N).comp Monoid.Coprod.inl = Monoid.Coprod.inr
                                    @[simp]
                                    theorem AddMonoid.Coprod.swap_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (x : M) :
                                    (AddMonoid.Coprod.swap M N) (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inr x
                                    @[simp]
                                    theorem Monoid.Coprod.swap_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (x : M) :
                                    (Monoid.Coprod.swap M N) (Monoid.Coprod.inl x) = Monoid.Coprod.inr x
                                    @[simp]
                                    theorem AddMonoid.Coprod.swap_comp_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                                    (AddMonoid.Coprod.swap M N).comp AddMonoid.Coprod.inr = AddMonoid.Coprod.inl
                                    @[simp]
                                    theorem Monoid.Coprod.swap_comp_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                                    (Monoid.Coprod.swap M N).comp Monoid.Coprod.inr = Monoid.Coprod.inl
                                    @[simp]
                                    theorem AddMonoid.Coprod.swap_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (x : N) :
                                    (AddMonoid.Coprod.swap M N) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inl x
                                    @[simp]
                                    theorem Monoid.Coprod.swap_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (x : N) :
                                    (Monoid.Coprod.swap M N) (Monoid.Coprod.inr x) = Monoid.Coprod.inl x
                                    @[simp]
                                    @[simp]
                                    theorem Monoid.Coprod.swap_inj {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {x : Monoid.Coprod M N} {y : Monoid.Coprod M N} :
                                    @[simp]
                                    theorem AddMonoid.Coprod.swap_eq_zero {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {x : AddMonoid.Coprod M N} :
                                    @[simp]
                                    theorem Monoid.Coprod.swap_eq_one {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {x : Monoid.Coprod M N} :
                                    (Monoid.Coprod.swap M N) x = 1 x = 1
                                    theorem AddMonoid.Coprod.lift.proof_3 {M : Type u_2} {P : Type u_1} [AddZeroClass M] [AddMonoid P] (f : M →+ P) (x : M) (y : M) :
                                    f (x + y) = f x + f y
                                    theorem AddMonoid.Coprod.lift.proof_2 {N : Type u_2} {P : Type u_1} [AddZeroClass N] [AddMonoid P] (g : N →+ P) :
                                    g 0 = 0
                                    def AddMonoid.Coprod.lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) :

                                    Lift a pair of additive monoid homomorphisms f : M →+ P, g : N →+ P to an additive monoid homomorphism AddMonoid.Coprod M N →+ P.

                                    See also AddMonoid.Coprod.clift for a version that allows custom computational behavior and works for an AddZeroClass codomain.

                                    Equations
                                    Instances For
                                      theorem AddMonoid.Coprod.lift.proof_4 {N : Type u_2} {P : Type u_1} [AddZeroClass N] [AddMonoid P] (g : N →+ P) (x : N) (y : N) :
                                      g (x + y) = g x + g y
                                      theorem AddMonoid.Coprod.lift.proof_1 {M : Type u_2} {P : Type u_1} [AddZeroClass M] [AddMonoid P] (f : M →+ P) :
                                      f 0 = 0
                                      def Monoid.Coprod.lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) :

                                      Lift a pair of monoid homomorphisms f : M →* P, g : N →* P to a monoid homomorphism M ∗ N →* P.

                                      See also Coprod.clift for a version that allows custom computational behavior and works for a MulOneClass codomain.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem AddMonoid.Coprod.lift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (x : FreeAddMonoid (M N)) :
                                        (AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.mk x) = (FreeAddMonoid.lift (Sum.elim f g)) x
                                        @[simp]
                                        theorem Monoid.Coprod.lift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (x : FreeMonoid (M N)) :
                                        (Monoid.Coprod.lift f g) (Monoid.Coprod.mk x) = (FreeMonoid.lift (Sum.elim f g)) x
                                        @[simp]
                                        theorem AddMonoid.Coprod.lift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (x : M) :
                                        (AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.inl x) = f x
                                        @[simp]
                                        theorem Monoid.Coprod.lift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (x : M) :
                                        (Monoid.Coprod.lift f g) (Monoid.Coprod.inl x) = f x
                                        theorem AddMonoid.Coprod.lift_unique {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] {f : M →+ P} {g : N →+ P} {fg : AddMonoid.Coprod M N →+ P} (h₁ : fg.comp AddMonoid.Coprod.inl = f) (h₂ : fg.comp AddMonoid.Coprod.inr = g) :
                                        theorem Monoid.Coprod.lift_unique {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] {f : M →* P} {g : N →* P} {fg : Monoid.Coprod M N →* P} (h₁ : fg.comp Monoid.Coprod.inl = f) (h₂ : fg.comp Monoid.Coprod.inr = g) :
                                        @[simp]
                                        theorem AddMonoid.Coprod.lift_comp_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) :
                                        (AddMonoid.Coprod.lift f g).comp AddMonoid.Coprod.inl = f
                                        @[simp]
                                        theorem Monoid.Coprod.lift_comp_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) :
                                        (Monoid.Coprod.lift f g).comp Monoid.Coprod.inl = f
                                        @[simp]
                                        theorem AddMonoid.Coprod.lift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (x : N) :
                                        (AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.inr x) = g x
                                        @[simp]
                                        theorem Monoid.Coprod.lift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (x : N) :
                                        (Monoid.Coprod.lift f g) (Monoid.Coprod.inr x) = g x
                                        @[simp]
                                        theorem AddMonoid.Coprod.lift_comp_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) :
                                        (AddMonoid.Coprod.lift f g).comp AddMonoid.Coprod.inr = g
                                        @[simp]
                                        theorem Monoid.Coprod.lift_comp_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) :
                                        (Monoid.Coprod.lift f g).comp Monoid.Coprod.inr = g
                                        @[simp]
                                        theorem AddMonoid.Coprod.lift_comp_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) :
                                        @[simp]
                                        theorem Monoid.Coprod.lift_comp_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) :
                                        @[simp]
                                        theorem AddMonoid.Coprod.lift_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] (f : M →+ P) (g : N →+ P) (x : AddMonoid.Coprod N M) :
                                        @[simp]
                                        theorem Monoid.Coprod.lift_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] (f : M →* P) (g : N →* P) (x : Monoid.Coprod N M) :
                                        theorem AddMonoid.Coprod.comp_lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] {P' : Type u_4} [AddMonoid P'] (f : P →+ P') (g₁ : M →+ P) (g₂ : N →+ P) :
                                        f.comp (AddMonoid.Coprod.lift g₁ g₂) = AddMonoid.Coprod.lift (f.comp g₁) (f.comp g₂)
                                        theorem Monoid.Coprod.comp_lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] {P' : Type u_4} [Monoid P'] (f : P →* P') (g₁ : M →* P) (g₂ : N →* P) :
                                        f.comp (Monoid.Coprod.lift g₁ g₂) = Monoid.Coprod.lift (f.comp g₁) (f.comp g₂)
                                        def AddMonoid.Coprod.liftEquiv {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] :
                                        (M →+ P) × (N →+ P) (AddMonoid.Coprod M N →+ P)

                                        AddMonoid.Coprod.lift as an equivalence.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem AddMonoid.Coprod.liftEquiv.proof_1 {M : Type u_2} {N : Type u_3} {P : Type u_1} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] :
                                          ∀ (x : (M →+ P) × (N →+ P)), (fun (f : AddMonoid.Coprod M N →+ P) => (f.comp AddMonoid.Coprod.inl, f.comp AddMonoid.Coprod.inr)) ((fun (fg : (M →+ P) × (N →+ P)) => AddMonoid.Coprod.lift fg.1 fg.2) x) = (fun (f : AddMonoid.Coprod M N →+ P) => (f.comp AddMonoid.Coprod.inl, f.comp AddMonoid.Coprod.inr)) ((fun (fg : (M →+ P) × (N →+ P)) => AddMonoid.Coprod.lift fg.1 fg.2) x)
                                          theorem AddMonoid.Coprod.liftEquiv.proof_2 {M : Type u_2} {N : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddMonoid P] :
                                          ∀ (x : AddMonoid.Coprod M N →+ P), (fun (fg : (M →+ P) × (N →+ P)) => AddMonoid.Coprod.lift fg.1 fg.2) ((fun (f : AddMonoid.Coprod M N →+ P) => (f.comp AddMonoid.Coprod.inl, f.comp AddMonoid.Coprod.inr)) x) = x
                                          def Monoid.Coprod.liftEquiv {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [Monoid P] :
                                          (M →* P) × (N →* P) (Monoid.Coprod M N →* P)

                                          Coprod.lift as an equivalence.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem AddMonoid.Coprod.inst.proof_1 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (a : (AddMonoid.coprodCon M N).Quotient) (b : (AddMonoid.coprodCon M N).Quotient) (c : (AddMonoid.coprodCon M N).Quotient) :
                                            a + b + c = a + (b + c)
                                            theorem AddMonoid.Coprod.inst.proof_3 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (a : (AddMonoid.coprodCon M N).Quotient) :
                                            a + 0 = a
                                            instance AddMonoid.Coprod.inst {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                            Equations
                                            theorem AddMonoid.Coprod.inst.proof_5 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                            ∀ (n : ) (x : AddMonoid.Coprod M N), nsmulRec (n + 1) x = nsmulRec (n + 1) x
                                            theorem AddMonoid.Coprod.inst.proof_2 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (a : (AddMonoid.coprodCon M N).Quotient) :
                                            0 + a = a
                                            theorem AddMonoid.Coprod.inst.proof_4 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                            ∀ (x : AddMonoid.Coprod M N), nsmulRec 0 x = nsmulRec 0 x
                                            instance Monoid.Coprod.inst {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                            Equations
                                            • Monoid.Coprod.inst = Monoid.mk npowRec
                                            def AddMonoid.Coprod.fst {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :

                                            The natural projection AddMonoid.Coprod M N →+ M.

                                            Equations
                                            Instances For
                                              def Monoid.Coprod.fst {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :

                                              The natural projection M ∗ N →* M.

                                              Equations
                                              Instances For
                                                def AddMonoid.Coprod.snd {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :

                                                The natural projection AddMonoid.Coprod M N →+ N.

                                                Equations
                                                Instances For
                                                  def Monoid.Coprod.snd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :

                                                  The natural projection M ∗ N →* N.

                                                  Equations
                                                  Instances For
                                                    def AddMonoid.Coprod.toSum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :

                                                    The natural projection AddMonoid.Coprod M N →+ M × N.

                                                    Equations
                                                    Instances For
                                                      def Monoid.Coprod.toProd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :

                                                      The natural projection M ∗ N →* M × N.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_comp_inl {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.fst.comp AddMonoid.Coprod.inl = AddMonoidHom.id M
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_comp_inl {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.fst.comp Monoid.Coprod.inl = MonoidHom.id M
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_apply_inl {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : M) :
                                                        AddMonoid.Coprod.fst (AddMonoid.Coprod.inl x) = x
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_apply_inl {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : M) :
                                                        Monoid.Coprod.fst (Monoid.Coprod.inl x) = x
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_comp_inr {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.fst.comp AddMonoid.Coprod.inr = 0
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_comp_inr {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.fst.comp Monoid.Coprod.inr = 1
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_apply_inr {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : N) :
                                                        AddMonoid.Coprod.fst (AddMonoid.Coprod.inr x) = 0
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_apply_inr {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : N) :
                                                        Monoid.Coprod.fst (Monoid.Coprod.inr x) = 1
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_comp_inl {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.snd.comp AddMonoid.Coprod.inl = 0
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_comp_inl {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.snd.comp Monoid.Coprod.inl = 1
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_apply_inl {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : M) :
                                                        AddMonoid.Coprod.snd (AddMonoid.Coprod.inl x) = 0
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_apply_inl {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : M) :
                                                        Monoid.Coprod.snd (Monoid.Coprod.inl x) = 1
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_comp_inr {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.snd.comp AddMonoid.Coprod.inr = AddMonoidHom.id N
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_comp_inr {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.snd.comp Monoid.Coprod.inr = MonoidHom.id N
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_apply_inr {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : N) :
                                                        AddMonoid.Coprod.snd (AddMonoid.Coprod.inr x) = x
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_apply_inr {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : N) :
                                                        Monoid.Coprod.snd (Monoid.Coprod.inr x) = x
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.toSum_comp_inl {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.toSum.comp AddMonoid.Coprod.inl = AddMonoidHom.inl M N
                                                        @[simp]
                                                        theorem Monoid.Coprod.toProd_comp_inl {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.toProd.comp Monoid.Coprod.inl = MonoidHom.inl M N
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.toSum_comp_inr {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.toSum.comp AddMonoid.Coprod.inr = AddMonoidHom.inr M N
                                                        @[simp]
                                                        theorem Monoid.Coprod.toProd_comp_inr {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.toProd.comp Monoid.Coprod.inr = MonoidHom.inr M N
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.toSum_apply_inl {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : M) :
                                                        AddMonoid.Coprod.toSum (AddMonoid.Coprod.inl x) = (x, 0)
                                                        @[simp]
                                                        theorem Monoid.Coprod.toProd_apply_inl {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : M) :
                                                        Monoid.Coprod.toProd (Monoid.Coprod.inl x) = (x, 1)
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.toSum_apply_inr {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : N) :
                                                        AddMonoid.Coprod.toSum (AddMonoid.Coprod.inr x) = (0, x)
                                                        @[simp]
                                                        theorem Monoid.Coprod.toProd_apply_inr {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : N) :
                                                        Monoid.Coprod.toProd (Monoid.Coprod.inr x) = (1, x)
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_sum_snd {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.fst.prod AddMonoid.Coprod.snd = AddMonoid.Coprod.toSum
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_prod_snd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.fst.prod Monoid.Coprod.snd = Monoid.Coprod.toProd
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.sum_mk_fst_snd {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : AddMonoid.Coprod M N) :
                                                        (AddMonoid.Coprod.fst x, AddMonoid.Coprod.snd x) = AddMonoid.Coprod.toSum x
                                                        @[simp]
                                                        theorem Monoid.Coprod.prod_mk_fst_snd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : Monoid.Coprod M N) :
                                                        (Monoid.Coprod.fst x, Monoid.Coprod.snd x) = Monoid.Coprod.toProd x
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_comp_toSum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        (AddMonoidHom.fst M N).comp AddMonoid.Coprod.toSum = AddMonoid.Coprod.fst
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_comp_toProd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        (MonoidHom.fst M N).comp Monoid.Coprod.toProd = Monoid.Coprod.fst
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_toSum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : AddMonoid.Coprod M N) :
                                                        (AddMonoid.Coprod.toSum x).1 = AddMonoid.Coprod.fst x
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_toProd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : Monoid.Coprod M N) :
                                                        (Monoid.Coprod.toProd x).1 = Monoid.Coprod.fst x
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_comp_toSum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        (AddMonoidHom.snd M N).comp AddMonoid.Coprod.toSum = AddMonoid.Coprod.snd
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_comp_toProd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        (MonoidHom.snd M N).comp Monoid.Coprod.toProd = Monoid.Coprod.snd
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_toSum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : AddMonoid.Coprod M N) :
                                                        (AddMonoid.Coprod.toSum x).2 = AddMonoid.Coprod.snd x
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_toProd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : Monoid.Coprod M N) :
                                                        (Monoid.Coprod.toProd x).2 = Monoid.Coprod.snd x
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_comp_swap {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.fst.comp (AddMonoid.Coprod.swap M N) = AddMonoid.Coprod.snd
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_comp_swap {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.fst.comp (Monoid.Coprod.swap M N) = Monoid.Coprod.snd
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.fst_swap {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : AddMonoid.Coprod M N) :
                                                        AddMonoid.Coprod.fst ((AddMonoid.Coprod.swap M N) x) = AddMonoid.Coprod.snd x
                                                        @[simp]
                                                        theorem Monoid.Coprod.fst_swap {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : Monoid.Coprod M N) :
                                                        Monoid.Coprod.fst ((Monoid.Coprod.swap M N) x) = Monoid.Coprod.snd x
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_comp_swap {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.snd.comp (AddMonoid.Coprod.swap M N) = AddMonoid.Coprod.fst
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_comp_swap {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.snd.comp (Monoid.Coprod.swap M N) = Monoid.Coprod.fst
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.snd_swap {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : AddMonoid.Coprod M N) :
                                                        AddMonoid.Coprod.snd ((AddMonoid.Coprod.swap M N) x) = AddMonoid.Coprod.fst x
                                                        @[simp]
                                                        theorem Monoid.Coprod.snd_swap {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : Monoid.Coprod M N) :
                                                        Monoid.Coprod.snd ((Monoid.Coprod.swap M N) x) = Monoid.Coprod.fst x
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.lift_inr_inl {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.lift AddMonoid.Coprod.inr AddMonoid.Coprod.inl = AddMonoid.Coprod.swap M N
                                                        @[simp]
                                                        theorem Monoid.Coprod.lift_inr_inl {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.lift Monoid.Coprod.inr Monoid.Coprod.inl = Monoid.Coprod.swap M N
                                                        @[simp]
                                                        theorem AddMonoid.Coprod.lift_inl_inr {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        AddMonoid.Coprod.lift AddMonoid.Coprod.inl AddMonoid.Coprod.inr = AddMonoidHom.id (AddMonoid.Coprod M N)
                                                        @[simp]
                                                        theorem Monoid.Coprod.lift_inl_inr {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Monoid.Coprod.lift Monoid.Coprod.inl Monoid.Coprod.inr = MonoidHom.id (Monoid.Coprod M N)
                                                        theorem AddMonoid.Coprod.inl_injective {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        Function.Injective AddMonoid.Coprod.inl
                                                        theorem Monoid.Coprod.inl_injective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Function.Injective Monoid.Coprod.inl
                                                        theorem AddMonoid.Coprod.inr_injective {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        Function.Injective AddMonoid.Coprod.inr
                                                        theorem Monoid.Coprod.inr_injective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Function.Injective Monoid.Coprod.inr
                                                        theorem AddMonoid.Coprod.fst_surjective {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        Function.Surjective AddMonoid.Coprod.fst
                                                        theorem Monoid.Coprod.fst_surjective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Function.Surjective Monoid.Coprod.fst
                                                        theorem AddMonoid.Coprod.snd_surjective {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        Function.Surjective AddMonoid.Coprod.snd
                                                        theorem Monoid.Coprod.snd_surjective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Function.Surjective Monoid.Coprod.snd
                                                        theorem AddMonoid.Coprod.toSum_surjective {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] :
                                                        Function.Surjective AddMonoid.Coprod.toSum
                                                        theorem Monoid.Coprod.toProd_surjective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] :
                                                        Function.Surjective Monoid.Coprod.toProd
                                                        theorem AddMonoid.Coprod.mk_of_neg_add {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (x : G H) :
                                                        AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.map Neg.neg Neg.neg x)) + AddMonoid.Coprod.mk (FreeAddMonoid.of x) = 0
                                                        abbrev AddMonoid.Coprod.mk_of_neg_add.match_1 {G : Type u_1} {H : Type u_2} (motive : G HProp) :
                                                        ∀ (x : G H), (∀ (val : G), motive (Sum.inl val))(∀ (val : H), motive (Sum.inr val))motive x
                                                        Equations
                                                        • =
                                                        Instances For
                                                          theorem Monoid.Coprod.mk_of_inv_mul {G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : G H) :
                                                          Monoid.Coprod.mk (FreeMonoid.of (Sum.map Inv.inv Inv.inv x)) * Monoid.Coprod.mk (FreeMonoid.of x) = 1
                                                          theorem AddMonoid.Coprod.con_add_left_neg {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (x : FreeAddMonoid (G H)) :
                                                          (AddMonoid.coprodCon G H) (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList x)).reverse + x) 0
                                                          theorem Monoid.Coprod.con_mul_left_inv {G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : FreeMonoid (G H)) :
                                                          (Monoid.coprodCon G H) (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList x)).reverse * x) 1
                                                          theorem AddMonoid.Coprod.instNeg.proof_1 {G : Type u_2} {H : Type u_1} [AddGroup G] [AddGroup H] :
                                                          ∀ (x x_1 : FreeAddMonoid (G H)), (AddMonoid.coprodCon G H) x x_1(AddMonoid.coprodCon G H) (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList x)).reverse) (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList x_1)).reverse)
                                                          instance AddMonoid.Coprod.instNeg {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          instance Monoid.Coprod.instInv {G : Type u_1} {H : Type u_2} [Group G] [Group H] :
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          theorem AddMonoid.Coprod.neg_def {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (w : FreeAddMonoid (G H)) :
                                                          -AddMonoid.Coprod.mk w = AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList w)).reverse)
                                                          theorem Monoid.Coprod.inv_def {G : Type u_1} {H : Type u_2} [Group G] [Group H] (w : FreeMonoid (G H)) :
                                                          (Monoid.Coprod.mk w)⁻¹ = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList w)).reverse)
                                                          theorem AddMonoid.Coprod.instAddGroup.proof_5 {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (y : AddMonoid.Coprod G H) :
                                                          -y + y = 0
                                                          theorem AddMonoid.Coprod.instAddGroup.proof_1 {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          ∀ (a b : AddMonoid.Coprod G H), a - b = a - b
                                                          theorem AddMonoid.Coprod.instAddGroup.proof_4 {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          ∀ (n : ) (a : AddMonoid.Coprod G H), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
                                                          Equations
                                                          theorem AddMonoid.Coprod.instAddGroup.proof_2 {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          ∀ (a : AddMonoid.Coprod G H), zsmulRec 0 a = zsmulRec 0 a
                                                          theorem AddMonoid.Coprod.instAddGroup.proof_3 {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          ∀ (n : ) (a : AddMonoid.Coprod G H), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
                                                          instance Monoid.Coprod.instGroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] :
                                                          Equations
                                                          @[simp]
                                                          theorem AddMonoid.Coprod.closure_range_inl_union_inr {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          AddSubgroup.closure (Set.range AddMonoid.Coprod.inl Set.range AddMonoid.Coprod.inr) =
                                                          @[simp]
                                                          theorem Monoid.Coprod.closure_range_inl_union_inr {G : Type u_1} {H : Type u_2} [Group G] [Group H] :
                                                          Subgroup.closure (Set.range Monoid.Coprod.inl Set.range Monoid.Coprod.inr) =
                                                          @[simp]
                                                          theorem AddMonoid.Coprod.range_inl_sup_range_inr {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          AddMonoid.Coprod.inl.range AddMonoid.Coprod.inr.range =
                                                          @[simp]
                                                          theorem Monoid.Coprod.range_inl_sup_range_inr {G : Type u_1} {H : Type u_2} [Group G] [Group H] :
                                                          Monoid.Coprod.inl.range Monoid.Coprod.inr.range =
                                                          theorem AddMonoid.Coprod.codisjoint_range_inl_range_inr {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          Codisjoint AddMonoid.Coprod.inl.range AddMonoid.Coprod.inr.range
                                                          theorem Monoid.Coprod.codisjoint_range_inl_range_inr {G : Type u_1} {H : Type u_2} [Group G] [Group H] :
                                                          Codisjoint Monoid.Coprod.inl.range Monoid.Coprod.inr.range
                                                          @[simp]
                                                          theorem AddMonoid.Coprod.range_swap {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
                                                          @[simp]
                                                          theorem Monoid.Coprod.range_swap {G : Type u_1} {H : Type u_2} [Group G] [Group H] :
                                                          theorem AddMonoid.Coprod.range_eq {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {K : Type u_3} [AddGroup K] (f : AddMonoid.Coprod G H →+ K) :
                                                          f.range = (f.comp AddMonoid.Coprod.inl).range (f.comp AddMonoid.Coprod.inr).range
                                                          theorem Monoid.Coprod.range_eq {G : Type u_1} {H : Type u_2} [Group G] [Group H] {K : Type u_3} [Group K] (f : Monoid.Coprod G H →* K) :
                                                          f.range = (f.comp Monoid.Coprod.inl).range (f.comp Monoid.Coprod.inr).range
                                                          @[simp]
                                                          theorem AddMonoid.Coprod.range_lift {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {K : Type u_3} [AddGroup K] (f : G →+ K) (g : H →+ K) :
                                                          (AddMonoid.Coprod.lift f g).range = f.range g.range
                                                          @[simp]
                                                          theorem Monoid.Coprod.range_lift {G : Type u_1} {H : Type u_2} [Group G] [Group H] {K : Type u_3} [Group K] (f : G →* K) (g : H →* K) :
                                                          (Monoid.Coprod.lift f g).range = f.range g.range
                                                          theorem AddMonoid.MulEquiv.coprodCongr.proof_5 {M : Type u_1} {N : Type u_3} {M' : Type u_2} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N') :
                                                          (AddMonoid.Coprod.map e.symm e'.symm).comp (AddMonoid.Coprod.map e e') = AddMonoidHom.id (AddMonoid.Coprod M M')
                                                          theorem AddMonoid.MulEquiv.coprodCongr.proof_6 {M : Type u_3} {N : Type u_1} {M' : Type u_4} {N' : Type u_2} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N') :
                                                          (AddMonoid.Coprod.map e e').comp (AddMonoid.Coprod.map e.symm e'.symm) = AddMonoidHom.id (AddMonoid.Coprod N N')
                                                          def AddMonoid.MulEquiv.coprodCongr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N') :

                                                          Lift two additive monoid equivalences e : M ≃+ N and e' : M' ≃+ N' to an additive monoid equivalence (AddMonoid.Coprod M M') ≃+ (AddMonoid.Coprod N N').

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem AddMonoid.MulEquiv.coprodCongr_symm_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N') :
                                                            (AddMonoid.MulEquiv.coprodCongr e e').symm = (AddMonoid.Coprod.map e.symm e'.symm)
                                                            @[simp]
                                                            theorem Monoid.MulEquiv.coprodCongr_symm_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (e : M ≃* N) (e' : M' ≃* N') :
                                                            (Monoid.MulEquiv.coprodCongr e e').symm = (Monoid.Coprod.map e.symm e'.symm)
                                                            @[simp]
                                                            theorem Monoid.MulEquiv.coprodCongr_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (e : M ≃* N) (e' : M' ≃* N') :
                                                            @[simp]
                                                            theorem AddMonoid.MulEquiv.coprodCongr_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N') :
                                                            def Monoid.MulEquiv.coprodCongr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (e : M ≃* N) (e' : M' ≃* N') :

                                                            Lift two monoid equivalences e : M ≃* N and e' : M' ≃* N' to a monoid equivalence (M ∗ M') ≃* (N ∗ N').

                                                            Equations
                                                            Instances For

                                                              A MulEquiv version of Coprod.swap.

                                                              Equations
                                                              Instances For
                                                                theorem AddMonoid.MulEquiv.coprodAssoc.proof_1 (M : Type u_1) (N : Type u_2) (P : Type u_3) [AddMonoid M] [AddMonoid N] [AddMonoid P] :
                                                                (AddMonoid.Coprod.lift (AddMonoid.Coprod.inl.comp AddMonoid.Coprod.inl) (AddMonoid.Coprod.map AddMonoid.Coprod.inr (AddMonoidHom.id P))).comp (AddMonoid.Coprod.lift (AddMonoid.Coprod.map (AddMonoidHom.id M) AddMonoid.Coprod.inl) (AddMonoid.Coprod.inr.comp AddMonoid.Coprod.inr)) = AddMonoidHom.id (AddMonoid.Coprod (AddMonoid.Coprod M N) P)

                                                                An additive equivalence between AddMonoid.Coprod (AddMonoid.Coprod M N) P and AddMonoid.Coprod M (AddMonoid.Coprod N P).

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  theorem AddMonoid.MulEquiv.coprodAssoc.proof_2 (M : Type u_1) (N : Type u_2) (P : Type u_3) [AddMonoid M] [AddMonoid N] [AddMonoid P] :
                                                                  (AddMonoid.Coprod.lift (AddMonoid.Coprod.map (AddMonoidHom.id M) AddMonoid.Coprod.inl) (AddMonoid.Coprod.inr.comp AddMonoid.Coprod.inr)).comp (AddMonoid.Coprod.lift (AddMonoid.Coprod.inl.comp AddMonoid.Coprod.inl) (AddMonoid.Coprod.map AddMonoid.Coprod.inr (AddMonoidHom.id P))) = AddMonoidHom.id (AddMonoid.Coprod M (AddMonoid.Coprod N P))

                                                                  A multiplicative equivalence between (M ∗ N) ∗ P and M ∗ (N ∗ P).

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem AddMonoid.MulEquiv.coprodAssoc_apply_inl_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddMonoid M] [AddMonoid N] [AddMonoid P] (x : M) :
                                                                    (AddMonoid.MulEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inl (AddMonoid.Coprod.inl x)) = AddMonoid.Coprod.inl x
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (x : M) :
                                                                    (Monoid.MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inl (Monoid.Coprod.inl x)) = Monoid.Coprod.inl x
                                                                    @[simp]
                                                                    theorem AddMonoid.MulEquiv.coprodAssoc_apply_inl_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddMonoid M] [AddMonoid N] [AddMonoid P] (x : N) :
                                                                    (AddMonoid.MulEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inl (AddMonoid.Coprod.inr x)) = AddMonoid.Coprod.inr (AddMonoid.Coprod.inl x)
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (x : N) :
                                                                    (Monoid.MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inl (Monoid.Coprod.inr x)) = Monoid.Coprod.inr (Monoid.Coprod.inl x)
                                                                    @[simp]
                                                                    theorem AddMonoid.MulEquiv.coprodAssoc_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddMonoid M] [AddMonoid N] [AddMonoid P] (x : P) :
                                                                    (AddMonoid.MulEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inr (AddMonoid.Coprod.inr x)
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodAssoc_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (x : P) :
                                                                    (Monoid.MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inr x) = Monoid.Coprod.inr (Monoid.Coprod.inr x)
                                                                    @[simp]
                                                                    theorem AddMonoid.MulEquiv.coprodAssoc_symm_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddMonoid M] [AddMonoid N] [AddMonoid P] (x : M) :
                                                                    (AddMonoid.MulEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inl (AddMonoid.Coprod.inl x)
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (x : M) :
                                                                    (Monoid.MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inl x) = Monoid.Coprod.inl (Monoid.Coprod.inl x)
                                                                    @[simp]
                                                                    theorem AddMonoid.MulEquiv.coprodAssoc_symm_apply_inr_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddMonoid M] [AddMonoid N] [AddMonoid P] (x : N) :
                                                                    (AddMonoid.MulEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inr (AddMonoid.Coprod.inl x)) = AddMonoid.Coprod.inl (AddMonoid.Coprod.inr x)
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (x : N) :
                                                                    (Monoid.MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inr (Monoid.Coprod.inl x)) = Monoid.Coprod.inl (Monoid.Coprod.inr x)
                                                                    @[simp]
                                                                    theorem AddMonoid.MulEquiv.coprodAssoc_symm_apply_inr_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddMonoid M] [AddMonoid N] [AddMonoid P] (x : P) :
                                                                    (AddMonoid.MulEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inr (AddMonoid.Coprod.inr x)) = AddMonoid.Coprod.inr x
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (x : P) :
                                                                    (Monoid.MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inr (Monoid.Coprod.inr x)) = Monoid.Coprod.inr x
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodPUnit_apply (M : Type u_1) [Monoid M] :
                                                                    (Monoid.MulEquiv.coprodPUnit M) = Monoid.Coprod.fst
                                                                    @[simp]
                                                                    theorem Monoid.MulEquiv.coprodPUnit_symm_apply (M : Type u_1) [Monoid M] :
                                                                    (Monoid.MulEquiv.coprodPUnit M).symm = Monoid.Coprod.inl

                                                                    Isomorphism between M ∗ PUnit and M.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Monoid.MulEquiv.punitCoprod_apply (M : Type u_1) [Monoid M] :
                                                                      (Monoid.MulEquiv.punitCoprod M) = Monoid.Coprod.snd
                                                                      @[simp]
                                                                      theorem Monoid.MulEquiv.punitCoprod_symm_apply (M : Type u_1) [Monoid M] :
                                                                      (Monoid.MulEquiv.punitCoprod M).symm = Monoid.Coprod.inr

                                                                      Isomorphism between PUnit ∗ M and M.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem Monoid.AddEquiv.coprodUnit_apply {M : Type u_1} [AddMonoid M] :
                                                                        Monoid.AddEquiv.coprodUnit = AddMonoid.Coprod.fst
                                                                        @[simp]
                                                                        theorem Monoid.AddEquiv.coprodUnit_symm_apply {M : Type u_1} [AddMonoid M] :
                                                                        Monoid.AddEquiv.coprodUnit.symm = AddMonoid.Coprod.inl

                                                                        Isomorphism between M ∗ PUnit and M.

                                                                        Equations
                                                                        • Monoid.AddEquiv.coprodUnit = AddMonoid.Coprod.fst.toAddEquiv AddMonoid.Coprod.inl
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Monoid.AddEquiv.punitCoprod_symm_apply {M : Type u_1} [AddMonoid M] :
                                                                          Monoid.AddEquiv.punitCoprod.symm = AddMonoid.Coprod.inr
                                                                          @[simp]
                                                                          theorem Monoid.AddEquiv.punitCoprod_apply {M : Type u_1} [AddMonoid M] :
                                                                          Monoid.AddEquiv.punitCoprod = AddMonoid.Coprod.snd

                                                                          Isomorphism between PUnit ∗ M and M.

                                                                          Equations
                                                                          • Monoid.AddEquiv.punitCoprod = AddMonoid.Coprod.snd.toAddEquiv AddMonoid.Coprod.inr
                                                                          Instances For