ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>x : α →₀ M<VAR>a : β<VAR>h : a ∉ Set.range f<GOAL>(Finsupp.mapDomain f x) a = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>v : α →₀ M<GOAL>Finsupp.mapDomain id v = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>v : α →₀ M<VAR>f : α → β<VAR>g : β → γ<GOAL>Finsupp.mapDomain (g ∘ f) v = Finsupp.mapDomain g (Finsupp.mapDomain f v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>a : α<VAR>b : M<GOAL>Finsupp.mapDomain f (Finsupp.single a b) = Finsupp.single (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<GOAL>Finsupp.mapDomain f 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>v : α →₀ M<VAR>f g : α → β<VAR>h : ∀ x ∈ v.support, f x = g x<GOAL>Finsupp.mapDomain f v = Finsupp.mapDomain g v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>v₁ v₂ : α →₀ M<VAR>f : α → β<GOAL>Finsupp.mapDomain f (v₁ + v₂) = Finsupp.mapDomain f v₁ + Finsupp.mapDomain f v₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α ≃ β<VAR>x : α →₀ M<VAR>a : β<GOAL>(Finsupp.mapDomain (⇑f) x) a = x (f.symm a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>v : α →₀ M<GOAL>(Finsupp.mapDomain.addMonoidHom f) v = Finsupp.mapDomain f v
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<GOAL>Finsupp.mapDomain.addMonoidHom id = AddMonoidHom.id (α →₀ M)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : β → γ<VAR>g : α → β<GOAL>Finsupp.mapDomain.addMonoidHom (f ∘ g) = (Finsupp.mapDomain.addMonoidHom f).comp (Finsupp.mapDomain.addMonoidHom g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>s : Finset ι<VAR>v : ι → α →₀ M<GOAL>Finsupp.mapDomain f (∑ i ∈ s, v i) = ∑ i ∈ s, Finsupp.mapDomain f (v i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>Zero N<VAR>f : α → β<VAR>s : α →₀ N<VAR>v : α → N → α →₀ M<GOAL>Finsupp.mapDomain f (s.sum v) = s.sum fun a b => Finsupp.mapDomain f (v a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<GOAL>(Finsupp.mapDomain f s).support ⊆ Finset.image f s.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>S : Set α<VAR>f : α → β<VAR>x : α →₀ M<VAR>hS : ↑x.support ⊆ S<VAR>hf : Set.InjOn f S<VAR>a : α<VAR>ha : a ∈ S<GOAL>(Finsupp.mapDomain f x) (f a) = x a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<GOAL>(Finsupp.mapDomain f s).support = Finset.image f s.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : α →₀ M<GOAL>(Finsupp.mapDomain f s).support = Finset.image f s.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → β<VAR>s : α →₀ M<VAR>h : β → M → N<VAR>h_zero : ∀ (b : β), h b 0 = 0<VAR>h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂<GOAL>(Finsupp.mapDomain f s).sum h = s.sum fun a m => h (f a) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>CommMonoid N<VAR>f : α → β<VAR>s : α →₀ M<VAR>h : β → M → N<VAR>h_zero : ∀ (b : β), h b 0 = 1<VAR>h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂<GOAL>(Finsupp.mapDomain f s).prod h = s.prod fun a m => h (f a) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → β<VAR>s : α →₀ M<VAR>h : β → M →+ N<GOAL>((Finsupp.mapDomain f s).sum fun b m => (h b) m) = s.sum fun a m => (h (f a)) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α ↪ β<VAR>v : α →₀ M<GOAL>Finsupp.embDomain f v = Finsupp.mapDomain (⇑f) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>CommMonoid N<VAR>f : α → β<VAR>s : α →₀ M<VAR>h : β → M → N<VAR>hf : Function.Injective f<GOAL>(Finsupp.mapDomain f s).prod h = s.prod fun a b => h (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → β<VAR>s : α →₀ M<VAR>h : β → M → N<VAR>hf : Function.Injective f<GOAL>(Finsupp.mapDomain f s).sum h = s.sum fun a b => h (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Injective (Finsupp.mapDomain f)
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>f : α ↪ β<VAR>v : α →₀ ℕ<GOAL>(Finsupp.mapDomainEmbedding f) v = Finsupp.mapDomain (⇑f) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → β<VAR>g : M →+ N<GOAL>(Finsupp.mapDomain.addMonoidHom f).comp (Finsupp.mapRange.addMonoidHom g) = (Finsupp.mapRange.addMonoidHom g).comp (Finsupp.mapDomain.addMonoidHom f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → β<VAR>v : α →₀ M<VAR>g : M → N<VAR>h0 : g 0 = 0<VAR>hadd : ∀ (x y : M), g (x + y) = g x + g y<GOAL>Finsupp.mapDomain f (Finsupp.mapRange g h0 v) = Finsupp.mapRange g h0 (Finsupp.mapDomain f v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>f : ι →₀ α<VAR>i : ι<VAR>a : α<VAR>g : ι → α → β<VAR>hg : ∀ (i : ι), g i 0 = 0<VAR>hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂<GOAL>(f.update i a).sum g + g i (f i) = f.sum g + g i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>S : Set α<VAR>f : α → β<VAR>hf : Set.InjOn f S<GOAL>Set.InjOn (Finsupp.mapDomain f) {w | ↑w.support ⊆ S}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_13<VAR>AddCommMonoid M<VAR>f : α ≃ β<VAR>l : α →₀ M<GOAL>Finsupp.equivMapDomain f l = Finsupp.mapDomain (⇑f) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.InjOn f (f ⁻¹' ↑l.support)<GOAL>(Finsupp.comapDomain f l hf).support = l.support.preimage f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.InjOn f (f ⁻¹' ↑l.support)<VAR>a : α<GOAL>(Finsupp.comapDomain f l hf) a = l (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α → β<VAR>l : β →₀ M<VAR>g : β → M → N<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<GOAL>(Finsupp.comapDomain f l ⋯).sum (g ∘ f) = l.sum g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<GOAL>Finsupp.comapDomain f l ⋯ = 0 → l = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<VAR>g : β →₀ M<VAR>hg : ↑g.support ⊆ Set.range ⇑f<GOAL>Finsupp.embDomain f (Finsupp.comapDomain (⇑f) g ⋯) = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → β<VAR>hif : Set.InjOn f (f ⁻¹' ↑(Finsupp.support 0)) := ⋯<GOAL>Finsupp.comapDomain f 0 hif = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → β<VAR>a : α<VAR>m : M<VAR>hif : Set.InjOn f (f ⁻¹' ↑(Finsupp.single (f a) m).support)<GOAL>Finsupp.comapDomain f (Finsupp.single (f a) m) hif = Finsupp.single a m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α → β<VAR>v₁ v₂ : β →₀ M<VAR>hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)<VAR>hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)<VAR>hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)<GOAL>Finsupp.comapDomain f (v₁ + v₂) hv₁₂ = Finsupp.comapDomain f v₁ hv₁ + Finsupp.comapDomain f v₂ hv₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>v₁ v₂ : β →₀ M<GOAL>Finsupp.comapDomain f (v₁ + v₂) ⋯ = Finsupp.comapDomain f v₁ ⋯ + Finsupp.comapDomain f v₂ ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x : β →₀ M<GOAL>(Finsupp.comapDomain.addMonoidHom hf) x = Finsupp.comapDomain f x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>l : β →₀ M<VAR>hl : ↑l.support ⊆ Set.range f<GOAL>Finsupp.mapDomain f (Finsupp.comapDomain f l ⋯) = l
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : Option α →₀ M<VAR>a : α<GOAL>f.some a = f (some a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>Finsupp.some 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f g : Option α →₀ M<GOAL>(f + g).some = f.some + g.some
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>m : M<GOAL>(Finsupp.single none m).some = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>m : M<GOAL>(Finsupp.single (some a) m).some = Finsupp.single a m
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : Option α →₀ M<VAR>b : Option α → M → N<VAR>h_zero : ∀ (o : Option α), b o 0 = 0<VAR>h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂<GOAL>f.sum b = b none (f none) + f.some.sum fun a => b (some a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>CommMonoid N<VAR>f : Option α →₀ M<VAR>b : Option α → M → N<VAR>h_zero : ∀ (o : Option α), b o 0 = 1<VAR>h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂<GOAL>f.prod b = b none (f none) * f.some.prod fun a => b (some a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Option α →₀ R<VAR>b : Option α → M<GOAL>(f.sum fun o r => r • b o) = f none • b none + f.some.sum fun a r => r • b (some a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>a : α<GOAL>(Finsupp.filter p f) a = if p a then f a else 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<GOAL>⇑(Finsupp.filter p f) = {x | p x}.indicator ⇑f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<GOAL>Finsupp.filter p f = 0 ↔ ∀ (x : α), p x → f x = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<GOAL>Finsupp.filter p f = f ↔ ∀ (x : α), f x ≠ 0 → p x
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>a : α<VAR>h : p a<GOAL>(Finsupp.filter p f) a = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>a : α<VAR>h : ¬p a<GOAL>(Finsupp.filter p f) a = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<GOAL>(Finsupp.filter p f).support = Finset.filter p f.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Finsupp.filter p 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>b : M<VAR>h : p a<GOAL>Finsupp.filter p (Finsupp.single a b) = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>b : M<VAR>h : ¬p a<GOAL>Finsupp.filter p (Finsupp.single a b) = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>CommMonoid N<VAR>g : α → M → N<GOAL>(Finsupp.filter p f).prod g = ∏ x ∈ (Finsupp.filter p f).support, g x (f x)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>AddCommMonoid N<VAR>g : α → M → N<GOAL>(Finsupp.filter p f).sum g = ∑ x ∈ (Finsupp.filter p f).support, g x (f x)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>AddCommMonoid N<VAR>g : α → M → N<GOAL>(Finsupp.filter p f).sum g + (Finsupp.filter (fun a => ¬p a) f).sum g = f.sum g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>CommMonoid N<VAR>g : α → M → N<GOAL>(Finsupp.filter p f).prod g * (Finsupp.filter (fun a => ¬p a) f).prod g = f.prod g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>G : Type u_9<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>AddCommGroup G<VAR>g : α → M → G<GOAL>f.sum g - (Finsupp.filter p f).sum g = (Finsupp.filter (fun a => ¬p a) f).sum g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>G : Type u_9<VAR>Zero M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<VAR>CommGroup G<VAR>g : α → M → G<GOAL>f.prod g / (Finsupp.filter p f).prod g = (Finsupp.filter (fun a => ¬p a) f).prod g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α →₀ M<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Finsupp.filter p f + Finsupp.filter (fun a => ¬p a) f = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>y : M<GOAL>y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>0 ∉ f.frange
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>x : α<VAR>y : M<GOAL>(Finsupp.single x y).frange ⊆ {y}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>D : DecidablePred p<VAR>f : α →₀ M<GOAL>(Finsupp.subtypeDomain p f).support = Finset.subtype p f.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>a : Subtype p<VAR>v : α →₀ M<GOAL>(Finsupp.subtypeDomain p v) a = v ↑a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<GOAL>Finsupp.subtypeDomain p 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>f : α →₀ M<GOAL>Finsupp.subtypeDomain p f = 0 ↔ ∀ (x : α), p x → f x = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>p : α → Prop<VAR>f : α →₀ M<VAR>hf : ∀ x ∈ f.support, p x<GOAL>Finsupp.subtypeDomain p f = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>p : α → Prop<VAR>AddCommMonoid N<VAR>v : α →₀ M<VAR>h : α → M → N<VAR>hp : ∀ x ∈ v.support, p x<GOAL>((Finsupp.subtypeDomain p v).sum fun a b => h (↑a) b) = v.sum h
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>p : α → Prop<VAR>CommMonoid N<VAR>v : α →₀ M<VAR>h : α → M → N<VAR>hp : ∀ x ∈ v.support, p x<GOAL>((Finsupp.subtypeDomain p v).prod fun a b => h (↑a) b) = v.prod h
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>p : α → Prop<VAR>v v' : α →₀ M<GOAL>Finsupp.subtypeDomain p (v + v') = Finsupp.subtypeDomain p v + Finsupp.subtypeDomain p v'
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>v v' : α →₀ M<GOAL>Finsupp.filter p (v + v') = Finsupp.filter p v + Finsupp.filter p v'
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>p : α → Prop<VAR>s : Finset ι<VAR>h : ι → α →₀ M<GOAL>Finsupp.subtypeDomain p (∑ c ∈ s, h c) = ∑ c ∈ s, Finsupp.subtypeDomain p (h c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>p : α → Prop<VAR>Zero N<VAR>s : β →₀ N<VAR>h : β → N → α →₀ M<GOAL>Finsupp.subtypeDomain p (s.sum h) = s.sum fun c d => Finsupp.subtypeDomain p (h c d)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset ι<VAR>f : ι → α →₀ M<GOAL>Finsupp.filter p (∑ a ∈ s, f a) = ∑ a ∈ s, Finsupp.filter p (f a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ M<GOAL>Finsupp.filter p f = ∑ i ∈ Finset.filter p f.support, Finsupp.single i (f i)
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>p : α → Prop<VAR>v : α →₀ G<GOAL>Finsupp.subtypeDomain p (-v) = -Finsupp.subtypeDomain p v
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>p : α → Prop<VAR>v v' : α →₀ G<GOAL>Finsupp.subtypeDomain p (v - v') = Finsupp.subtypeDomain p v - Finsupp.subtypeDomain p v'
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>a : α<VAR>b : G<GOAL>Finsupp.single a (-b) = -Finsupp.single a b
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>a : α<VAR>b₁ b₂ : G<GOAL>Finsupp.single a (b₁ - b₂) = Finsupp.single a b₁ - Finsupp.single a b₂
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>a : α<VAR>f : α →₀ G<GOAL>Finsupp.erase a (-f) = -Finsupp.erase a f
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>a : α<VAR>f₁ f₂ : α →₀ G<GOAL>Finsupp.erase a (f₁ - f₂) = Finsupp.erase a f₁ - Finsupp.erase a f₂
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α →₀ G<GOAL>Finsupp.filter p (-f) = -Finsupp.filter p f
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f₁ f₂ : α →₀ G<GOAL>Finsupp.filter p (f₁ - f₂) = Finsupp.filter p f₁ - Finsupp.filter p f₂
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Multiset (α →₀ M)<VAR>a : α<GOAL>a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>h : ι → α →₀ M<VAR>a : α<VAR>ha : a ∈ (∑ c ∈ s, h c).support<GOAL>∃ c ∈ s, a ∈ (h c).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α × β →₀ M<VAR>x : α<VAR>y : β<GOAL>(f.curry x) y = f (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α × β →₀ M<VAR>g : α → β → M → N<VAR>hg₀ : ∀ (a : α) (b : β), g a b 0 = 0<VAR>hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁<GOAL>(f.curry.sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α × β →₀ M<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>(Finsupp.filter (fun a => p a.1) f).curry = Finsupp.filter p f.curry
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>DecidableEq α<VAR>f : α × β →₀ M<GOAL>f.curry.support ⊆ Finset.image Prod.fst f.support
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>f : α →₀ γ<VAR>g : β →₀ γ<GOAL>⇑(f.sumElim g) = Sum.elim ⇑f ⇑g
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>f : α →₀ γ<VAR>g : β →₀ γ<VAR>x : α ⊕ β<GOAL>(f.sumElim g) x = Sum.elim (⇑f) (⇑g) x
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>f : α →₀ γ<VAR>g : β →₀ γ<VAR>x : α<GOAL>(f.sumElim g) (Sum.inl x) = f x
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>f : α →₀ γ<VAR>g : β →₀ γ<VAR>x : β<GOAL>(f.sumElim g) (Sum.inr x) = g x
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>fg : (α →₀ γ) × (β →₀ γ)<GOAL>Finsupp.sumFinsuppEquivProdFinsupp.symm fg = fg.1.sumElim fg.2
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>f : α ⊕ β →₀ γ<GOAL>Finsupp.sumFinsuppEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f ⋯, Finsupp.comapDomain Sum.inr f ⋯)
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>f : α ⊕ β →₀ γ<VAR>x : α<GOAL>(Finsupp.sumFinsuppEquivProdFinsupp f).1 x = f (Sum.inl x)
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>f : α ⊕ β →₀ γ<VAR>y : β<GOAL>(Finsupp.sumFinsuppEquivProdFinsupp f).2 y = f (Sum.inr y)
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>fg : (α →₀ γ) × (β →₀ γ)<VAR>x : α<GOAL>(Finsupp.sumFinsuppEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x
<VAR>α : Type u_13<VAR>β : Type u_14<VAR>γ : Type u_15<VAR>Zero γ<VAR>fg : (α →₀ γ) × (β →₀ γ)<VAR>y : β<GOAL>(Finsupp.sumFinsuppEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y
<VAR>M : Type u_5<VAR>AddMonoid M<VAR>α : Type u_13<VAR>β : Type u_14<VAR>f : α ⊕ β →₀ M<GOAL>Finsupp.sumFinsuppAddEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f ⋯, Finsupp.comapDomain Sum.inr f ⋯)
<VAR>M : Type u_5<VAR>AddMonoid M<VAR>α : Type u_13<VAR>β : Type u_14<VAR>fg : (α →₀ M) × (β →₀ M)<GOAL>Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg = fg.1.sumElim fg.2
<VAR>M : Type u_5<VAR>AddMonoid M<VAR>α : Type u_13<VAR>β : Type u_14<VAR>f : α ⊕ β →₀ M<VAR>x : α<GOAL>(Finsupp.sumFinsuppAddEquivProdFinsupp f).1 x = f (Sum.inl x)
<VAR>M : Type u_5<VAR>AddMonoid M<VAR>α : Type u_13<VAR>β : Type u_14<VAR>f : α ⊕ β →₀ M<VAR>y : β<GOAL>(Finsupp.sumFinsuppAddEquivProdFinsupp f).2 y = f (Sum.inr y)
<VAR>M : Type u_5<VAR>AddMonoid M<VAR>α : Type u_13<VAR>β : Type u_14<VAR>fg : (α →₀ M) × (β →₀ M)<VAR>x : α<GOAL>(Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x
<VAR>M : Type u_5<VAR>AddMonoid M<VAR>α : Type u_13<VAR>β : Type u_14<VAR>fg : (α →₀ M) × (β →₀ M)<VAR>y : β<GOAL>(Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>MonoidWithZero R<VAR>MulActionWithZero R M<VAR>a b : α<VAR>f : α → M<VAR>r : R<GOAL>(Finsupp.single a r) b • f a = (Finsupp.single a (r • f b)) b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>G : Type u_9<VAR>Monoid G<VAR>MulAction G α<VAR>AddCommMonoid M<VAR>g : G<VAR>f : α →₀ M<GOAL>g • f = Finsupp.mapDomain (fun x => g • x) f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>G : Type u_9<VAR>Monoid G<VAR>MulAction G α<VAR>AddCommMonoid M<VAR>g : G<VAR>a : α<VAR>b : M<GOAL>g • Finsupp.single a b = Finsupp.single (g • a) b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>G : Type u_9<VAR>Group G<VAR>MulAction G α<VAR>AddCommMonoid M<VAR>g : G<VAR>f : α →₀ M<VAR>a : α<GOAL>(g • f) a = f (g⁻¹ • a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>SMulZeroClass R M<VAR>b : R<VAR>v : α →₀ M<GOAL>⇑(b • v) = b • ⇑v
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>SMulZeroClass R M<VAR>b : R<VAR>v : α →₀ M<VAR>a : α<GOAL>(b • v) a = b • v a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>SMulZeroClass R M<VAR>k : R<VAR>hk : IsSMulRegular M k<GOAL>IsSMulRegular (α →₀ M) k
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>AddMonoid M<VAR>SMulZeroClass R M<VAR>b : R<VAR>g : α →₀ M<GOAL>(b • g).support ⊆ g.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>b : R<VAR>hb : b ≠ 0<VAR>g : α →₀ M<GOAL>(b • g).support = g.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>∀ {x : Monoid R} [inst : AddMonoid M] [inst_1 : DistribMulAction R M] {b : R} {v : α →₀ M}, Finsupp.filter p (b • v) = b • Finsupp.filter p v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>R : Type u_11<GOAL>∀ {x : Monoid R} [inst : AddCommMonoid M] [inst_1 : DistribMulAction R M] {f : α → β} (b : R) (v : α →₀ M), Finsupp.mapDomain f (b • v) = b • Finsupp.mapDomain f v
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>SMulZeroClass R M<VAR>c : R<VAR>a : α<VAR>b : M<GOAL>c • Finsupp.single a b = Finsupp.single a (c • b)
<VAR>α : Type u_1<VAR>R : Type u_11<GOAL>∀ {x : Semiring R} (c : R) (a : α) (b : R), c • Finsupp.single a b = Finsupp.single a (c * b)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>R : Type u_11<GOAL>∀ {x : Monoid R} [inst : AddMonoid M] [inst_1 : DistribMulAction R M] [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M), (∀ (x_1 : M), f (c • x_1) = c • f x_1) → Finsupp.mapRange f hf (c • v) = c • Finsupp.mapRange f hf v
<VAR>α : Type u_1<VAR>R : Type u_11<VAR>Semiring R<VAR>a : α<VAR>b : R<GOAL>b • Finsupp.single a 1 = Finsupp.single a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>R : Type u_11<VAR>AddMonoid M<VAR>Monoid R<VAR>DistribMulAction R M<VAR>f : α → β<VAR>r : R<VAR>v : β →₀ M<VAR>hfv : Set.InjOn f (f ⁻¹' ↑v.support)<VAR>hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support) := ⋯<GOAL>Finsupp.comapDomain f (r • v) hfrv = r • Finsupp.comapDomain f v hfv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>R : Type u_11<VAR>AddMonoid M<VAR>Monoid R<VAR>DistribMulAction R M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>r : R<VAR>v : β →₀ M<GOAL>Finsupp.comapDomain f (r • v) ⋯ = r • Finsupp.comapDomain f v ⋯
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>g : α →₀ R<VAR>b : R<VAR>h : α → R → M<VAR>h0 : ∀ (i : α), h i 0 = 0<GOAL>(b • g).sum h = g.sum fun i a => h i (b * a)