ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hHK : H.relindex K ≠ 0<VAR>hKL : K.relindex L ≠ 0<GOAL>H.relindex L ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hHK : H.relindex K ≠ 0<VAR>hKL : K.relindex L ≠ 0<GOAL>H.relindex L ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hH : H.relindex L ≠ 0<VAR>hK : K.relindex L ≠ 0<GOAL>(H ⊓ K).relindex L ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hH : H.relindex L ≠ 0<VAR>hK : K.relindex L ≠ 0<GOAL>(H ⊓ K).relindex L ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>hH : H.index ≠ 0<VAR>hK : K.index ≠ 0<GOAL>(H ⊓ K).index ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hH : H.index ≠ 0<VAR>hK : K.index ≠ 0<GOAL>(H ⊓ K).index ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<GOAL>(H ⊓ K).relindex L ≤ H.relindex L * K.relindex L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<GOAL>(H ⊓ K).relindex L ≤ H.relindex L * K.relindex L
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>(H ⊓ K).index ≤ H.index * K.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>(H ⊓ K).index ≤ H.index * K.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>L : AddSubgroup G<VAR>ι : Type u_3<VAR>_hι : Finite ι<VAR>f : ι → AddSubgroup G<VAR>hf : ∀ (i : ι), (f i).relindex L ≠ 0<GOAL>(⨅ i, f i).relindex L ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>L : Subgroup G<VAR>ι : Type u_3<VAR>_hι : Finite ι<VAR>f : ι → Subgroup G<VAR>hf : ∀ (i : ι), (f i).relindex L ≠ 0<GOAL>(⨅ i, f i).relindex L ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>L : AddSubgroup G<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : ι → AddSubgroup G<GOAL>(⨅ i, f i).relindex L ≤ ∏ i : ι, (f i).relindex L
<VAR>G : Type u_1<VAR>Group G<VAR>L : Subgroup G<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : ι → Subgroup G<GOAL>(⨅ i, f i).relindex L ≤ ∏ i : ι, (f i).relindex L
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_3<VAR>Finite ι<VAR>f : ι → Subgroup G<VAR>hf : ∀ (i : ι), (f i).index ≠ 0<GOAL>(⨅ i, f i).index ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_3<VAR>Finite ι<VAR>f : ι → AddSubgroup G<VAR>hf : ∀ (i : ι), (f i).index ≠ 0<GOAL>(⨅ i, f i).index ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : ι → Subgroup G<GOAL>(⨅ i, f i).index ≤ ∏ i : ι, (f i).index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : ι → AddSubgroup G<GOAL>(⨅ i, f i).index ≤ ∏ i : ι, (f i).index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.index = 1 ↔ H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.index = 1 ↔ H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>H.relindex K = 1 ↔ K ≤ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>H.relindex K = 1 ↔ K ≤ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>Nat.card ↥H = 1 ↔ H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Nat.card ↥H = 1 ↔ H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>hH : Finite (G ⧸ H)<GOAL>H.index ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hH : Finite (G ⧸ H)<GOAL>H.index ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite (G ⧸ H)<VAR>hH : H ≠ ⊤<GOAL>1 < H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite (G ⧸ H)<VAR>hH : H ≠ ⊤<GOAL>1 < H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>self : H.FiniteIndex<GOAL>H.index ≠ 0
<VAR>G : Type u_3<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>self : H.FiniteIndex<GOAL>H.index ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite (G ⧸ H)<GOAL>H.FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite (G ⧸ H)<GOAL>H.FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_3<VAR>Finite ι<VAR>f : ι → AddSubgroup G<VAR>hf : ∀ (i : ι), (f i).FiniteIndex<GOAL>(⨅ i, f i).FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_3<VAR>Finite ι<VAR>f : ι → Subgroup G<VAR>hf : ∀ (i : ι), (f i).FiniteIndex<GOAL>(⨅ i, f i).FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → AddSubgroup G<VAR>hs : ∀ i ∈ s, (f i).FiniteIndex<GOAL>(⨅ i ∈ s, f i).FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → Subgroup G<VAR>hs : ∀ i ∈ s, (f i).FiniteIndex<GOAL>(⨅ i ∈ s, f i).FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>H.FiniteIndex<VAR>h : H ≤ K<GOAL>K.FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>H.FiniteIndex<VAR>h : H ≤ K<GOAL>K.FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>Finite ↑(commutatorSet G)<VAR>Group.FG G<GOAL>(Subgroup.center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>Group G<VAR>Fintype G<VAR>Monoid M<VAR>DecidableEq M<VAR>FunLike F G M<VAR>MonoidHomClass F G M<VAR>f : F<VAR>x y : M<VAR>hx : x ∈ Set.range ⇑f<VAR>hy : y ∈ Set.range ⇑f<GOAL>(Finset.filter (fun g => f g = x) Finset.univ).card = (Finset.filter (fun g => f g = y) Finset.univ).card
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>AddGroup G<VAR>Fintype G<VAR>AddMonoid M<VAR>DecidableEq M<VAR>FunLike F G M<VAR>AddMonoidHomClass F G M<VAR>f : F<VAR>x y : M<VAR>hx : x ∈ Set.range ⇑f<VAR>hy : y ∈ Set.range ⇑f<GOAL>(Finset.filter (fun g => f g = x) Finset.univ).card = (Finset.filter (fun g => f g = y) Finset.univ).card
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Con.ker Monoid.Coprod.mk = Monoid.coprodCon M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddCon.ker AddMonoid.Coprod.mk = AddMonoid.coprodCon M N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Function.Surjective ⇑Monoid.Coprod.mk
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Function.Surjective ⇑AddMonoid.Coprod.mk
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange AddMonoid.Coprod.mk = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange Monoid.Coprod.mk = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>w₁ w₂ : FreeMonoid (M ⊕ N)<GOAL>Monoid.Coprod.mk w₁ = Monoid.Coprod.mk w₂ ↔ (Monoid.coprodCon M N) w₁ w₂
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>w₁ w₂ : FreeAddMonoid (M ⊕ N)<GOAL>AddMonoid.Coprod.mk w₁ = AddMonoid.Coprod.mk w₂ ↔ (AddMonoid.coprodCon M N) w₁ w₂
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : M<GOAL>AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl x)) = AddMonoid.Coprod.inl x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : M<GOAL>Monoid.Coprod.mk (FreeMonoid.of (Sum.inl x)) = Monoid.Coprod.inl x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : N<GOAL>Monoid.Coprod.mk (FreeMonoid.of (Sum.inr x)) = Monoid.Coprod.inr x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : N<GOAL>AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr x)) = AddMonoid.Coprod.inr x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>C : AddMonoid.Coprod M N → Prop<VAR>m : AddMonoid.Coprod M N<VAR>one : C 0<VAR>inl_mul : ∀ (m : M) (x : AddMonoid.Coprod M N), C x → C (AddMonoid.Coprod.inl m + x)<VAR>inr_mul : ∀ (n : N) (x : AddMonoid.Coprod M N), C x → C (AddMonoid.Coprod.inr n + x)<GOAL>C m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>C : Monoid.Coprod M N → Prop<VAR>m : Monoid.Coprod M N<VAR>one : C 1<VAR>inl_mul : ∀ (m : M) (x : Monoid.Coprod M N), C x → C (Monoid.Coprod.inl m * x)<VAR>inr_mul : ∀ (n : N) (x : Monoid.Coprod M N), C x → C (Monoid.Coprod.inr n * x)<GOAL>C m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>C : AddMonoid.Coprod M N → Prop<VAR>m : AddMonoid.Coprod M N<VAR>inl : ∀ (m : M), C (AddMonoid.Coprod.inl m)<VAR>inr : ∀ (n : N), C (AddMonoid.Coprod.inr n)<VAR>mul : ∀ (x y : AddMonoid.Coprod M N), C x → C y → C (x + y)<GOAL>C m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>C : Monoid.Coprod M N → Prop<VAR>m : Monoid.Coprod M N<VAR>inl : ∀ (m : M), C (Monoid.Coprod.inl m)<VAR>inr : ∀ (n : N), C (Monoid.Coprod.inr n)<VAR>mul : ∀ (x y : Monoid.Coprod M N), C x → C y → C (x * y)<GOAL>C m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : FreeMonoid (M ⊕ N) →* P<VAR>hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1<VAR>hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1<VAR>hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))<VAR>x : M<GOAL>(Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inl x) = f (FreeMonoid.of (Sum.inl x))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : FreeAddMonoid (M ⊕ N) →+ P<VAR>hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0<VAR>hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0<VAR>hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))<VAR>x : M<GOAL>(AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inl x) = f (FreeAddMonoid.of (Sum.inl x))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : FreeAddMonoid (M ⊕ N) →+ P<VAR>hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0<VAR>hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0<VAR>hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))<VAR>x : N<GOAL>(AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inr x) = f (FreeAddMonoid.of (Sum.inr x))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : FreeMonoid (M ⊕ N) →* P<VAR>hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1<VAR>hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1<VAR>hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))<VAR>x : N<GOAL>(Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inr x) = f (FreeMonoid.of (Sum.inr x))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : FreeMonoid (M ⊕ N) →* P<VAR>hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1<VAR>hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1<VAR>hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))<VAR>w : FreeMonoid (M ⊕ N)<GOAL>(Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.mk w) = f w
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : FreeAddMonoid (M ⊕ N) →+ P<VAR>hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0<VAR>hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0<VAR>hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))<VAR>w : FreeAddMonoid (M ⊕ N)<GOAL>(AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.mk w) = f w
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : FreeMonoid (M ⊕ N) →* P<VAR>hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1<VAR>hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1<VAR>hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))<GOAL>(Monoid.Coprod.clift f hM₁ hN₁ hM hN).comp Monoid.Coprod.mk = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : FreeAddMonoid (M ⊕ N) →+ P<VAR>hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0<VAR>hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0<VAR>hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))<VAR>hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))<GOAL>(AddMonoid.Coprod.clift f hM₁ hN₁ hM hN).comp AddMonoid.Coprod.mk = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Submonoid.closure (Set.range ⇑Monoid.Coprod.inl ∪ Set.range ⇑Monoid.Coprod.inr) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddSubmonoid.closure (Set.range ⇑AddMonoid.Coprod.inl ∪ Set.range ⇑AddMonoid.Coprod.inr) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange Monoid.Coprod.inl ⊔ MonoidHom.mrange Monoid.Coprod.inr = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange AddMonoid.Coprod.inl ⊔ AddMonoidHom.mrange AddMonoid.Coprod.inr = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Codisjoint (AddMonoidHom.mrange AddMonoid.Coprod.inl) (AddMonoidHom.mrange AddMonoid.Coprod.inr)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Codisjoint (MonoidHom.mrange Monoid.Coprod.inl) (MonoidHom.mrange Monoid.Coprod.inr)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : Monoid.Coprod M N →* P<GOAL>MonoidHom.mrange f = MonoidHom.mrange (f.comp Monoid.Coprod.inl) ⊔ MonoidHom.mrange (f.comp Monoid.Coprod.inr)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : AddMonoid.Coprod M N →+ P<GOAL>AddMonoidHom.mrange f = AddMonoidHom.mrange (f.comp AddMonoid.Coprod.inl) ⊔ AddMonoidHom.mrange (f.comp AddMonoid.Coprod.inr)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f g : AddMonoid.Coprod M N →+ P<VAR>h₁ : f.comp AddMonoid.Coprod.inl = g.comp AddMonoid.Coprod.inl<VAR>h₂ : f.comp AddMonoid.Coprod.inr = g.comp AddMonoid.Coprod.inr<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f g : Monoid.Coprod M N →* P<VAR>h₁ : f.comp Monoid.Coprod.inl = g.comp Monoid.Coprod.inl<VAR>h₂ : f.comp Monoid.Coprod.inr = g.comp Monoid.Coprod.inr<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Monoid.Coprod.clift Monoid.Coprod.mk ⋯ ⋯ ⋯ ⋯ = MonoidHom.id (Monoid.Coprod M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoid.Coprod.clift AddMonoid.Coprod.mk ⋯ ⋯ ⋯ ⋯ = AddMonoidHom.id (AddMonoid.Coprod M N)
<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>f : M →* M'<VAR>g : N →* N'<VAR>l : List (M ⊕ N)<GOAL>(Monoid.Coprod.map f g) (Monoid.Coprod.mk (FreeMonoid.ofList l)) = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map ⇑f ⇑g) l))
<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>f : M →+ M'<VAR>g : N →+ N'<VAR>l : List (M ⊕ N)<GOAL>(AddMonoid.Coprod.map f g) (AddMonoid.Coprod.mk (FreeAddMonoid.ofList l)) = AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map ⇑f ⇑g) l))
<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>f : M →+ M'<VAR>g : N →+ N'<VAR>x : M<GOAL>(AddMonoid.Coprod.map f g) (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inl (f x)
<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>f : M →* M'<VAR>g : N →* N'<VAR>x : M<GOAL>(Monoid.Coprod.map f g) (Monoid.Coprod.inl x) = Monoid.Coprod.inl (f x)
<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>f : M →* M'<VAR>g : N →* N'<VAR>x : N<GOAL>(Monoid.Coprod.map f g) (Monoid.Coprod.inr x) = Monoid.Coprod.inr (g x)
<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>f : M →+ M'<VAR>g : N →+ N'<VAR>x : N<GOAL>(AddMonoid.Coprod.map f g) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inr (g x)
<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>f : M →* M'<VAR>g : N →* N'<GOAL>(Monoid.Coprod.map f g).comp Monoid.Coprod.inl = Monoid.Coprod.inl.comp f
<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>f : M →+ M'<VAR>g : N →+ N'<GOAL>(AddMonoid.Coprod.map f g).comp AddMonoid.Coprod.inl = AddMonoid.Coprod.inl.comp f
<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>f : M →+ M'<VAR>g : N →+ N'<GOAL>(AddMonoid.Coprod.map f g).comp AddMonoid.Coprod.inr = AddMonoid.Coprod.inr.comp g
<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>f : M →* M'<VAR>g : N →* N'<GOAL>(Monoid.Coprod.map f g).comp Monoid.Coprod.inr = Monoid.Coprod.inr.comp g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoid.Coprod.map (AddMonoidHom.id M) (AddMonoidHom.id N) = AddMonoidHom.id (AddMonoid.Coprod M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Monoid.Coprod.map (MonoidHom.id M) (MonoidHom.id N) = MonoidHom.id (Monoid.Coprod M N)
<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>M'' : Type u_6<VAR>N'' : Type u_7<VAR>MulOneClass M''<VAR>MulOneClass N''<VAR>f' : M' →* M''<VAR>g' : N' →* N''<VAR>f : M →* M'<VAR>g : N →* N'<GOAL>(Monoid.Coprod.map f' g').comp (Monoid.Coprod.map f g) = Monoid.Coprod.map (f'.comp f) (g'.comp g)
<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>M'' : Type u_6<VAR>N'' : Type u_7<VAR>AddZeroClass M''<VAR>AddZeroClass N''<VAR>f' : M' →+ M''<VAR>g' : N' →+ N''<VAR>f : M →+ M'<VAR>g : N →+ N'<GOAL>(AddMonoid.Coprod.map f' g').comp (AddMonoid.Coprod.map f g) = AddMonoid.Coprod.map (f'.comp f) (g'.comp g)
<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>M'' : Type u_6<VAR>N'' : Type u_7<VAR>MulOneClass M''<VAR>MulOneClass N''<VAR>f' : M' →* M''<VAR>g' : N' →* N''<VAR>f : M →* M'<VAR>g : N →* N'<VAR>x : Monoid.Coprod M N<GOAL>(Monoid.Coprod.map f' g') ((Monoid.Coprod.map f g) x) = (Monoid.Coprod.map (f'.comp f) (g'.comp g)) x
<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>M'' : Type u_6<VAR>N'' : Type u_7<VAR>AddZeroClass M''<VAR>AddZeroClass N''<VAR>f' : M' →+ M''<VAR>g' : N' →+ N''<VAR>f : M →+ M'<VAR>g : N →+ N'<VAR>x : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.map f' g') ((AddMonoid.Coprod.map f g) x) = (AddMonoid.Coprod.map (f'.comp f) (g'.comp g)) x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>(AddMonoid.Coprod.swap M N).comp (AddMonoid.Coprod.swap N M) = AddMonoidHom.id (AddMonoid.Coprod N M)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>(Monoid.Coprod.swap M N).comp (Monoid.Coprod.swap N M) = MonoidHom.id (Monoid.Coprod N M)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : Monoid.Coprod M N<GOAL>(Monoid.Coprod.swap N M) ((Monoid.Coprod.swap M N) x) = x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.swap N M) ((AddMonoid.Coprod.swap M N) x) = x
<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>f : M →+ M'<VAR>g : N →+ N'<GOAL>(AddMonoid.Coprod.swap M' N').comp (AddMonoid.Coprod.map f g) = (AddMonoid.Coprod.map g f).comp (AddMonoid.Coprod.swap M N)
<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>f : M →* M'<VAR>g : N →* N'<GOAL>(Monoid.Coprod.swap M' N').comp (Monoid.Coprod.map f g) = (Monoid.Coprod.map g f).comp (Monoid.Coprod.swap M N)
<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>f : M →+ M'<VAR>g : N →+ N'<VAR>x : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.swap M' N') ((AddMonoid.Coprod.map f g) x) = (AddMonoid.Coprod.map g f) ((AddMonoid.Coprod.swap M N) x)
<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>f : M →* M'<VAR>g : N →* N'<VAR>x : Monoid.Coprod M N<GOAL>(Monoid.Coprod.swap M' N') ((Monoid.Coprod.map f g) x) = (Monoid.Coprod.map g f) ((Monoid.Coprod.swap M N) x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>(Monoid.Coprod.swap M N).comp Monoid.Coprod.inl = Monoid.Coprod.inr
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>(AddMonoid.Coprod.swap M N).comp AddMonoid.Coprod.inl = AddMonoid.Coprod.inr
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : M<GOAL>(Monoid.Coprod.swap M N) (Monoid.Coprod.inl x) = Monoid.Coprod.inr x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : M<GOAL>(AddMonoid.Coprod.swap M N) (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inr x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>(AddMonoid.Coprod.swap M N).comp AddMonoid.Coprod.inr = AddMonoid.Coprod.inl
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>(Monoid.Coprod.swap M N).comp Monoid.Coprod.inr = Monoid.Coprod.inl
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : N<GOAL>(Monoid.Coprod.swap M N) (Monoid.Coprod.inr x) = Monoid.Coprod.inl x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : N<GOAL>(AddMonoid.Coprod.swap M N) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inl x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Function.Injective ⇑(Monoid.Coprod.swap M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Function.Injective ⇑(AddMonoid.Coprod.swap M N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x y : Monoid.Coprod M N<GOAL>(Monoid.Coprod.swap M N) x = (Monoid.Coprod.swap M N) y ↔ x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x y : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.swap M N) x = (AddMonoid.Coprod.swap M N) y ↔ x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : AddMonoid.Coprod M N<GOAL>(AddMonoid.Coprod.swap M N) x = 0 ↔ x = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : Monoid.Coprod M N<GOAL>(Monoid.Coprod.swap M N) x = 1 ↔ x = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Function.Surjective ⇑(AddMonoid.Coprod.swap M N)