ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>CommMonoid γ<VAR>r : β → γ → Prop<VAR>f : α → β<VAR>g : α → γ<VAR>s : Finset α<VAR>h₁ : r 1 1<VAR>h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)<GOAL>r (∏ x ∈ s, f x) (∏ x ∈ s, g x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : ∀ x ∈ s, f x ≠ 1 → p x<GOAL>∏ x ∈ Finset.filter p s, f x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : ∀ x ∈ s, f x ≠ 0 → p x<GOAL>∑ x ∈ Finset.filter p s, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>CommMonoid β<VAR>s : Finset α<VAR>(x : α) → Decidable (f x ≠ 1)<GOAL>∏ x ∈ Finset.filter (fun x => f x ≠ 1) s, f x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>(x : α) → Decidable (f x ≠ 0)<GOAL>∑ x ∈ Finset.filter (fun x => f x ≠ 0) s, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → β<GOAL>∑ a ∈ Finset.filter p s, f a = ∑ a ∈ s, if p a then f a else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → β<GOAL>∏ a ∈ Finset.filter p s, f a = ∏ a ∈ s, if p a then f a else 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<VAR>h₀ : ∀ b ∈ s, b ≠ a → f b = 0<GOAL>∑ x ∈ s, f x = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<VAR>h₀ : ∀ b ∈ s, b ≠ a → f b = 1<GOAL>∏ x ∈ s, f x = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h₀ : ∀ b ∈ s, b ≠ a → f b = 0<VAR>h₁ : a ∉ s → f a = 0<GOAL>∑ x ∈ s, f x = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h₀ : ∀ b ∈ s, b ≠ a → f b = 1<VAR>h₁ : a ∉ s → f a = 1<GOAL>∏ x ∈ s, f x = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1<GOAL>∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₁, f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 0<GOAL>∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₁, f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1<GOAL>∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 0<GOAL>∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₂, f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0<GOAL>∑ x ∈ s, f x = f a + f b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1<GOAL>∏ x ∈ s, f x = f a * f b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1<VAR>ha : a ∉ s → f a = 1<VAR>hb : b ∉ s → f b = 1<GOAL>∏ x ∈ s, f x = f a * f b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0<VAR>ha : a ∉ s → f a = 0<VAR>hb : b ∉ s → f b = 0<GOAL>∑ x ∈ s, f x = f a + f b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ Finset.filter p s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ Finset.filter p s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>h : ∀ x ∈ s, p x<GOAL>∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>h : ∀ x ∈ s, p x<GOAL>∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>f : { x // p x } → β<VAR>g : α → β<VAR>h : ∀ x ∈ s, g ↑x = f x<GOAL>∑ x ∈ Finset.map (Function.Embedding.subtype fun x => p x) s, g x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>f : { x // p x } → β<VAR>g : α → β<VAR>h : ∀ x ∈ s, g ↑x = f x<GOAL>∏ x ∈ Finset.map (Function.Embedding.subtype fun x => p x) s, g x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>f : { x // x ∈ s } → β<GOAL>∏ i : { x // x ∈ s }, f i = ∏ i ∈ s.attach, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>f : { x // x ∈ s } → β<GOAL>∑ i : { x // x ∈ s }, f i = ∑ i ∈ s.attach, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<GOAL>∑ i : { x // x ∈ s }, f ↑i = ∑ i ∈ s, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<GOAL>∏ i : { x // x ∈ s }, f ↑i = ∏ i ∈ s, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : α → β<VAR>s : Finset α<GOAL>∑ i : ↑↑s, f ↑i = ∑ i ∈ s, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : α → β<VAR>s : Finset α<GOAL>∏ i : ↑↑s, f ↑i = ∏ i ∈ s, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>p : α → Prop<VAR>F : Fintype (Subtype p)<VAR>s : Finset α<VAR>h : ∀ (x : α), x ∈ s ↔ p x<VAR>f : α → β<GOAL>∏ a ∈ s, f a = ∏ a : Subtype p, f ↑a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>p : α → Prop<VAR>F : Fintype (Subtype p)<VAR>s : Finset α<VAR>h : ∀ (x : α), x ∈ s ↔ p x<VAR>f : α → β<GOAL>∑ a ∈ s, f a = ∑ a : Subtype p, f ↑a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ι → κ<VAR>DecidablePred fun x => x ∈ Set.range f<VAR>s : Finset κ<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<VAR>g : κ → β<GOAL>∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ Finset.filter (fun x => x ∈ Set.range f) s, g x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ι → κ<VAR>DecidablePred fun x => x ∈ Set.range f<VAR>s : Finset κ<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<VAR>g : κ → β<GOAL>∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ Finset.filter (fun x => x ∈ Set.range f) s, g x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ι → κ<VAR>s : Finset κ<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<VAR>g : κ → β<VAR>hg : ∀ x ∈ s, x ∉ Set.range f → g x = 0<GOAL>∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ s, g x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ι → κ<VAR>s : Finset κ<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<VAR>g : κ → β<VAR>hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1<GOAL>∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ι → κ<VAR>s : Finset κ<VAR>hf : Set.BijOn f (f ⁻¹' ↑s) ↑s<VAR>g : κ → β<GOAL>∏ x ∈ s.preimage f ⋯, g (f x) = ∏ x ∈ s, g x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ι → κ<VAR>s : Finset κ<VAR>hf : Set.BijOn f (f ⁻¹' ↑s) ↑s<VAR>g : κ → β<GOAL>∑ x ∈ s.preimage f ⋯, g (f x) = ∑ x ∈ s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>AddCommMonoid β<VAR>s : Set α<VAR>Fintype ↑s<GOAL>∑ i : ↑s, f ↑i = ∑ i ∈ s.toFinset, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>CommMonoid β<VAR>s : Set α<VAR>Fintype ↑s<GOAL>∏ i : ↑s, f ↑i = ∏ i ∈ s.toFinset, f i
<VAR>α : Type u_6<VAR>AddCommMonoid α<VAR>β : Type u_7<VAR>Fintype β<VAR>s : Set β<VAR>DecidablePred fun x => x ∈ s<VAR>f : β → α<VAR>g : ↑s → α<VAR>w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩<VAR>w' : ∀ x ∉ s, f x = 0<GOAL>Finset.univ.sum f = Finset.univ.sum g
<VAR>α : Type u_6<VAR>CommMonoid α<VAR>β : Type u_7<VAR>Fintype β<VAR>s : Set β<VAR>DecidablePred fun x => x ∈ s<VAR>f : β → α<VAR>g : ↑s → α<VAR>w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩<VAR>w' : ∀ x ∉ s, f x = 1<GOAL>Finset.univ.prod f = Finset.univ.prod g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>DecidablePred fun x => ¬p x<VAR>f : (x : α) → p x → γ<VAR>g : (x : α) → ¬p x → γ<VAR>h : γ → β<GOAL>∏ x ∈ s, h (if hx : p x then f x hx else g x hx) = (∏ x ∈ (Finset.filter p s).attach, h (f ↑x ⋯)) * ∏ x ∈ (Finset.filter (fun x => ¬p x) s).attach, h (g ↑x ⋯)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>DecidablePred fun x => ¬p x<VAR>f : (x : α) → p x → γ<VAR>g : (x : α) → ¬p x → γ<VAR>h : γ → β<GOAL>∑ x ∈ s, h (if hx : p x then f x hx else g x hx) = ∑ x ∈ (Finset.filter p s).attach, h (f ↑x ⋯) + ∑ x ∈ (Finset.filter (fun x => ¬p x) s).attach, h (g ↑x ⋯)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>_hp : DecidablePred p<VAR>f g : α → γ<VAR>h : γ → β<GOAL>∏ x ∈ s, h (if p x then f x else g x) = (∏ x ∈ Finset.filter p s, h (f x)) * ∏ x ∈ Finset.filter (fun x => ¬p x) s, h (g x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>_hp : DecidablePred p<VAR>f g : α → γ<VAR>h : γ → β<GOAL>∑ x ∈ s, h (if p x then f x else g x) = ∑ x ∈ Finset.filter p s, h (f x) + ∑ x ∈ Finset.filter (fun x => ¬p x) s, h (g x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f : (x : α) → p x → β<VAR>g : (x : α) → ¬p x → β<GOAL>(∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x ∈ (Finset.filter p s).attach, f ↑x ⋯) * ∏ x ∈ (Finset.filter (fun x => ¬p x) s).attach, g ↑x ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f : (x : α) → p x → β<VAR>g : (x : α) → ¬p x → β<GOAL>(∑ x ∈ s, if hx : p x then f x hx else g x hx) = ∑ x ∈ (Finset.filter p s).attach, f ↑x ⋯ + ∑ x ∈ (Finset.filter (fun x => ¬p x) s).attach, g ↑x ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → β<GOAL>(∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ Finset.filter p s, f x + ∑ x ∈ Finset.filter (fun x => ¬p x) s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → β<GOAL>(∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ Finset.filter p s, f x) * ∏ x ∈ Finset.filter (fun x => ¬p x) s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p} (h : ∀ i ∈ s, ¬p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β), (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : { x // x ∈ s }, g ↑i ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p} (h : ∀ i ∈ s, ¬p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β), (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x // x ∈ s }, g ↑i ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p}, (∀ x ∈ s, ¬p x) → ∀ (f g : α → β), (∏ x_1 ∈ s, if p x_1 then f x_1 else g x_1) = ∏ x ∈ s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p}, (∀ x ∈ s, ¬p x) → ∀ (f g : α → β), (∑ x_1 ∈ s, if p x_1 then f x_1 else g x_1) = ∑ x ∈ s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p} (h : ∀ i ∈ s, p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β), (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : { x // x ∈ s }, f ↑i ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p} (h : ∀ i ∈ s, p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β), (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x // x ∈ s }, f ↑i ⋯
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p}, (∀ x ∈ s, p x) → ∀ (f g : α → β), (∏ x_1 ∈ s, if p x_1 then f x_1 else g x_1) = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p}, (∀ x ∈ s, p x) → ∀ (f g : α → β), (∑ x_1 ∈ s, if p x_1 then f x_1 else g x_1) = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<VAR>CommMonoid β<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, ¬p x<GOAL>∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, ¬p x<GOAL>∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (g x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<VAR>CommMonoid β<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, p x<GOAL>∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<VAR>AddCommMonoid β<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, p x<GOAL>∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<GOAL>(∏ i ∈ s, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<GOAL>(∑ i ∈ s, if i ∈ s then f i else 0) = ∑ i ∈ s, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>f : α → β<GOAL>(∏ i ∈ s, if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s t : Finset α<VAR>f : α → β<GOAL>(∑ i ∈ s, if i ∈ t then f i else 0) = ∑ i ∈ s ∩ t, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : (x : α) → a = x → β<GOAL>(∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : (x : α) → a = x → β<GOAL>(∑ x ∈ s, if h : a = x then b x h else 0) = if a ∈ s then b a ⋯ else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : (x : α) → x = a → β<GOAL>(∑ x ∈ s, if h : x = a then b x h else 0) = if a ∈ s then b a ⋯ else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : (x : α) → x = a → β<GOAL>(∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : α → β<GOAL>(∏ x ∈ s, if a = x then b x else 1) = if a ∈ s then b a else 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : α → β<GOAL>(∑ x ∈ s, if a = x then b x else 0) = if a ∈ s then b a else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : α → β<GOAL>(∑ x ∈ s, if x = a then b x else 0) = if a ∈ s then b a else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : α → β<GOAL>(∏ x ∈ s, if x = a then b x else 1) = if a ∈ s then b a else 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>p : Prop<VAR>Decidable p<VAR>s t : Finset α<VAR>f : α → β<GOAL>∑ x ∈ if p then s else t, f x = if p then ∑ x ∈ s, f x else ∑ x ∈ t, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>p : Prop<VAR>Decidable p<VAR>s t : Finset α<VAR>f : α → β<GOAL>∏ x ∈ if p then s else t, f x = if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>p : Prop<VAR>Decidable p<VAR>s : Finset α<VAR>f g : α → β<GOAL>(∑ x ∈ s, if p then f x else g x) = if p then ∑ x ∈ s, f x else ∑ x ∈ s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>p : Prop<VAR>Decidable p<VAR>s : Finset α<VAR>f g : α → β<GOAL>(∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>p : Prop<VAR>Decidable p<VAR>s : Finset α<VAR>f : p → α → β<VAR>g : ¬p → α → β<GOAL>(∑ x ∈ s, if h : p then f h x else g h x) = if h : p then ∑ x ∈ s, f h x else ∑ x ∈ s, g h x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>p : Prop<VAR>Decidable p<VAR>s : Finset α<VAR>f : p → α → β<VAR>g : ¬p → α → β<GOAL>(∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>a : α<VAR>x : β<VAR>s : Finset α<GOAL>∑ a' ∈ s, Pi.single a x a' = if a ∈ s then x else 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>a : α<VAR>x : β<VAR>s : Finset α<GOAL>∏ a' ∈ s, Pi.mulSingle a x a' = if a ∈ s then x else 1
<VAR>α : Type u_3<VAR>β : α → Type u_6<VAR>DecidableEq α<VAR>(a : α) → AddCommMonoid (β a)<VAR>a : α<VAR>f : (a : α) → β a<VAR>s : Finset α<GOAL>∑ a' ∈ s, Pi.single a' (f a') a = if a ∈ s then f a else 0
<VAR>α : Type u_3<VAR>β : α → Type u_6<VAR>DecidableEq α<VAR>(a : α) → CommMonoid (β a)<VAR>a : α<VAR>f : (a : α) → β a<VAR>s : Finset α<GOAL>∏ a' ∈ s, Pi.mulSingle a' (f a') a = if a ∈ s then f a else 1
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset ι<VAR>f : ι → α → β<GOAL>(Function.mulSupport fun x => ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.mulSupport (f i)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset ι<VAR>f : ι → α → β<GOAL>(Function.support fun x => ∑ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.support (f i)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>One α<VAR>f : ι → α<VAR>g : ι → α → β<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>hg : ∀ (a : ι), g a 1 = 1<GOAL>∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>Zero α<VAR>f : ι → α<VAR>g : ι → α → β<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>hg : ∀ (a : ι), g a 0 = 0<GOAL>∑ i ∈ t, g i ((↑s).indicator f i) = ∑ i ∈ s, g i (f i)
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ι → β<VAR>s t : Finset ι<VAR>h : s ⊆ t<GOAL>∏ i ∈ t, (↑s).mulIndicator f i = ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ι → β<VAR>s t : Finset ι<VAR>h : s ⊆ t<GOAL>∑ i ∈ t, (↑s).indicator f i = ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>κ : Type u_6<VAR>s : Finset ι<VAR>f : ι → κ → β<VAR>t : ι → Set κ<VAR>g : ι → κ<VAR>DecidablePred fun i => g i ∈ t i<GOAL>∑ i ∈ s, (t i).indicator (f i) (g i) = ∑ i ∈ Finset.filter (fun i => g i ∈ t i) s, f i (g i)
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>κ : Type u_6<VAR>s : Finset ι<VAR>f : ι → κ → β<VAR>t : ι → Set κ<VAR>g : ι → κ<VAR>DecidablePred fun i => g i ∈ t i<GOAL>∏ i ∈ s, (t i).mulIndicator (f i) (g i) = ∏ i ∈ Finset.filter (fun i => g i ∈ t i) s, f i (g i)
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq ι<VAR>s t : Finset ι<VAR>f : ι → β<GOAL>∑ i ∈ s, (↑t).indicator f i = ∑ i ∈ s ∩ t, f i
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq ι<VAR>s t : Finset ι<VAR>f : ι → β<GOAL>∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s ∩ t, f i
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>κ : Type u_6<VAR>s : Finset ι<VAR>t : Set κ<VAR>f : ι → κ → β<GOAL>t.mulIndicator (∏ i ∈ s, f i) = ∏ i ∈ s, t.mulIndicator (f i)
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>κ : Type u_6<VAR>s : Finset ι<VAR>t : Set κ<VAR>f : ι → κ → β<GOAL>t.indicator (∑ i ∈ s, f i) = ∑ i ∈ s, t.indicator (f i)
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>κ : Type u_7<VAR>s : Finset ι<VAR>t : ι → Set κ<VAR>f : κ → β<GOAL>(↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>κ : Type u_7<VAR>s : Finset ι<VAR>t : ι → Set κ<VAR>f : κ → β<GOAL>(↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).indicator f = fun a => ∑ i ∈ s, (t i).indicator f a
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>κ : Type u_7<VAR>s : Finset ι<VAR>t : ι → Set κ<VAR>f : κ → β<VAR>h : (↑s).PairwiseDisjoint t<VAR>x : κ<GOAL>(⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>κ : Type u_7<VAR>s : Finset ι<VAR>t : ι → Set κ<VAR>f : κ → β<VAR>h : (↑s).PairwiseDisjoint t<VAR>x : κ<GOAL>(⋃ i ∈ s, t i).indicator f x = ∑ i ∈ s, (t i).indicator f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>t : Finset γ<VAR>f : α → β<VAR>g : γ → β<VAR>i : (a : α) → a ∈ s → f a ≠ 0 → γ<VAR>hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ ∈ t<VAR>i_inj : ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 0) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂<VAR>i_surj : ∀ b ∈ t, g b ≠ 0 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ = b<VAR>h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)<GOAL>∑ x ∈ s, f x = ∑ x ∈ t, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset α<VAR>t : Finset γ<VAR>f : α → β<VAR>g : γ → β<VAR>i : (a : α) → a ∈ s → f a ≠ 1 → γ<VAR>hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t<VAR>i_inj : ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂<VAR>i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b<VAR>h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)<GOAL>∏ x ∈ s, f x = ∏ x ∈ t, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>h : ∏ x ∈ s, f x ≠ 1<GOAL>s.Nonempty
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>h : ∑ x ∈ s, f x ≠ 0<GOAL>s.Nonempty
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>h : ∏ x ∈ s, f x ≠ 1<GOAL>∃ a ∈ s, f a ≠ 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>h : ∑ x ∈ s, f x ≠ 0<GOAL>∃ a ∈ s, f a ≠ 0
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∑ x ∈ Finset.range (n + 1), f x = f n + ∑ x ∈ Finset.range n, f x
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∏ x ∈ Finset.range (n + 1), f x = f n * ∏ x ∈ Finset.range n, f x
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∏ x ∈ Finset.range (n + 1), f x = (∏ x ∈ Finset.range n, f x) * f n
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∑ x ∈ Finset.range (n + 1), f x = ∑ x ∈ Finset.range n, f x + f n
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∏ k ∈ Finset.range (n + 1), f k = (∏ k ∈ Finset.range n, f (k + 1)) * f 0
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range (n + 1), f k = ∑ k ∈ Finset.range n, f (k + 1) + f 0
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>u : ℕ → β<VAR>N : ℕ<VAR>hu : ∀ n ≥ N, u n = 1<VAR>n : ℕ<VAR>hn : N ≤ n<GOAL>∏ k ∈ Finset.range n, u k = ∏ k ∈ Finset.range N, u k
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>u : ℕ → β<VAR>N : ℕ<VAR>hu : ∀ n ≥ N, u n = 0<VAR>n : ℕ<VAR>hn : N ≤ n<GOAL>∑ k ∈ Finset.range n, u k = ∑ k ∈ Finset.range N, u k
<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : ℕ → β<VAR>n m : ℕ<GOAL>∑ x ∈ Finset.range (n + m), f x = ∑ x ∈ Finset.range n, f x + ∑ x ∈ Finset.range m, f (n + x)
<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : ℕ → β<VAR>n m : ℕ<GOAL>∏ x ∈ Finset.range (n + m), f x = (∏ x ∈ Finset.range n, f x) * ∏ x ∈ Finset.range m, f (n + x)