ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Function.Surjective ⇑(Monoid.Coprod.swap M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Function.Bijective ⇑(AddMonoid.Coprod.swap M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Function.Bijective ⇑(Monoid.Coprod.swap M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mker (Monoid.Coprod.swap M N) = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mker (AddMonoid.Coprod.swap M N) = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoid.Coprod.swap M N) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (Monoid.Coprod.swap M N) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>x : FreeMonoid (M ⊕ N)<GOAL>(Monoid.Coprod.lift f g) (Monoid.Coprod.mk x) = (FreeMonoid.lift (Sum.elim ⇑f ⇑g)) x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>x : FreeAddMonoid (M ⊕ N)<GOAL>(AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.mk x) = (FreeAddMonoid.lift (Sum.elim ⇑f ⇑g)) x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>x : M<GOAL>(AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.inl x) = f x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>x : M<GOAL>(Monoid.Coprod.lift f g) (Monoid.Coprod.inl x) = f x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>fg : AddMonoid.Coprod M N →+ P<VAR>h₁ : fg.comp AddMonoid.Coprod.inl = f<VAR>h₂ : fg.comp AddMonoid.Coprod.inr = g<GOAL>fg = AddMonoid.Coprod.lift f g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>fg : Monoid.Coprod M N →* P<VAR>h₁ : fg.comp Monoid.Coprod.inl = f<VAR>h₂ : fg.comp Monoid.Coprod.inr = g<GOAL>fg = Monoid.Coprod.lift f g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<GOAL>(Monoid.Coprod.lift f g).comp Monoid.Coprod.inl = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<GOAL>(AddMonoid.Coprod.lift f g).comp AddMonoid.Coprod.inl = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>x : N<GOAL>(AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.inr x) = g x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>x : N<GOAL>(Monoid.Coprod.lift f g) (Monoid.Coprod.inr x) = g x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<GOAL>(Monoid.Coprod.lift f g).comp Monoid.Coprod.inr = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<GOAL>(AddMonoid.Coprod.lift f g).comp AddMonoid.Coprod.inr = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<GOAL>(AddMonoid.Coprod.lift f g).comp (AddMonoid.Coprod.swap N M) = AddMonoid.Coprod.lift g f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<GOAL>(Monoid.Coprod.lift f g).comp (Monoid.Coprod.swap N M) = Monoid.Coprod.lift g f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>x : AddMonoid.Coprod N M<GOAL>(AddMonoid.Coprod.lift f g) ((AddMonoid.Coprod.swap N M) x) = (AddMonoid.Coprod.lift g f) x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>x : Monoid.Coprod N M<GOAL>(Monoid.Coprod.lift f g) ((Monoid.Coprod.swap N M) x) = (Monoid.Coprod.lift g f) x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>P' : Type u_4<VAR>AddMonoid P'<VAR>f : P →+ P'<VAR>g₁ : M →+ P<VAR>g₂ : N →+ P<GOAL>f.comp (AddMonoid.Coprod.lift g₁ g₂) = AddMonoid.Coprod.lift (f.comp g₁) (f.comp g₂)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>P' : Type u_4<VAR>Monoid P'<VAR>f : P →* P'<VAR>g₁ : M →* P<VAR>g₂ : N →* P<GOAL>f.comp (Monoid.Coprod.lift g₁ g₂) = Monoid.Coprod.lift (f.comp g₁) (f.comp g₂)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<GOAL>AddMonoidHom.mrange (AddMonoid.Coprod.lift f g) = AddMonoidHom.mrange f ⊔ AddMonoidHom.mrange g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<GOAL>MonoidHom.mrange (Monoid.Coprod.lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.fst.comp AddMonoid.Coprod.inl = AddMonoidHom.id M
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.fst.comp Monoid.Coprod.inl = MonoidHom.id M
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : M<GOAL>AddMonoid.Coprod.fst (AddMonoid.Coprod.inl x) = x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : M<GOAL>Monoid.Coprod.fst (Monoid.Coprod.inl x) = x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.fst.comp AddMonoid.Coprod.inr = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.fst.comp Monoid.Coprod.inr = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : N<GOAL>AddMonoid.Coprod.fst (AddMonoid.Coprod.inr x) = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : N<GOAL>Monoid.Coprod.fst (Monoid.Coprod.inr x) = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.snd.comp Monoid.Coprod.inl = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.snd.comp AddMonoid.Coprod.inl = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : M<GOAL>Monoid.Coprod.snd (Monoid.Coprod.inl x) = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : M<GOAL>AddMonoid.Coprod.snd (AddMonoid.Coprod.inl x) = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.snd.comp Monoid.Coprod.inr = MonoidHom.id N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.snd.comp AddMonoid.Coprod.inr = AddMonoidHom.id N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : N<GOAL>AddMonoid.Coprod.snd (AddMonoid.Coprod.inr x) = x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : N<GOAL>Monoid.Coprod.snd (Monoid.Coprod.inr x) = x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.toProd.comp Monoid.Coprod.inl = MonoidHom.inl M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.toSum.comp AddMonoid.Coprod.inl = AddMonoidHom.inl M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.toSum.comp AddMonoid.Coprod.inr = AddMonoidHom.inr M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.toProd.comp Monoid.Coprod.inr = MonoidHom.inr M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : M<GOAL>Monoid.Coprod.toProd (Monoid.Coprod.inl x) = (x, 1)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : M<GOAL>AddMonoid.Coprod.toSum (AddMonoid.Coprod.inl x) = (x, 0)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : N<GOAL>AddMonoid.Coprod.toSum (AddMonoid.Coprod.inr x) = (0, x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : N<GOAL>Monoid.Coprod.toProd (Monoid.Coprod.inr x) = (1, x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.fst.prod Monoid.Coprod.snd = Monoid.Coprod.toProd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.fst.prod AddMonoid.Coprod.snd = AddMonoid.Coprod.toSum
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.fst x, AddMonoid.Coprod.snd x) = AddMonoid.Coprod.toSum x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : Monoid.Coprod M N<GOAL>(Monoid.Coprod.fst x, Monoid.Coprod.snd x) = Monoid.Coprod.toProd x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>(MonoidHom.fst M N).comp Monoid.Coprod.toProd = Monoid.Coprod.fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>(AddMonoidHom.fst M N).comp AddMonoid.Coprod.toSum = AddMonoid.Coprod.fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : Monoid.Coprod M N<GOAL>(Monoid.Coprod.toProd x).1 = Monoid.Coprod.fst x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.toSum x).1 = AddMonoid.Coprod.fst x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>(AddMonoidHom.snd M N).comp AddMonoid.Coprod.toSum = AddMonoid.Coprod.snd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>(MonoidHom.snd M N).comp Monoid.Coprod.toProd = Monoid.Coprod.snd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.toSum x).2 = AddMonoid.Coprod.snd x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : Monoid.Coprod M N<GOAL>(Monoid.Coprod.toProd x).2 = Monoid.Coprod.snd x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.fst.comp (Monoid.Coprod.swap M N) = Monoid.Coprod.snd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.fst.comp (AddMonoid.Coprod.swap M N) = AddMonoid.Coprod.snd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : Monoid.Coprod M N<GOAL>Monoid.Coprod.fst ((Monoid.Coprod.swap M N) x) = Monoid.Coprod.snd x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : AddMonoid.Coprod M N<GOAL>AddMonoid.Coprod.fst ((AddMonoid.Coprod.swap M N) x) = AddMonoid.Coprod.snd x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.snd.comp (AddMonoid.Coprod.swap M N) = AddMonoid.Coprod.fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.snd.comp (Monoid.Coprod.swap M N) = Monoid.Coprod.fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>x : AddMonoid.Coprod M N<GOAL>AddMonoid.Coprod.snd ((AddMonoid.Coprod.swap M N) x) = AddMonoid.Coprod.fst x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>x : Monoid.Coprod M N<GOAL>Monoid.Coprod.snd ((Monoid.Coprod.swap M N) x) = Monoid.Coprod.fst x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.lift Monoid.Coprod.inr Monoid.Coprod.inl = Monoid.Coprod.swap M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.lift AddMonoid.Coprod.inr AddMonoid.Coprod.inl = AddMonoid.Coprod.swap M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Monoid.Coprod.lift Monoid.Coprod.inl Monoid.Coprod.inr = MonoidHom.id (Monoid.Coprod M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>AddMonoid.Coprod.lift AddMonoid.Coprod.inl AddMonoid.Coprod.inr = AddMonoidHom.id (AddMonoid.Coprod M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Function.Injective ⇑Monoid.Coprod.inl
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>Function.Injective ⇑AddMonoid.Coprod.inl
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>Function.Injective ⇑AddMonoid.Coprod.inr
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Function.Injective ⇑Monoid.Coprod.inr
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>Function.Surjective ⇑AddMonoid.Coprod.fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Function.Surjective ⇑Monoid.Coprod.fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>Function.Surjective ⇑AddMonoid.Coprod.snd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Function.Surjective ⇑Monoid.Coprod.snd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<GOAL>Function.Surjective ⇑Monoid.Coprod.toProd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>Function.Surjective ⇑AddMonoid.Coprod.toSum
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>x : G ⊕ H<GOAL>Monoid.Coprod.mk (FreeMonoid.of (Sum.map Inv.inv Inv.inv x)) * Monoid.Coprod.mk (FreeMonoid.of x) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>x : G ⊕ H<GOAL>AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.map Neg.neg Neg.neg x)) + AddMonoid.Coprod.mk (FreeAddMonoid.of x) = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>x : FreeMonoid (G ⊕ H)<GOAL>(Monoid.coprodCon G H) (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList x)).reverse * x) 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>x : FreeAddMonoid (G ⊕ H)<GOAL>(AddMonoid.coprodCon G H) (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList x)).reverse + x) 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>w : FreeMonoid (G ⊕ H)<GOAL>(Monoid.Coprod.mk w)⁻¹ = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList w)).reverse)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>w : FreeAddMonoid (G ⊕ H)<GOAL>-AddMonoid.Coprod.mk w = AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList w)).reverse)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<GOAL>Subgroup.closure (Set.range ⇑Monoid.Coprod.inl ∪ Set.range ⇑Monoid.Coprod.inr) = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<GOAL>AddSubgroup.closure (Set.range ⇑AddMonoid.Coprod.inl ∪ Set.range ⇑AddMonoid.Coprod.inr) = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<GOAL>Monoid.Coprod.inl.range ⊔ Monoid.Coprod.inr.range = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<GOAL>AddMonoid.Coprod.inl.range ⊔ AddMonoid.Coprod.inr.range = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<GOAL>Codisjoint AddMonoid.Coprod.inl.range AddMonoid.Coprod.inr.range
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<GOAL>Codisjoint Monoid.Coprod.inl.range Monoid.Coprod.inr.range
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<GOAL>(Monoid.Coprod.swap G H).range = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<GOAL>(AddMonoid.Coprod.swap G H).range = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>K : Type u_3<VAR>AddGroup K<VAR>f : AddMonoid.Coprod G H →+ K<GOAL>f.range = (f.comp AddMonoid.Coprod.inl).range ⊔ (f.comp AddMonoid.Coprod.inr).range
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>K : Type u_3<VAR>Group K<VAR>f : Monoid.Coprod G H →* K<GOAL>f.range = (f.comp Monoid.Coprod.inl).range ⊔ (f.comp Monoid.Coprod.inr).range
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>K : Type u_3<VAR>Group K<VAR>f : G →* K<VAR>g : H →* K<GOAL>(Monoid.Coprod.lift f g).range = f.range ⊔ g.range
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>K : Type u_3<VAR>AddGroup K<VAR>f : G →+ K<VAR>g : H →+ K<GOAL>(AddMonoid.Coprod.lift f g).range = f.range ⊔ g.range
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>e : M ≃+ N<VAR>e' : M' ≃+ N'<GOAL>⇑(AddMonoid.MulEquiv.coprodCongr e e') = ⇑(AddMonoid.Coprod.map ↑e ↑e')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>e : M ≃+ N<VAR>e' : M' ≃+ N'<GOAL>⇑(AddMonoid.MulEquiv.coprodCongr e e').symm = ⇑(AddMonoid.Coprod.map ↑e.symm ↑e'.symm)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>e : M ≃* N<VAR>e' : M' ≃* N'<GOAL>⇑(Monoid.MulEquiv.coprodCongr e e').symm = ⇑(Monoid.Coprod.map ↑e.symm ↑e'.symm)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>e : M ≃* N<VAR>e' : M' ≃* N'<GOAL>⇑(Monoid.MulEquiv.coprodCongr e e') = ⇑(Monoid.Coprod.map ↑e ↑e')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⇑(AddMonoid.MulEquiv.coprodComm M N) = ⇑(AddMonoid.Coprod.swap M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⇑(AddMonoid.MulEquiv.coprodComm M N).symm = ⇑(AddMonoid.Coprod.swap N M)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⇑(Monoid.MulEquiv.coprodComm M N).symm = ⇑(Monoid.Coprod.swap N M)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⇑(Monoid.MulEquiv.coprodComm M N) = ⇑(Monoid.Coprod.swap M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>x : M<GOAL>(AddMonoid.MulEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inl (AddMonoid.Coprod.inl x)) = AddMonoid.Coprod.inl x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>x : M<GOAL>(Monoid.MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inl (Monoid.Coprod.inl x)) = Monoid.Coprod.inl x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>x : N<GOAL>(Monoid.MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inl (Monoid.Coprod.inr x)) = Monoid.Coprod.inr (Monoid.Coprod.inl x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>x : N<GOAL>(AddMonoid.MulEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inl (AddMonoid.Coprod.inr x)) = AddMonoid.Coprod.inr (AddMonoid.Coprod.inl x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>x : P<GOAL>(AddMonoid.MulEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inr (AddMonoid.Coprod.inr x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>x : P<GOAL>(Monoid.MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inr x) = Monoid.Coprod.inr (Monoid.Coprod.inr x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>x : M<GOAL>(Monoid.MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inl x) = Monoid.Coprod.inl (Monoid.Coprod.inl x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>x : M<GOAL>(AddMonoid.MulEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inl (AddMonoid.Coprod.inl x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>x : N<GOAL>(Monoid.MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inr (Monoid.Coprod.inl x)) = Monoid.Coprod.inl (Monoid.Coprod.inr x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>x : N<GOAL>(AddMonoid.MulEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inr (AddMonoid.Coprod.inl x)) = AddMonoid.Coprod.inl (AddMonoid.Coprod.inr x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>x : P<GOAL>(AddMonoid.MulEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inr (AddMonoid.Coprod.inr x)) = AddMonoid.Coprod.inr x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>x : P<GOAL>(Monoid.MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inr (Monoid.Coprod.inr x)) = Monoid.Coprod.inr x
<VAR>M : Type u_1<VAR>Monoid M<GOAL>⇑(Monoid.MulEquiv.coprodPUnit M) = ⇑Monoid.Coprod.fst
<VAR>M : Type u_1<VAR>Monoid M<GOAL>⇑(Monoid.MulEquiv.coprodPUnit M).symm = ⇑Monoid.Coprod.inl
<VAR>M : Type u_1<VAR>Monoid M<GOAL>⇑(Monoid.MulEquiv.punitCoprod M) = ⇑Monoid.Coprod.snd
<VAR>M : Type u_1<VAR>Monoid M<GOAL>⇑(Monoid.MulEquiv.punitCoprod M).symm = ⇑Monoid.Coprod.inr
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>⇑Monoid.AddEquiv.coprodUnit = ⇑AddMonoid.Coprod.fst
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>⇑Monoid.AddEquiv.coprodUnit.symm = ⇑AddMonoid.Coprod.inl
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>⇑Monoid.AddEquiv.punitCoprod.symm = ⇑AddMonoid.Coprod.inr
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>⇑Monoid.AddEquiv.punitCoprod = ⇑AddMonoid.Coprod.snd
<VAR>α : Type u_1<VAR>Mul α<VAR>s : Set α<VAR>x : α<VAR>a : α<VAR>hxS : x ∈ s<GOAL>a * x ∈ a • s
<VAR>α : Type u_1<VAR>Add α<VAR>s : Set α<VAR>x : α<VAR>a : α<VAR>hxS : x ∈ s<GOAL>a + x ∈ a +ᵥ s
<VAR>α : Type u_1<VAR>Mul α<VAR>s : Set α<VAR>x : α<VAR>a : α<VAR>hxS : x ∈ s<GOAL>x * a ∈ MulOpposite.op a • s
<VAR>α : Type u_1<VAR>Add α<VAR>s : Set α<VAR>x : α<VAR>a : α<VAR>hxS : x ∈ s<GOAL>x + a ∈ AddOpposite.op a +ᵥ s
<VAR>α : Type u_1<VAR>Add α<VAR>s : Set α<GOAL>Equivalence (LeftAddCosetEquivalence s)
<VAR>α : Type u_1<VAR>Mul α<VAR>s : Set α<GOAL>Equivalence (LeftCosetEquivalence s)
<VAR>α : Type u_1<VAR>Mul α<VAR>s : Set α<GOAL>Equivalence (RightCosetEquivalence s)
<VAR>α : Type u_1<VAR>Add α<VAR>s : Set α<GOAL>Equivalence (RightAddCosetEquivalence s)
<VAR>α : Type u_1<VAR>Semigroup α<VAR>s : Set α<VAR>a b : α<GOAL>a • b • s = (a * b) • s
<VAR>α : Type u_1<VAR>AddSemigroup α<VAR>s : Set α<VAR>a b : α<GOAL>a +ᵥ (b +ᵥ s) = a + b +ᵥ s
<VAR>α : Type u_1<VAR>Semigroup α<VAR>s : Set α<VAR>a b : α<GOAL>MulOpposite.op b • MulOpposite.op a • s = MulOpposite.op (a * b) • s
<VAR>α : Type u_1<VAR>AddSemigroup α<VAR>s : Set α<VAR>a b : α<GOAL>AddOpposite.op b +ᵥ (AddOpposite.op a +ᵥ s) = AddOpposite.op (a + b) +ᵥ s
<VAR>α : Type u_1<VAR>AddSemigroup α<VAR>s : Set α<VAR>a b : α<GOAL>AddOpposite.op b +ᵥ (a +ᵥ s) = a +ᵥ (AddOpposite.op b +ᵥ s)
<VAR>α : Type u_1<VAR>Semigroup α<VAR>s : Set α<VAR>a b : α<GOAL>MulOpposite.op b • a • s = a • MulOpposite.op b • s
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>s : Set α<GOAL>0 +ᵥ s = s
<VAR>α : Type u_1<VAR>Monoid α<VAR>s : Set α<GOAL>1 • s = s
<VAR>α : Type u_1<VAR>Monoid α<VAR>s : Set α<GOAL>MulOpposite.op 1 • s = s
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>s : Set α<GOAL>AddOpposite.op 0 +ᵥ s = s
<VAR>α : Type u_1<VAR>Monoid α<VAR>s : Submonoid α<VAR>a : α<GOAL>a ∈ a • ↑s
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>s : AddSubmonoid α<VAR>a : α<GOAL>a ∈ a +ᵥ ↑s
<VAR>α : Type u_1<VAR>Monoid α<VAR>s : Submonoid α<VAR>a : α<GOAL>a ∈ MulOpposite.op a • ↑s
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>s : AddSubmonoid α<VAR>a : α<GOAL>a ∈ AddOpposite.op a +ᵥ ↑s
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>s : AddSubmonoid α<VAR>a : α<VAR>ha : a +ᵥ ↑s = ↑s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>Monoid α<VAR>s : Submonoid α<VAR>a : α<VAR>ha : a • ↑s = ↑s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>s : AddSubmonoid α<VAR>a : α<VAR>ha : AddOpposite.op a +ᵥ ↑s = ↑s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>Monoid α<VAR>s : Submonoid α<VAR>a : α<VAR>ha : MulOpposite.op a • ↑s = ↑s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : Set α<VAR>x : α<VAR>a : α<GOAL>x ∈ a +ᵥ s ↔ -a + x ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Set α<VAR>x : α<VAR>a : α<GOAL>x ∈ a • s ↔ a⁻¹ * x ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Set α<VAR>x : α<VAR>a : α<GOAL>x ∈ MulOpposite.op a • s ↔ x * a⁻¹ ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : Set α<VAR>x : α<VAR>a : α<GOAL>x ∈ AddOpposite.op a +ᵥ s ↔ x + -a ∈ s