ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>y : β<GOAL>(Finset.filter (fun x => f x = y) s).Nonempty ↔ y ∈ Finset.image f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>↑(Finset.image f s) = f '' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>(Finset.image f s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>h : s.Nonempty<VAR>f : α → β<GOAL>(Finset.image f s).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → β<GOAL>(Finset.image f s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>Finset.image f s.toFinset = (Multiset.map f s).toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>H : Set.InjOn f ↑s<GOAL>(Finset.image f s).val = Multiset.map f s.val
<VAR>α : Type u_1<VAR>s : Finset α<VAR>DecidableEq α<GOAL>Finset.image id s = s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>DecidableEq α<GOAL>Finset.image (fun x => x) s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>DecidableEq γ<VAR>g : β → γ<GOAL>Finset.image g (Finset.image f s) = Finset.image (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq β<VAR>s : Finset α<VAR>β' : Type u_4<VAR>DecidableEq β'<VAR>DecidableEq γ<VAR>f : β → γ<VAR>g : α → β<VAR>f' : α → β'<VAR>g' : β' → γ<VAR>h_comm : ∀ (a : α), f (g a) = g' (f' a)<GOAL>Finset.image f (Finset.image g s) = Finset.image g' (Finset.image f' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>h : Function.Semiconj f ga gb<GOAL>Function.Semiconj (Finset.image f) (Finset.image ga) (Finset.image gb)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Function.Commute (Finset.image f) (Finset.image g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s₁ s₂ : Finset α<VAR>h : s₁ ⊆ s₂<GOAL>Finset.image f s₁ ⊆ Finset.image f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image f s ⊆ t ↔ ∀ x ∈ s, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<GOAL>Monotone (Finset.image f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Injective (Finset.image f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : Function.Injective f<GOAL>Finset.image f s = Finset.image f t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : Function.Injective f<GOAL>Finset.image f s ⊆ Finset.image f t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : Function.Injective f<GOAL>Finset.image f s ⊂ Finset.image f t ↔ s ⊂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>↑(Finset.image f s) ⊆ Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>p : β → Prop<VAR>DecidablePred p<GOAL>Finset.filter p (Finset.image f s) = Finset.image f (Finset.filter (fun a => p (f a)) s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>s₁ s₂ : Finset α<GOAL>Finset.image f (s₁ ∪ s₂) = Finset.image f s₁ ∪ Finset.image f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<GOAL>Finset.image f (s ∩ t) ⊆ Finset.image f s ∩ Finset.image f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : Set.InjOn f (↑s ∪ ↑t)<GOAL>Finset.image f (s ∩ t) = Finset.image f s ∩ Finset.image f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>hf : Function.Injective f<GOAL>Finset.image f (s₁ ∩ s₂) = Finset.image f s₁ ∩ Finset.image f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>a : α<GOAL>Finset.image f {a} = {f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>a : α<VAR>s : Finset α<GOAL>Finset.image f (insert a s) = insert (f a) (Finset.image f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>s : Finset α<VAR>a : α<GOAL>(Finset.image f s).erase (f a) ⊆ Finset.image f (s.erase a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Finset α<VAR>a : α<GOAL>Finset.image f (s.erase a) = (Finset.image f s).erase (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>Finset.image f s = ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : Function.Injective f<GOAL>Finset.image f (s \ t) = Finset.image f s \ Finset.image f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : Function.Injective f<GOAL>Finset.image f (symmDiff s t) = symmDiff (Finset.image f s) (Finset.image f t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s t : Finset α<VAR>f : α → β<VAR>h : Disjoint (Finset.image f s) (Finset.image f t)<GOAL>Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : ℕ → α<VAR>a : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ (i : ℕ), f (i % n) = f i<GOAL>a ∈ Set.range f ↔ a ∈ Finset.image (fun i => f i) (Finset.range n)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : ℤ → α<VAR>a : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ (i : ℤ), f (i % ↑n) = f i<GOAL>a ∈ Set.range f ↔ a ∈ Finset.image (fun i => f ↑i) (Finset.range n)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.image Subtype.val s.attach = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).attach = insert ⟨a, ⋯⟩ (Finset.image (fun x => ⟨↑x, ⋯⟩) s.attach)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s t : Finset α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Disjoint (Finset.image f s) (Finset.image f t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>h : s.Nonempty<VAR>b : β<GOAL>Finset.image (fun x => b) s = {b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>f : α ↪ β<VAR>s : Finset α<VAR>a : α<GOAL>Finset.map f (s.erase a) = (Finset.map f s).erase (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>f : α → β<VAR>s : Finset α<VAR>t : β → Finset γ<GOAL>(Finset.image f s).biUnion t = s.biUnion fun a => t (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>s : Finset α<VAR>t : α → Finset β<VAR>f : β → γ<GOAL>Finset.image f (s.biUnion t) = s.biUnion fun a => Finset.image f (t a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>s : Finset β<VAR>g : β → α<GOAL>((Finset.image g s).biUnion fun a => Finset.filter (fun c => g c = a) s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → β<GOAL>(s.biUnion fun a => {f a}) = Finset.image f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>s' : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<GOAL>(Finset.filterMap f s' f_inj).val = Multiset.filterMap f s'.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<GOAL>Finset.filterMap f ∅ f_inj = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>s : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<VAR>b : β<GOAL>b ∈ Finset.filterMap f s f_inj ↔ ∃ a ∈ s, f a = some b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>s : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<GOAL>↑(Finset.filterMap f s f_inj) = {b | ∃ a ∈ s, f a = some b}
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.filterMap some s ⋯ = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>s t : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<VAR>h : s ⊆ t<GOAL>Finset.filterMap f s f_inj ⊆ Finset.filterMap f t f_inj
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<VAR>a : Subtype p<GOAL>a ∈ Finset.subtype p s ↔ ↑a ∈ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Monotone (Finset.subtype p)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = Finset.filter p s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<VAR>h : ∀ x ∈ s, p x<GOAL>Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>a : α<VAR>h : a ∈ Finset.map (Function.Embedding.subtype fun x => p x) s<GOAL>p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>a : α<VAR>h : ¬p a<GOAL>a ∉ Finset.map (Function.Embedding.subtype fun x => p x) s
<VAR>α : Type u_1<VAR>t : Set α<VAR>s : Finset ↑t<GOAL>↑(Finset.map (Function.Embedding.subtype fun x => x ∈ t) s) ⊆ t
<VAR>n : ℕ<VAR>s : Finset ℕ<VAR>a : Fin n<GOAL>a ∈ Finset.fin n s ↔ ↑a ∈ s
<VAR>n : ℕ<GOAL>Monotone (Finset.fin n)
<VAR>n : ℕ<VAR>s : Finset ℕ<GOAL>Finset.map Fin.valEmbedding (Finset.fin n s) = Finset.filter (fun x => x < n) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Set α<VAR>t : Finset β<VAR>f : α → β<GOAL>↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ Finset.image f s' = t
<VAR>n : ℕ<GOAL>Finset.range (n + 1) \ {0} = Finset.image Nat.succ (Finset.range n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>m : Multiset α<GOAL>(Multiset.map f m).toFinset = Finset.image f m.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Finset α<GOAL>e.finsetCongr s = Finset.map e.toEmbedding s
<VAR>α : Type u_1<GOAL>(Equiv.refl α).finsetCongr = Equiv.refl (Finset α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.finsetCongr.symm = e.symm.finsetCongr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>e' : β ≃ γ<GOAL>e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β → β<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>b : β<GOAL>Multiset.noncommFoldr f (↑l) comm b = List.foldr f b l
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β → β<VAR>h : {x | x ∈ 0}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>b : β<GOAL>Multiset.noncommFoldr f 0 h b = b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β → β<VAR>s : Multiset α<VAR>a : α<VAR>h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>h' : {x | x ∈ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>b : β<GOAL>Multiset.noncommFoldr f (a ::ₘ s) h b = f a (Multiset.noncommFoldr f s h' b)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β → β<VAR>s : Multiset α<VAR>h : LeftCommutative f<VAR>b : β<GOAL>Multiset.noncommFoldr f s ⋯ b = Multiset.foldr f h b s
<VAR>α : Type u_3<VAR>op : α → α → α<VAR>assoc : Std.Associative op<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise fun x y => op x y = op y x<VAR>a : α<GOAL>Multiset.noncommFold op (↑l) comm a = List.foldr op a l
<VAR>α : Type u_3<VAR>op : α → α → α<VAR>assoc : Std.Associative op<VAR>h : {x | x ∈ 0}.Pairwise fun x y => op x y = op y x<VAR>a : α<GOAL>Multiset.noncommFold op 0 h a = a
<VAR>α : Type u_3<VAR>op : α → α → α<VAR>assoc : Std.Associative op<VAR>s : Multiset α<VAR>a : α<VAR>h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => op x y = op y x<VAR>h' : {x | x ∈ s}.Pairwise fun x y => op x y = op y x<VAR>x : α<GOAL>Multiset.noncommFold op (a ::ₘ s) h x = op a (Multiset.noncommFold op s h' x)
<VAR>α : Type u_3<VAR>op : α → α → α<VAR>assoc : Std.Associative op<VAR>s : Multiset α<VAR>Std.Commutative op<VAR>a : α<GOAL>Multiset.noncommFold op s ⋯ a = Multiset.fold op a s
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise AddCommute<GOAL>(↑l).noncommSum comm = l.sum
<VAR>α : Type u_3<VAR>Monoid α<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise Commute<GOAL>(↑l).noncommProd comm = l.prod
<VAR>α : Type u_3<VAR>Monoid α<VAR>h : {x | x ∈ 0}.Pairwise Commute<GOAL>Multiset.noncommProd 0 h = 1
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>h : {x | x ∈ 0}.Pairwise AddCommute<GOAL>Multiset.noncommSum 0 h = 0
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>comm : {x | x ∈ a ::ₘ s}.Pairwise AddCommute<GOAL>(a ::ₘ s).noncommSum comm = a + s.noncommSum ⋯
<VAR>α : Type u_3<VAR>Monoid α<VAR>s : Multiset α<VAR>a : α<VAR>comm : {x | x ∈ a ::ₘ s}.Pairwise Commute<GOAL>(a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>comm : {x | x ∈ a ::ₘ s}.Pairwise AddCommute<GOAL>(a ::ₘ s).noncommSum comm = s.noncommSum ⋯ + a
<VAR>α : Type u_3<VAR>Monoid α<VAR>s : Multiset α<VAR>a : α<VAR>comm : {x | x ∈ a ::ₘ s}.Pairwise Commute<GOAL>(a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a
<VAR>α : Type u_3<VAR>Monoid α<VAR>s t : Multiset α<VAR>comm : {x | x ∈ s + t}.Pairwise Commute<GOAL>(s + t).noncommProd comm = s.noncommProd ⋯ * t.noncommProd ⋯
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s t : Multiset α<VAR>comm : {x | x ∈ s + t}.Pairwise AddCommute<GOAL>(s + t).noncommSum comm = s.noncommSum ⋯ + t.noncommSum ⋯
<VAR>α : Type u_3<VAR>Monoid α<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>p : α → Prop<VAR>hom : ∀ (a b : α), p a → p b → p (a * b)<VAR>unit : p 1<VAR>base : ∀ x ∈ s, p x<GOAL>p (s.noncommProd comm)
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise AddCommute<VAR>p : α → Prop<VAR>hom : ∀ (a b : α), p a → p b → p (a + b)<VAR>unit : p 0<VAR>base : ∀ x ∈ s, p x<GOAL>p (s.noncommSum comm)
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid α<VAR>AddMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise AddCommute<VAR>f : F<GOAL>{x | x ∈ Multiset.map (⇑f) s}.Pairwise AddCommute
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid α<VAR>Monoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>f : F<GOAL>{x | x ∈ Multiset.map (⇑f) s}.Pairwise Commute
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid α<VAR>AddMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise AddCommute<VAR>f : F<GOAL>f (s.noncommSum comm) = (Multiset.map (⇑f) s).noncommSum ⋯
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid α<VAR>Monoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>f : F<GOAL>f (s.noncommProd comm) = (Multiset.map (⇑f) s).noncommProd ⋯
<VAR>α : Type u_3<VAR>Monoid α<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>m : α<VAR>h : ∀ x ∈ s, x = m<GOAL>s.noncommProd comm = m ^ Multiset.card s
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise AddCommute<VAR>m : α<VAR>h : ∀ x ∈ s, x = m<GOAL>s.noncommSum comm = Multiset.card s • m
<VAR>α : Type u_6<VAR>CommMonoid α<VAR>s : Multiset α<GOAL>s.noncommProd ⋯ = s.prod
<VAR>α : Type u_6<VAR>AddCommMonoid α<VAR>s : Multiset α<GOAL>s.noncommSum ⋯ = s.sum
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise AddCommute<VAR>y : α<VAR>h : ∀ x ∈ s, AddCommute y x<GOAL>AddCommute y (s.noncommSum comm)
<VAR>α : Type u_3<VAR>Monoid α<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>y : α<VAR>h : ∀ x ∈ s, Commute y x<GOAL>Commute y (s.noncommProd comm)
<VAR>α : Type u_3<VAR>Monoid α<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ y ∈ {x | x ∈ s.erase a}, x ≠ y → Commute x y := ⋯<GOAL>a * (s.erase a).noncommProd comm' = s.noncommProd comm
<VAR>α : Type u_3<VAR>Monoid α<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ y ∈ {x | x ∈ s.erase a}, x ≠ y → Commute x y := ⋯<GOAL>(s.erase a).noncommProd comm' * a = s.noncommProd comm
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<GOAL>{x | x ∈ Multiset.map f s.val}.Pairwise Commute
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => AddCommute (f a) (f b)<GOAL>{x | x ∈ Multiset.map f s.val}.Pairwise AddCommute
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>p : β → Prop<VAR>hom : ∀ (a b : β), p a → p b → p (a * b)<VAR>unit : p 1<VAR>base : ∀ x ∈ s, p (f x)<GOAL>p (s.noncommProd f comm)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => AddCommute (f a) (f b)<VAR>p : β → Prop<VAR>hom : ∀ (a b : β), p a → p b → p (a + b)<VAR>unit : p 0<VAR>base : ∀ x ∈ s, p (f x)<GOAL>p (s.noncommSum f comm)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s₁ s₂ : Finset α<VAR>f g : α → β<VAR>h₁ : s₁ = s₂<VAR>h₂ : ∀ x ∈ s₂, f x = g x<VAR>comm : (↑s₁).Pairwise fun a b => Commute (f a) (f b)<GOAL>s₁.noncommProd f comm = s₂.noncommProd g ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s₁ s₂ : Finset α<VAR>f g : α → β<VAR>h₁ : s₁ = s₂<VAR>h₂ : ∀ x ∈ s₂, f x = g x<VAR>comm : (↑s₁).Pairwise fun a b => AddCommute (f a) (f b)<GOAL>s₁.noncommSum f comm = s₂.noncommSum g ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>DecidableEq α<VAR>l : List α<VAR>f : α → β<VAR>comm : (↑l.toFinset).Pairwise fun a b => AddCommute (f a) (f b)<VAR>hl : l.Nodup<GOAL>l.toFinset.noncommSum f comm = (List.map f l).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>DecidableEq α<VAR>l : List α<VAR>f : α → β<VAR>comm : (↑l.toFinset).Pairwise fun a b => Commute (f a) (f b)<VAR>hl : l.Nodup<GOAL>l.toFinset.noncommProd f comm = (List.map f l).prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>f : α → β<VAR>h : (↑∅).Pairwise fun a b => AddCommute (f a) (f b)<GOAL>∅.noncommSum f h = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>f : α → β<VAR>h : (↑∅).Pairwise fun a b => Commute (f a) (f b)<GOAL>∅.noncommProd f h = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>ha : a ∉ s<VAR>comm : (↑(Finset.cons a s ha)).Pairwise fun a b => AddCommute (f a) (f b)<GOAL>(Finset.cons a s ha).noncommSum f comm = f a + s.noncommSum f ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>ha : a ∉ s<VAR>comm : (↑(Finset.cons a s ha)).Pairwise fun a b => Commute (f a) (f b)<GOAL>(Finset.cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>ha : a ∉ s<VAR>comm : (↑(Finset.cons a s ha)).Pairwise fun a b => AddCommute (f a) (f b)<GOAL>(Finset.cons a s ha).noncommSum f comm = s.noncommSum f ⋯ + f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>ha : a ∉ s<VAR>comm : (↑(Finset.cons a s ha)).Pairwise fun a b => Commute (f a) (f b)<GOAL>(Finset.cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>comm : (↑(insert a s)).Pairwise fun a b => Commute (f a) (f b)<VAR>ha : a ∉ s<GOAL>(insert a s).noncommProd f comm = f a * s.noncommProd f ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>comm : (↑(insert a s)).Pairwise fun a b => AddCommute (f a) (f b)<VAR>ha : a ∉ s<GOAL>(insert a s).noncommSum f comm = f a + s.noncommSum f ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>comm : (↑(insert a s)).Pairwise fun a b => AddCommute (f a) (f b)<VAR>ha : a ∉ s<GOAL>(insert a s).noncommSum f comm = s.noncommSum f ⋯ + f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>comm : (↑(insert a s)).Pairwise fun a b => Commute (f a) (f b)<VAR>ha : a ∉ s<GOAL>(insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>a : α<VAR>f : α → β<GOAL>{a}.noncommProd f ⋯ = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>a : α<VAR>f : α → β<GOAL>{a}.noncommSum f ⋯ = f a
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Monoid β<VAR>Monoid γ<VAR>FunLike F β γ<VAR>MonoidHomClass F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>g : F<GOAL>g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) ⋯
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddMonoid β<VAR>AddMonoid γ<VAR>FunLike F β γ<VAR>AddMonoidHomClass F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => AddCommute (f a) (f b)<VAR>g : F<GOAL>g (s.noncommSum f comm) = s.noncommSum (fun i => g (f i)) ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>m : β<VAR>h : ∀ x ∈ s, f x = m<GOAL>s.noncommProd f comm = m ^ s.card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => AddCommute (f a) (f b)<VAR>m : β<VAR>h : ∀ x ∈ s, f x = m<GOAL>s.noncommSum f comm = s.card • m
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>y : β<VAR>h : ∀ x ∈ s, Commute y (f x)<GOAL>Commute y (s.noncommProd f comm)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => AddCommute (f a) (f b)<VAR>y : β<VAR>h : ∀ x ∈ s, AddCommute y (f x)<GOAL>AddCommute y (s.noncommSum f comm)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>comm' : ∀ x ∈ ↑(s.erase a), ∀ y ∈ ↑(s.erase a), x ≠ y → (fun a b => Commute (f a) (f b)) x y := ⋯<GOAL>f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>comm' : ∀ x ∈ ↑(s.erase a), ∀ y ∈ ↑(s.erase a), x ≠ y → (fun a b => Commute (f a) (f b)) x y := ⋯<GOAL>(s.erase a).noncommProd f comm' * f a = s.noncommProd f comm
<VAR>α : Type u_3<VAR>β : Type u_6<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>s.noncommSum f ⋯ = s.sum f
<VAR>α : Type u_3<VAR>β : Type u_6<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>s.noncommProd f ⋯ = s.prod f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<VAR>f : α → β<VAR>comm : {x | x ∈ s ∪ t}.Pairwise fun a b => Commute (f a) (f b)<GOAL>(s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<VAR>f : α → β<VAR>comm : {x | x ∈ s ∪ t}.Pairwise fun a b => AddCommute (f a) (f b)<GOAL>(s ∪ t).noncommSum f comm = s.noncommSum f ⋯ + t.noncommSum f ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => AddCommute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => AddCommute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => AddCommute (g x) (f y)<GOAL>(↑s).Pairwise fun x y => AddCommute ((f + g) x) ((f + g) y)