ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_6<VAR>AddCommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<GOAL>∑ k ∈ Finset.range (n + m), f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.range m, f (n + k)
<VAR>α : Type u_6<VAR>CommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<GOAL>(∏ k ∈ Finset.range (n + m), f k) / ∏ k ∈ Finset.range n, f k = ∏ k ∈ Finset.range m, f (n + k)
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ℕ → β<GOAL>∑ k ∈ Finset.range 0, f k = 0
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ℕ → β<GOAL>∏ k ∈ Finset.range 0, f k = 1
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ℕ → β<GOAL>∑ k ∈ Finset.range 1, f k = f 0
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ℕ → β<GOAL>∏ k ∈ Finset.range 1, f k = f 0
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>l : List α<VAR>M : Type u_6<VAR>CommMonoid M<VAR>f : α → M<GOAL>(List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ List.count m l
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>l : List α<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>f : α → M<GOAL>(List.map f l).sum = ∑ m ∈ l.toFinset, List.count m l • f m
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>s : List α<GOAL>s.sum = ∑ m ∈ s.toFinset, List.count m s • m
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>CommMonoid α<VAR>s : List α<GOAL>s.prod = ∏ m ∈ s.toFinset, m ^ List.count m s
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>CommMonoid α<VAR>m : List α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<GOAL>m.prod = ∏ i ∈ s, i ^ List.count i m
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>m : List α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<GOAL>m.sum = ∑ i ∈ s, List.count i m • i
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<GOAL>∑ x ∈ Finset.filter p l.toFinset, List.count x l = List.countP (fun b => decide (p b)) l
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>s : Multiset α<VAR>M : Type u_6<VAR>CommMonoid M<VAR>f : α → M<GOAL>(Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>s : Multiset α<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>f : α → M<GOAL>(Multiset.map f s).sum = ∑ m ∈ s.toFinset, Multiset.count m s • f m
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>CommMonoid α<VAR>s : Multiset α<GOAL>s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>s : Multiset α<GOAL>s.sum = ∑ m ∈ s.toFinset, Multiset.count m s • m
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>m : Multiset α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<GOAL>m.sum = ∑ i ∈ s, Multiset.count i m • i
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>CommMonoid α<VAR>m : Multiset α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<GOAL>m.prod = ∏ i ∈ s, i ^ Multiset.count i m
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>m : Multiset α<VAR>f : { x // x ∈ m } → β<VAR>g : α → β<VAR>hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x<GOAL>∏ x : { x // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>m : Multiset α<VAR>f : { x // x ∈ m } → β<VAR>g : α → β<VAR>hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x<GOAL>∑ x : { x // x ∈ m }, f x = ∑ x ∈ m.toFinset, g x
<VAR>α : Type u_3<VAR>s : Finset α<VAR>M : Type u_6<VAR>CommMonoid M<VAR>f : α → M<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a * b)<VAR>unit : p 1<VAR>base : ∀ x ∈ s, p (f x)<GOAL>p (∏ x ∈ s, f x)
<VAR>α : Type u_3<VAR>s : Finset α<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>f : α → M<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a + b)<VAR>unit : p 0<VAR>base : ∀ x ∈ s, p (f x)<GOAL>p (∑ x ∈ s, f x)
<VAR>α : Type u_3<VAR>s : Finset α<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>f : α → M<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a + b)<VAR>nonempty : s.Nonempty<VAR>base : ∀ x ∈ s, p (f x)<GOAL>p (∑ x ∈ s, f x)
<VAR>α : Type u_3<VAR>s : Finset α<VAR>M : Type u_6<VAR>CommMonoid M<VAR>f : α → M<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a * b)<VAR>nonempty : s.Nonempty<VAR>base : ∀ x ∈ s, p (f x)<GOAL>p (∏ x ∈ s, f x)
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f s : ℕ → β<VAR>base : s 0 = 1<VAR>step : ∀ (n : ℕ), s (n + 1) = s n * f n<VAR>n : ℕ<GOAL>∏ k ∈ Finset.range n, f k = s n
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f s : ℕ → β<VAR>base : s 0 = 0<VAR>step : ∀ (n : ℕ), s (n + 1) = s n + f n<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, f k = s n
<VAR>M : Type u_6<VAR>CommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ Finset.range n, f (i + 1) / f i = f n / f 0
<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, (f i - f (i + 1)) = f 0 - f n
<VAR>M : Type u_6<VAR>CommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ Finset.range n, f i / f (i + 1) = f 0 / f n
<VAR>M : Type u_6<VAR>CommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>f n = f 0 * ∏ i ∈ Finset.range n, f (i + 1) / f i
<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>f n = f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i)
<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>f n = ∑ i ∈ Finset.range (n + 1), if i = 0 then f 0 else f i - f (i - 1)
<VAR>M : Type u_6<VAR>CommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>f n = ∏ i ∈ Finset.range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
<VAR>α : Type u_3<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : ℕ → α<VAR>h : Monotone f<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>b : β<GOAL>∏ _x ∈ s, b = b ^ s.card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>b : β<GOAL>∑ _x ∈ s, b = s.card • b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>b : β<VAR>hf : ∀ a ∈ s, f a = b<GOAL>∑ a ∈ s, f a = s.card • b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>b : β<VAR>hf : ∀ a ∈ s, f a = b<GOAL>∏ a ∈ s, f a = b ^ s.card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>b : β<GOAL>s.card • b + ∑ a ∈ s, f a = ∑ a ∈ s, (b + f a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>b : β<GOAL>b ^ s.card * ∏ a ∈ s, f a = ∏ a ∈ s, b * f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>b : β<GOAL>(∏ a ∈ s, f a) * b ^ s.card = ∏ a ∈ s, f a * b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>b : β<GOAL>∑ a ∈ s, f a + s.card • b = ∑ a ∈ s, (f a + b)
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>b : β<VAR>n : ℕ<GOAL>b ^ n = ∏ _k ∈ Finset.range n, b
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>b : β<VAR>n : ℕ<GOAL>n • b = ∑ _k ∈ Finset.range n, b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>n : ℕ<VAR>f : α → β<GOAL>∑ x ∈ s, n • f x = n • ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>n : ℕ<VAR>f : α → β<GOAL>∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>a : β<GOAL>∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>a : β<GOAL>∑ i ∈ s, f i • a = (∑ i ∈ s, f i) • a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>s : Finset α<VAR>f : ℕ → β<GOAL>∑ t ∈ Finset.powersetCard n s, f t.card = s.card.choose n • f n
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>n : ℕ<VAR>s : Finset α<VAR>f : ℕ → β<GOAL>∏ t ∈ Finset.powersetCard n s, f t.card = f n ^ s.card.choose n
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>f : ℕ → β<GOAL>∑ r ∈ Finset.range (n + 1), f (n - r) = ∑ k ∈ Finset.range (n + 1), f k
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>n : ℕ<VAR>f : ℕ → β<GOAL>∏ r ∈ Finset.range (n + 1), f (n - r) = ∏ k ∈ Finset.range (n + 1), f k
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>g : (a : α) → a ∈ s → α<GOAL>(∀ (a : α) (ha : a ∈ s), f a + f (g a ha) = 0) → (∀ (a : α) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a) → ∀ (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s), (∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a) → ∑ x ∈ s, f x = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>g : (a : α) → a ∈ s → α<GOAL>(∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1) → (∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) → ∀ (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s), (∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a) → ∏ x ∈ s, f x = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<VAR>CommMonoid β<VAR>DecidableEq γ<VAR>f : γ → β<VAR>g : α → γ<GOAL>∏ a ∈ s, f (g a) = ∏ b ∈ Finset.image g s, f b ^ (Finset.filter (fun a => g a = b) s).card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>DecidableEq γ<VAR>f : γ → β<VAR>g : α → γ<GOAL>∑ a ∈ s, f (g a) = ∑ b ∈ Finset.image g s, (Finset.filter (fun a => g a = b) s).card • f b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>f g : α → β<GOAL>∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>f g : α → β<GOAL>∑ x ∈ s, t.piecewise f g x = ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>f : α → β<GOAL>∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>f : α → β<GOAL>(∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<GOAL>∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<GOAL>∑ x ∈ s, f x = f i + ∑ x ∈ s \ {i}, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<GOAL>∑ x ∈ s, f x = ∑ x ∈ s \ {i}, f x + f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<GOAL>∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>Fintype α<VAR>a : α<VAR>f : α → β<GOAL>∏ i : α, f i = f a * ∏ i ∈ {a}ᶜ, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>Fintype α<VAR>a : α<VAR>f : α → β<GOAL>∑ i : α, f i = f a + ∑ i ∈ {a}ᶜ, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>Fintype α<VAR>a : α<VAR>f : α → β<GOAL>∏ i : α, f i = (∏ i ∈ {a}ᶜ, f i) * f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>Fintype α<VAR>a : α<VAR>f : α → β<GOAL>∑ i : α, f i = ∑ i ∈ {a}ᶜ, f i + f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : α → β<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∈ s<GOAL>f a ∣ ∏ i ∈ s, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>R : Setoid α<VAR>DecidableRel Setoid.r<GOAL>∑ x ∈ s, f x = ∑ xbar ∈ Finset.image Quotient.mk'' s, ∑ y ∈ Finset.filter (fun x => ⟦x⟧ = xbar) s, f y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>R : Setoid α<VAR>DecidableRel Setoid.r<GOAL>∏ x ∈ s, f x = ∏ xbar ∈ Finset.image Quotient.mk'' s, ∏ y ∈ Finset.filter (fun x => ⟦x⟧ = xbar) s, f y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>R : Setoid α<VAR>DecidableRel Setoid.r<VAR>h : ∀ x ∈ s, ∑ a ∈ Finset.filter (fun y => y ≈ x) s, f a = 0<GOAL>∑ x ∈ s, f x = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>R : Setoid α<VAR>DecidableRel Setoid.r<VAR>h : ∀ x ∈ s, ∏ a ∈ Finset.filter (fun y => y ≈ x) s, f a = 1<GOAL>∏ x ∈ s, f x = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∉ s<VAR>f : α → β<VAR>b : β<GOAL>∑ x ∈ s, Function.update f i b x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∉ s<VAR>f : α → β<VAR>b : β<GOAL>∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<VAR>b : β<GOAL>∑ x ∈ s, Function.update f i b x = b + ∑ x ∈ s \ {i}, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<VAR>b : β<GOAL>∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>hc : s.card ≤ 1<VAR>f : α → β<VAR>b : β<VAR>h : ∏ x ∈ s, f x = b<VAR>x : α<GOAL>x ∈ s → f x = b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>hc : s.card ≤ 1<VAR>f : α → β<VAR>b : β<VAR>h : ∑ x ∈ s, f x = b<VAR>x : α<GOAL>x ∈ s → f x = b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>(∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : f a = 0<GOAL>∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : f a = 1<GOAL>∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j<VAR>a : β<GOAL>(∑ i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then a else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j<VAR>a : β<GOAL>(∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1
<VAR>α : Type u_3<VAR>γ : Type u_6<VAR>DecidableEq α<VAR>OrderedCommMonoid γ<VAR>CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>s : Finset α<VAR>d : α<VAR>hd : d ∈ s<VAR>f : α → γ<VAR>hdf : 1 < f d<GOAL>∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m
<VAR>α : Type u_3<VAR>γ : Type u_6<VAR>DecidableEq α<VAR>OrderedAddCommMonoid γ<VAR>CovariantClass γ γ (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>s : Finset α<VAR>d : α<VAR>hd : d ∈ s<VAR>f : α → γ<VAR>hdf : 0 < f d<GOAL>∑ m ∈ s.erase d, f m < ∑ m ∈ s, f m
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>hp : ∑ x ∈ s, f x = 0<VAR>h1 : ∀ x ∈ s, x ≠ a → f x = 0<VAR>x : α<GOAL>x ∈ s → f x = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>hp : ∏ x ∈ s, f x = 1<VAR>h1 : ∀ x ∈ s, x ≠ a → f x = 1<VAR>x : α<GOAL>x ∈ s → f x = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<GOAL>∑ x ∈ s, (if a = x then 1 else 0) • f x = if a ∈ s then f a else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<GOAL>(∏ x ∈ s, f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>S : Finset α<VAR>g1 g2 : α → β<VAR>h : ∀ a ∈ S, g1 a ∣ g2 a<GOAL>S.prod g1 ∣ S.prod g2
<VAR>ι : Type u_6<VAR>M : Type u_7<VAR>CommMonoid M<VAR>s t : Finset ι<VAR>f : ι → M<VAR>h : s ⊆ t<GOAL>∏ i ∈ s, f i ∣ ∏ i ∈ t, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>b₁ b₂ : β<VAR>a : α<VAR>ha : a ∈ s<VAR>h : f a * b₁ = f a * b₂<GOAL>(∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>b₁ b₂ : β<VAR>a : α<VAR>ha : a ∈ s<VAR>h : f a + b₁ = f a + b₂<GOAL>∑ a ∈ s, f a + b₁ = ∑ a ∈ s, f a + b₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>s : Finset ι<VAR>AddCommMonoid α<VAR>f : ι → α<VAR>h : ∀ c ∈ s, Even (f c)<GOAL>Even (∑ i ∈ s, f i)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>s : Finset ι<VAR>CommMonoid α<VAR>f : ι → α<VAR>h : ∀ c ∈ s, IsSquare (f c)<GOAL>IsSquare (∏ i ∈ s, f i)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>DecidableEq ι<VAR>CancelCommMonoid α<VAR>s t : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ s \ t, f i = ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i = ∏ i ∈ t, f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>DecidableEq ι<VAR>AddCancelCommMonoid α<VAR>s t : Finset ι<VAR>f : ι → α<GOAL>∑ i ∈ s \ t, f i = ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i = ∑ i ∈ t, f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>DecidableEq ι<VAR>AddCancelCommMonoid α<VAR>s t : Finset ι<VAR>f : ι → α<GOAL>∑ i ∈ s \ t, f i ≠ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≠ ∑ i ∈ t, f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>DecidableEq ι<VAR>CancelCommMonoid α<VAR>s t : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ s \ t, f i ≠ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≠ ∏ i ∈ t, f i
<VAR>α : Type u_3<VAR>s : Finset α<GOAL>s.card = ∑ x ∈ s, 1
<VAR>α : Type u_3<VAR>s : Finset α<VAR>m : ℕ<VAR>f : α → ℕ<VAR>h₁ : ∀ x ∈ s, f x = m<GOAL>∑ x ∈ s, f x = s.card * m
<VAR>ι : Type u_1<VAR>κ : Type u_6<VAR>DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<GOAL>∑ j ∈ t, (Finset.filter (fun i => g i = j) s).card = (Finset.filter (fun i => g i ∈ t) s).card
<VAR>α : Type u_3<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>(Finset.filter p s).card = ∑ a ∈ s, if p a then 1 else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>MulOpposite.op (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.op (f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → βᵐᵒᵖ<GOAL>MulOpposite.unop (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.unop (f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>DivisionCommMonoid β<GOAL>∏ x ∈ s, (f x)⁻¹ = (∏ x ∈ s, f x)⁻¹
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>SubtractionCommMonoid β<GOAL>∑ x ∈ s, -f x = -∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f g : α → β<VAR>SubtractionCommMonoid β<GOAL>∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f g : α → β<VAR>DivisionCommMonoid β<GOAL>∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SubtractionCommMonoid β<VAR>f : α → β<VAR>s : Finset α<VAR>n : ℤ<GOAL>∑ a ∈ s, n • f a = n • ∑ a ∈ s, f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>DivisionCommMonoid β<VAR>f : α → β<VAR>s : Finset α<VAR>n : ℤ<GOAL>∏ a ∈ s, f a ^ n = (∏ a ∈ s, f a) ^ n
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>CommGroup β<VAR>DecidableEq α<VAR>h : s₁ ⊆ s₂<GOAL>∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>AddCommGroup β<VAR>DecidableEq α<VAR>h : s₁ ⊆ s₂<GOAL>∑ x ∈ s₂ \ s₁, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>CommGroup β<VAR>DecidableEq α<GOAL>(∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>AddCommGroup β<VAR>DecidableEq α<GOAL>∑ x ∈ s₂ \ s₁, f x - ∑ x ∈ s₁ \ s₂, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommGroup β<VAR>DecidableEq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommGroup β<VAR>DecidableEq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - f a
<VAR>α : Type u_3<VAR>σ : α → Type u_6<VAR>s : Finset α<VAR>t : (a : α) → Finset (σ a)<GOAL>(s.sigma t).card = ∑ a ∈ s, (t a).card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>t : α → Finset β<VAR>h : (↑s).PairwiseDisjoint t<GOAL>(s.disjiUnion t h).card = ∑ i ∈ s, (t i).card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : α → Finset β<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)<GOAL>(s.biUnion t).card = ∑ u ∈ s, (t u).card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : α → Finset β<GOAL>(s.biUnion t).card ≤ ∑ a ∈ s, (t a).card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>H : ∀ x ∈ s, f x ∈ t<GOAL>s.card = ∑ a ∈ t, (Finset.filter (fun x => f x = a) s).card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>s.card = ∑ a ∈ Finset.image f s, (Finset.filter (fun x => f x = a) s).card
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → Multiset β<VAR>s : Finset α<VAR>b : β<GOAL>b ∈ ∑ x ∈ s, f x ↔ ∃ a ∈ s, b ∈ f a
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>Unique α<VAR>s : Finset α<VAR>f : α → β<VAR>h : s.Nonempty<GOAL>∑ x ∈ s, f x = f default
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>CommMonoid β<VAR>Unique α<VAR>s : Finset α<VAR>f : α → β<VAR>h : s.Nonempty<GOAL>∏ x ∈ s, f x = f default
<VAR>α : Type u_3<VAR>s : Finset α<VAR>n : ℕ<VAR>f : α → ℕ<GOAL>(∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n
<VAR>α : Type u_3<VAR>s : Finset α<VAR>n : ℕ<VAR>f : α → ℕ<GOAL>(∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n
<VAR>α : Type u_3<VAR>s : Finset α<VAR>n : ℤ<VAR>f : α → ℤ<GOAL>(∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n
<VAR>α : Type u_3<VAR>s : Finset α<VAR>n : ℤ<VAR>f : α → ℤ<GOAL>(∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>CommMonoid α<VAR>e : ι → κ<VAR>he : Function.Bijective e<VAR>f : ι → α<VAR>g : κ → α<VAR>h : ∀ (x : ι), f x = g (e x)<GOAL>∏ x : ι, f x = ∏ x : κ, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>AddCommMonoid α<VAR>e : ι → κ<VAR>he : Function.Bijective e<VAR>f : ι → α<VAR>g : κ → α<VAR>h : ∀ (x : ι), f x = g (e x)<GOAL>∑ x : ι, f x = ∑ x : κ, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>AddCommMonoid α<VAR>e : ι ≃ κ<VAR>f : ι → α<VAR>g : κ → α<VAR>h : ∀ (x : ι), f x = g (e x)<GOAL>∑ x : ι, f x = ∑ x : κ, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>CommMonoid α<VAR>e : ι ≃ κ<VAR>f : ι → α<VAR>g : κ → α<VAR>h : ∀ (x : ι), f x = g (e x)<GOAL>∏ x : ι, f x = ∏ x : κ, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>CommMonoid α<VAR>e : ι → κ<VAR>he : Function.Bijective e<VAR>g : κ → α<GOAL>∏ i : ι, g (e i) = ∏ i : κ, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>AddCommMonoid α<VAR>e : ι → κ<VAR>he : Function.Bijective e<VAR>g : κ → α<GOAL>∑ i : ι, g (e i) = ∑ i : κ, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>AddCommMonoid α<VAR>e : ι ≃ κ<VAR>g : κ → α<GOAL>∑ i : ι, g (e i) = ∑ i : κ, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>CommMonoid α<VAR>e : ι ≃ κ<VAR>g : κ → α<GOAL>∏ i : ι, g (e i) = ∏ i : κ, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>CommMonoid α<VAR>e : ι → κ<VAR>he : Function.Injective e<VAR>f : ι → α<VAR>g : κ → α<VAR>h' : ∀ i ∉ Set.range e, g i = 1<VAR>h : ∀ (i : ι), f i = g (e i)<GOAL>∏ i : ι, f i = ∏ j : κ, g j
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>AddCommMonoid α<VAR>e : ι → κ<VAR>he : Function.Injective e<VAR>f : ι → α<VAR>g : κ → α<VAR>h' : ∀ i ∉ Set.range e, g i = 0<VAR>h : ∀ (i : ι), f i = g (e i)<GOAL>∑ i : ι, f i = ∑ j : κ, g j