ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → M →+ N<VAR>a : α<VAR>b : M<GOAL>(Finsupp.liftAddHom f) (Finsupp.single a b) = (f a) b
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → M →+ N<VAR>a : α<GOAL>(Finsupp.liftAddHom f).comp (Finsupp.singleAddHom a) = f a
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>P : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>g : N →+ P<VAR>f : α → M →+ N<GOAL>g.comp (Finsupp.liftAddHom f) = Finsupp.liftAddHom fun a => g.comp (f a)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>β : Type u_7<VAR>AddCommGroup β<VAR>AddCommGroup γ<VAR>f g : α →₀ β<VAR>h : α → β → γ<VAR>h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂<GOAL>(f - g).sum h = f.sum h - g.sum h
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>v : α →₀ M<VAR>f : α ↪ β<VAR>g : β → M → N<GOAL>(Finsupp.embDomain f v).prod g = v.prod fun a b => g (f a) b
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>v : α →₀ M<VAR>f : α ↪ β<VAR>g : β → M → N<GOAL>(Finsupp.embDomain f v).sum g = v.sum fun a b => g (f a) b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>s : Finset ι<VAR>g : ι → α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ (a : α), h a 0 = 0<VAR>h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂<GOAL>∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>CommMonoid N<VAR>s : Finset ι<VAR>g : ι → α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ (a : α), h a 0 = 1<VAR>h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂<GOAL>∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>N : Type u_10<VAR>P : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommMonoid P<VAR>f : α →₀ M<VAR>g : α → M → β →₀ N<VAR>h : β → N → P<VAR>h_zero : ∀ (a : β), h a 0 = 1<VAR>h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ * h a b₂<GOAL>(f.sum g).prod h = f.prod fun a b => (g a b).prod h
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>N : Type u_10<VAR>P : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>f : α →₀ M<VAR>g : α → M → β →₀ N<VAR>h : β → N → P<VAR>h_zero : ∀ (a : β), h a 0 = 0<VAR>h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂<GOAL>(f.sum g).sum h = f.sum fun a b => (g a b).sum h
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : Multiset (α →₀ M)<VAR>h : α → M → N<VAR>h₀ : ∀ (a : α), h a 0 = 0<VAR>h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂<GOAL>f.sum.sum h = (Multiset.map (fun g => g.sum h) f).sum
<VAR>α : Type u_16<VAR>ι : Type u_17<VAR>M : Type u_18<VAR>DecidableEq α<VAR>AddCommMonoid M<VAR>g : ι → α →₀ M<VAR>s : Finset ι<VAR>h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support<GOAL>(∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>β : Type u_7<VAR>M : Type u_8<VAR>Zero M<VAR>f : α →₀ M<VAR>m : β → γ<VAR>h : α → M → Multiset β<GOAL>Multiset.map m (f.sum h) = f.sum fun a b => Multiset.map m (h a b)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>h : α → M → Multiset N<GOAL>(f.sum h).sum = f.sum fun a b => (h a b).sum
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>f1 f2 : α →₀ M<VAR>hd : Disjoint f1.support f2.support<VAR>β : Type u_16<VAR>AddCommMonoid β<VAR>g : α → M → β<GOAL>(f1 + f2).sum g = f1.sum g + f2.sum g
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>f1 f2 : α →₀ M<VAR>hd : Disjoint f1.support f2.support<VAR>β : Type u_16<VAR>CommMonoid β<VAR>g : α → M → β<GOAL>(f1 + f2).prod g = f1.prod g * f2.prod g
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>CommMonoid N<VAR>f1 f2 : α →₀ M<VAR>g1 g2 : α → M → N<VAR>h1 : f1.support ⊆ f2.support<VAR>h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)<GOAL>f1.prod g1 ∣ f2.prod g2
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<GOAL>Finsupp.indicator s f = ∑ x ∈ s.attach, Finsupp.single (↑x) (f ↑x ⋯)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>s : Finset α<VAR>f : α → M<GOAL>(Finsupp.indicator s fun x x_1 => f x) = ∑ x ∈ s, Finsupp.single x (f x)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ s, h a 0 = 0<GOAL>(Finsupp.indicator s f).sum h = ∑ x ∈ s.attach, h (↑x) (f ↑x ⋯)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ s, h a 0 = 1<GOAL>(Finsupp.indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>s : Finset α<VAR>f : α → M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ s, h a 0 = 1<GOAL>(Finsupp.indicator s fun x x_1 => f x).prod h = ∏ x ∈ s, h x (f x)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>s : Finset α<VAR>f : α → M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ s, h a 0 = 0<GOAL>(Finsupp.indicator s fun x x_1 => f x).sum h = ∑ x ∈ s, h x (f x)
<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>σ : Fin n →₀ M<VAR>i : M<GOAL>((Finsupp.cons i σ).sum fun x e => e) = i + σ.sum fun x e => e
<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>n : ℕ<VAR>σ : Fin n →₀ M<VAR>i : M<VAR>f : Fin (n + 1) → M → N<VAR>h : ∀ (x : Fin (n + 1)), f x 0 = 0<GOAL>(Finsupp.cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>g : α → M → N<VAR>n₁ n₂ : N<VAR>a : α<VAR>ha : a ∈ f.support<VAR>h : g a (f a) * n₁ = g a (f a) * n₂<GOAL>f.prod g * n₁ = f.prod g * n₂
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>g : α → M → N<VAR>n₁ n₂ : N<VAR>a : α<VAR>ha : a ∈ f.support<VAR>h : g a (f a) + n₁ = g a (f a) + n₂<GOAL>f.sum g + n₁ = f.sum g + n₂
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_4<VAR>AddCommMonoid A<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i : ι<GOAL>(∑ k ∈ s, f k) i = ∑ k ∈ s, (f k) i
<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<GOAL>g.sum k x = g.sum fun i b => k i b x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_4<VAR>C : Type u_6<VAR>AddCommMonoid A<VAR>AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<GOAL>(∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t
<VAR>α : Type u_1<VAR>R : Type u_14<VAR>S : Type u_15<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>b : S<VAR>s : α →₀ R<VAR>f : α → R → S<GOAL>s.sum f * b = s.sum fun a c => f a c * b
<VAR>α : Type u_1<VAR>R : Type u_14<VAR>S : Type u_15<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>b : S<VAR>s : α →₀ R<VAR>f : α → R → S<GOAL>b * s.sum f = s.sum fun a c => b * f a c
<VAR>f : ℕ →₀ ℕ<VAR>nhf : 0 ∉ f.support<GOAL>0 < f.prod fun x x_1 => x ^ x_1
<VAR>α : Type u<VAR>x y : FreeAddMagma α<GOAL>x.add y = x + y
<VAR>α : Type u<VAR>x y : FreeMagma α<GOAL>x.mul y = x * y
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>f g : FreeMagma α →ₙ* β<VAR>h : ⇑f ∘ FreeMagma.of = ⇑g ∘ FreeMagma.of<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>f g : AddHom (FreeAddMagma α) β<VAR>h : ⇑f ∘ FreeAddMagma.of = ⇑g ∘ FreeAddMagma.of<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>F : FreeMagma α →ₙ* β<GOAL>∀ (a : α), FreeMagma.lift.symm F a = (⇑F ∘ FreeMagma.of) a
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>F : AddHom (FreeAddMagma α) β<GOAL>∀ (a : α), FreeAddMagma.lift.symm F a = (⇑F ∘ FreeAddMagma.of) a
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>f : α → β<VAR>x : α<GOAL>(FreeAddMagma.lift f) (FreeAddMagma.of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>f : α → β<VAR>x : α<GOAL>(FreeMagma.lift f) (FreeMagma.of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>f : α → β<GOAL>⇑(FreeAddMagma.lift f) ∘ FreeAddMagma.of = f
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>f : α → β<GOAL>⇑(FreeMagma.lift f) ∘ FreeMagma.of = f
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>f : FreeMagma α →ₙ* β<GOAL>FreeMagma.lift (⇑f ∘ FreeMagma.of) = f
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>f : AddHom (FreeAddMagma α) β<GOAL>FreeAddMagma.lift (⇑f ∘ FreeAddMagma.of) = f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeMagma.map f) (FreeMagma.of x) = FreeMagma.of (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeAddMagma.map f) (FreeAddMagma.of x) = FreeAddMagma.of (f x)
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeAddMagma α<GOAL>f <$> (x + y) = f <$> x + f <$> y
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeMagma α<GOAL>f <$> (x * y) = f <$> x * f <$> y
<VAR>α β : Type u<VAR>f : α → FreeAddMagma β<VAR>x : α<GOAL>pure x >>= f = f x
<VAR>α β : Type u<VAR>f : α → FreeMagma β<VAR>x : α<GOAL>pure x >>= f = f x
<VAR>α β : Type u<VAR>f : α → FreeAddMagma β<VAR>x y : FreeAddMagma α<GOAL>x + y >>= f = (x >>= f) + (y >>= f)
<VAR>α β : Type u<VAR>f : α → FreeMagma β<VAR>x y : FreeMagma α<GOAL>x * y >>= f = (x >>= f) * (y >>= f)
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeMagma α<GOAL>(Seq.seq (pure f) fun x_1 => x) = f <$> x
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeAddMagma α<GOAL>(Seq.seq (pure f) fun x_1 => x) = f <$> x
<VAR>α β : Type u<VAR>f g : FreeAddMagma (α → β)<VAR>x : FreeAddMagma α<GOAL>(Seq.seq (f + g) fun x_1 => x) = (Seq.seq f fun x_1 => x) + Seq.seq g fun x_1 => x
<VAR>α β : Type u<VAR>f g : FreeMagma (α → β)<VAR>x : FreeMagma α<GOAL>(Seq.seq (f * g) fun x_1 => x) = (Seq.seq f fun x_1 => x) * Seq.seq g fun x_1 => x
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>x : α<GOAL>traverse F (pure x) = pure <$> F x
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<GOAL>traverse F ∘ pure = fun x => pure <$> F x
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>x y : FreeMagma α<GOAL>traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>x y : FreeAddMagma α<GOAL>traverse F (x + y) = Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<GOAL>Function.comp (traverse F) ∘ HAdd.hAdd = fun x y => Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<GOAL>Function.comp (traverse F) ∘ HMul.hMul = fun x y => Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>x : FreeAddMagma α<GOAL>FreeAddMagma.traverse F x = traverse F x
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>x : FreeMagma α<GOAL>FreeMagma.traverse F x = traverse F x
<VAR>α : Type u<VAR>x y : FreeMagma α<GOAL>(Seq.seq ((fun x x_1 => x * x_1) <$> x) fun x => y) = x * y
<VAR>α : Type u<VAR>x y : FreeAddMagma α<GOAL>(Seq.seq ((fun x x_1 => x + x_1) <$> x) fun x => y) = x + y
<VAR>α : Type u<VAR>x : FreeAddMagma α<GOAL>0 < x.length
<VAR>α : Type u<VAR>x : FreeMagma α<GOAL>0 < x.length
<VAR>α : Type u<VAR>Mul α<VAR>x y z : α<GOAL>Quot.mk (Magma.AssocRel α) (x * y * z) = Quot.mk (Magma.AssocRel α) (x * (y * z))
<VAR>α : Type u<VAR>Add α<VAR>x y z : α<GOAL>Quot.mk (AddMagma.AssocRel α) (x + y + z) = Quot.mk (AddMagma.AssocRel α) (x + (y + z))
<VAR>α : Type u<VAR>Mul α<VAR>x y z w : α<GOAL>Quot.mk (Magma.AssocRel α) (x * (y * z * w)) = Quot.mk (Magma.AssocRel α) (x * (y * (z * w)))
<VAR>α : Type u<VAR>Add α<VAR>x y z w : α<GOAL>Quot.mk (AddMagma.AssocRel α) (x + (y + z + w)) = Quot.mk (AddMagma.AssocRel α) (x + (y + (z + w)))
<VAR>α : Type u<VAR>Add α<VAR>C : AddMagma.FreeAddSemigroup α → Prop<VAR>x : AddMagma.FreeAddSemigroup α<VAR>ih : ∀ (x : α), C (AddMagma.FreeAddSemigroup.of x)<GOAL>C x
<VAR>α : Type u<VAR>Mul α<VAR>C : Magma.AssocQuotient α → Prop<VAR>x : Magma.AssocQuotient α<VAR>ih : ∀ (x : α), C (Magma.AssocQuotient.of x)<GOAL>C x
<VAR>α : Type u<VAR>Mul α<VAR>β : Type v<VAR>Semigroup β<VAR>f g : Magma.AssocQuotient α →ₙ* β<VAR>h : f.comp Magma.AssocQuotient.of = g.comp Magma.AssocQuotient.of<GOAL>f = g
<VAR>α : Type u<VAR>Add α<VAR>β : Type v<VAR>AddSemigroup β<VAR>f g : AddHom (AddMagma.FreeAddSemigroup α) β<VAR>h : f.comp AddMagma.FreeAddSemigroup.of = g.comp AddMagma.FreeAddSemigroup.of<GOAL>f = g
<VAR>α : Type u<VAR>Mul α<VAR>β : Type v<VAR>Semigroup β<VAR>f : Magma.AssocQuotient α →ₙ* β<GOAL>Magma.AssocQuotient.lift.symm f = f.comp Magma.AssocQuotient.of
<VAR>α : Type u<VAR>Add α<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : AddHom (AddMagma.FreeAddSemigroup α) β<GOAL>AddMagma.FreeAddSemigroup.lift.symm f = f.comp AddMagma.FreeAddSemigroup.of
<VAR>α : Type u<VAR>Add α<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : AddHom α β<VAR>x : α<GOAL>(AddMagma.FreeAddSemigroup.lift f) (AddMagma.FreeAddSemigroup.of x) = f x
<VAR>α : Type u<VAR>Mul α<VAR>β : Type v<VAR>Semigroup β<VAR>f : α →ₙ* β<VAR>x : α<GOAL>(Magma.AssocQuotient.lift f) (Magma.AssocQuotient.of x) = f x
<VAR>α : Type u<VAR>Add α<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : AddHom α β<GOAL>(AddMagma.FreeAddSemigroup.lift f).comp AddMagma.FreeAddSemigroup.of = f
<VAR>α : Type u<VAR>Mul α<VAR>β : Type v<VAR>Semigroup β<VAR>f : α →ₙ* β<GOAL>(Magma.AssocQuotient.lift f).comp Magma.AssocQuotient.of = f
<VAR>α : Type u<VAR>Add α<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : AddHom (AddMagma.FreeAddSemigroup α) β<GOAL>AddMagma.FreeAddSemigroup.lift (f.comp AddMagma.FreeAddSemigroup.of) = f
<VAR>α : Type u<VAR>Mul α<VAR>β : Type v<VAR>Semigroup β<VAR>f : Magma.AssocQuotient α →ₙ* β<GOAL>Magma.AssocQuotient.lift (f.comp Magma.AssocQuotient.of) = f
<VAR>α : Type u<VAR>Add α<VAR>β : Type v<VAR>Add β<VAR>f : AddHom α β<VAR>x : α<GOAL>(AddMagma.FreeAddSemigroup.map f) (AddMagma.FreeAddSemigroup.of x) = AddMagma.FreeAddSemigroup.of (f x)
<VAR>α : Type u<VAR>Mul α<VAR>β : Type v<VAR>Mul β<VAR>f : α →ₙ* β<VAR>x : α<GOAL>(Magma.AssocQuotient.map f) (Magma.AssocQuotient.of x) = Magma.AssocQuotient.of (f x)
<VAR>α : Type u<VAR>x y : FreeAddSemigroup α<GOAL>(x + y).head = x.head
<VAR>α : Type u<VAR>x y : FreeSemigroup α<GOAL>(x * y).head = x.head
<VAR>α : Type u<VAR>x y : FreeSemigroup α<GOAL>(x * y).tail = x.tail ++ y.head :: y.tail
<VAR>α : Type u<VAR>x y : FreeAddSemigroup α<GOAL>(x + y).tail = x.tail ++ y.head :: y.tail
<VAR>α : Type u<VAR>x y : α<VAR>L1 L2 : List α<GOAL>{ head := x, tail := L1 } + { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
<VAR>α : Type u<VAR>x y : α<VAR>L1 L2 : List α<GOAL>{ head := x, tail := L1 } * { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
<VAR>α : Type u<VAR>x : α<GOAL>(FreeAddSemigroup.of x).tail = []
<VAR>α : Type u<VAR>x : α<GOAL>(FreeSemigroup.of x).tail = []
<VAR>α : Type u<VAR>x : α<GOAL>(FreeAddSemigroup.of x).head = x
<VAR>α : Type u<VAR>x : α<GOAL>(FreeSemigroup.of x).head = x
<VAR>α : Type u<VAR>x y : FreeAddSemigroup α<GOAL>(x + y).length = x.length + y.length
<VAR>α : Type u<VAR>x : α<GOAL>(FreeAddSemigroup.of x).length = 1
<VAR>α : Type u<VAR>x : α<GOAL>(FreeSemigroup.of x).length = 1
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>f g : AddHom (FreeAddSemigroup α) β<VAR>h : ⇑f ∘ FreeAddSemigroup.of = ⇑g ∘ FreeAddSemigroup.of<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>f g : FreeSemigroup α →ₙ* β<VAR>h : ⇑f ∘ FreeSemigroup.of = ⇑g ∘ FreeSemigroup.of<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>Semigroup β<VAR>f : FreeSemigroup α →ₙ* β<GOAL>∀ (a : α), FreeSemigroup.lift.symm f a = (⇑f ∘ FreeSemigroup.of) a
<VAR>α : Type u<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : AddHom (FreeAddSemigroup α) β<GOAL>∀ (a : α), FreeAddSemigroup.lift.symm f a = (⇑f ∘ FreeAddSemigroup.of) a
<VAR>α : Type u<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : α → β<VAR>x : α<GOAL>(FreeAddSemigroup.lift f) (FreeAddSemigroup.of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>Semigroup β<VAR>f : α → β<VAR>x : α<GOAL>(FreeSemigroup.lift f) (FreeSemigroup.of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>Semigroup β<VAR>f : α → β<GOAL>⇑(FreeSemigroup.lift f) ∘ FreeSemigroup.of = f
<VAR>α : Type u<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : α → β<GOAL>⇑(FreeAddSemigroup.lift f) ∘ FreeAddSemigroup.of = f
<VAR>α : Type u<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : AddHom (FreeAddSemigroup α) β<GOAL>FreeAddSemigroup.lift (⇑f ∘ FreeAddSemigroup.of) = f
<VAR>α : Type u<VAR>β : Type v<VAR>Semigroup β<VAR>f : FreeSemigroup α →ₙ* β<GOAL>FreeSemigroup.lift (⇑f ∘ FreeSemigroup.of) = f
<VAR>α : Type u<VAR>β : Type v<VAR>Semigroup β<VAR>f : α → β<VAR>x : α<VAR>y : FreeSemigroup α<GOAL>(FreeSemigroup.lift f) (FreeSemigroup.of x * y) = f x * (FreeSemigroup.lift f) y
<VAR>α : Type u<VAR>β : Type v<VAR>AddSemigroup β<VAR>f : α → β<VAR>x : α<VAR>y : FreeAddSemigroup α<GOAL>(FreeAddSemigroup.lift f) (FreeAddSemigroup.of x + y) = f x + (FreeAddSemigroup.lift f) y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeAddSemigroup.map f) (FreeAddSemigroup.of x) = FreeAddSemigroup.of (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeSemigroup.map f) (FreeSemigroup.of x) = FreeSemigroup.of (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeAddSemigroup α<GOAL>((FreeAddSemigroup.map f) x).length = x.length
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeSemigroup α<GOAL>((FreeSemigroup.map f) x).length = x.length
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeSemigroup α<GOAL>f <$> (x * y) = f <$> x * f <$> y
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeAddSemigroup α<GOAL>f <$> (x + y) = f <$> x + f <$> y
<VAR>α β : Type u<VAR>f : α → FreeSemigroup β<VAR>x : α<GOAL>pure x >>= f = f x
<VAR>α β : Type u<VAR>f : α → FreeAddSemigroup β<VAR>x : α<GOAL>pure x >>= f = f x
<VAR>α β : Type u<VAR>f : α → FreeSemigroup β<VAR>x y : FreeSemigroup α<GOAL>x * y >>= f = (x >>= f) * (y >>= f)
<VAR>α β : Type u<VAR>f : α → FreeAddSemigroup β<VAR>x y : FreeAddSemigroup α<GOAL>x + y >>= f = (x >>= f) + (y >>= f)
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeAddSemigroup α<GOAL>(Seq.seq (pure f) fun x_1 => x) = f <$> x
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeSemigroup α<GOAL>(Seq.seq (pure f) fun x_1 => x) = f <$> x
<VAR>α β : Type u<VAR>f g : FreeSemigroup (α → β)<VAR>x : FreeSemigroup α<GOAL>(Seq.seq (f * g) fun x_1 => x) = (Seq.seq f fun x_1 => x) * Seq.seq g fun x_1 => x
<VAR>α β : Type u<VAR>f g : FreeAddSemigroup (α → β)<VAR>x : FreeAddSemigroup α<GOAL>(Seq.seq (f + g) fun x_1 => x) = (Seq.seq f fun x_1 => x) + Seq.seq g fun x_1 => x
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>LawfulApplicative m<VAR>x y : FreeAddSemigroup α<GOAL>traverse F (x + y) = Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>LawfulApplicative m<VAR>x y : FreeSemigroup α<GOAL>traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>LawfulApplicative m<GOAL>Function.comp (traverse F) ∘ HAdd.hAdd = fun x y => Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>LawfulApplicative m<GOAL>Function.comp (traverse F) ∘ HMul.hMul = fun x y => Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>x : FreeSemigroup α<GOAL>FreeSemigroup.traverse F x = traverse F x
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Applicative m<VAR>F : α → m β<VAR>x : FreeAddSemigroup α<GOAL>FreeAddSemigroup.traverse F x = traverse F x
<VAR>α : Type u<VAR>x y : FreeAddSemigroup α<GOAL>(Seq.seq ((fun x x_1 => x + x_1) <$> x) fun x => y) = x + y
<VAR>α : Type u<VAR>x y : FreeSemigroup α<GOAL>(Seq.seq ((fun x x_1 => x * x_1) <$> x) fun x => y) = x * y
<VAR>α : Type u<VAR>x : α<GOAL>FreeMagma.toFreeSemigroup (FreeMagma.of x) = FreeSemigroup.of x
<VAR>α : Type u<VAR>x : α<GOAL>FreeAddMagma.toFreeAddSemigroup (FreeAddMagma.of x) = FreeAddSemigroup.of x
<VAR>α : Type u<GOAL>⇑FreeMagma.toFreeSemigroup ∘ FreeMagma.of = FreeSemigroup.of
<VAR>α : Type u<GOAL>⇑FreeAddMagma.toFreeAddSemigroup ∘ FreeAddMagma.of = FreeAddSemigroup.of
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>FreeMagma.toFreeSemigroup.comp (FreeMagma.map f) = (FreeSemigroup.map f).comp FreeMagma.toFreeSemigroup
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>FreeAddMagma.toFreeAddSemigroup.comp (FreeAddMagma.map f) = (FreeAddSemigroup.map f).comp FreeAddMagma.toFreeAddSemigroup
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeAddMagma α<GOAL>FreeAddMagma.toFreeAddSemigroup ((FreeAddMagma.map f) x) = (FreeAddSemigroup.map f) (FreeAddMagma.toFreeAddSemigroup x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeMagma α<GOAL>FreeMagma.toFreeSemigroup ((FreeMagma.map f) x) = (FreeSemigroup.map f) (FreeMagma.toFreeSemigroup x)
<VAR>α : Type u<VAR>x : FreeAddMagma α<GOAL>(FreeAddMagma.toFreeAddSemigroup x).length = x.length
<VAR>α : Type u<VAR>x : FreeMagma α<GOAL>(FreeMagma.toFreeSemigroup x).length = x.length
<VAR>α : Type u_1<VAR>x : α<GOAL>(Thunk.pure x).get = x
<VAR>α : Type u_1<VAR>f : Unit → α<GOAL>{ fn := f }.get = f ()
<VAR>α : Type u<VAR>β : Type v<VAR>a : Thunk α<VAR>b : Thunk β<GOAL>(a.prod b).get.fst = a.get
<VAR>α : Type u<VAR>β : Type v<VAR>a : Thunk α<VAR>b : Thunk β<GOAL>(a.prod b).get.snd = b.get
<VAR>α : Type u<VAR>Add α<VAR>a b : Thunk α<GOAL>(a + b).get = a.get + b.get
<VAR>α : Type u<VAR>β : Type v<VAR>Semiring α<VAR>Semiring β<VAR>f : α → β<VAR>self : IsSemiringHom f<VAR>x y : α<GOAL>f (x + y) = f x + f y
<VAR>α : Type u<VAR>β : Type v<VAR>Semiring α<VAR>Semiring β<VAR>f : α → β<VAR>self : IsSemiringHom f<VAR>x y : α<GOAL>f (x * y) = f x * f y
<VAR>α : Type u<VAR>β : Type v<VAR>Semiring α<VAR>Semiring β<VAR>f : α → β<VAR>self : IsSemiringHom f<GOAL>f 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>Semiring α<VAR>Semiring β<VAR>f : α → β<VAR>self : IsSemiringHom f<GOAL>f 0 = 0
<VAR>α : Type u<VAR>Semiring α<GOAL>IsSemiringHom id
<VAR>α : Type u<VAR>β : Type v<VAR>Semiring α<VAR>Semiring β<VAR>f : α → β<VAR>hf : IsSemiringHom f<VAR>γ : Type u_1<VAR>Semiring γ<VAR>g : β → γ<VAR>hg : IsSemiringHom g<GOAL>IsSemiringHom (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>Semiring α<VAR>Semiring β<VAR>f : α → β<VAR>hf : IsSemiringHom f<GOAL>IsAddMonoidHom f
<VAR>α : Type u<VAR>β : Type v<VAR>Semiring α<VAR>Semiring β<VAR>f : α → β<VAR>hf : IsSemiringHom f<GOAL>IsMonoidHom f
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>self : IsRingHom f<VAR>x y : α<GOAL>f (x * y) = f x * f y
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>self : IsRingHom f<VAR>x y : α<GOAL>f (x + y) = f x + f y
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>self : IsRingHom f<GOAL>f 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>H : IsSemiringHom f<GOAL>IsRingHom f
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>hf : IsRingHom f<GOAL>f 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>x : α<VAR>hf : IsRingHom f<GOAL>f (-x) = -f x
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>x y : α<VAR>hf : IsRingHom f<GOAL>f (x - y) = f x - f y
<VAR>α : Type u<VAR>Ring α<GOAL>IsRingHom id
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>hf : IsRingHom f<VAR>γ : Type u_1<VAR>Ring γ<VAR>g : β → γ<VAR>hg : IsRingHom g<GOAL>IsRingHom (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>hf : IsRingHom f<GOAL>IsSemiringHom f