ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>g : γ → α<GOAL>(∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∑ x ∈ Finset.image g s, f x = ∑ x ∈ s, f (g x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>e : α ↪ γ<VAR>f : γ → β<GOAL>∑ x ∈ Finset.map e s, f x = ∑ x ∈ s, f (e x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset α<VAR>e : α ↪ γ<VAR>f : γ → β<GOAL>∏ x ∈ Finset.map e s, f x = ∏ x ∈ s, f (e x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f g : α → β<VAR>AddCommMonoid β<VAR>h : s₁ = s₂<GOAL>(∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f g : α → β<VAR>CommMonoid β<VAR>h : s₁ = s₂<GOAL>(∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : α → β<VAR>s : Finset α<VAR>h : ∀ x ∈ s, f x = 1<GOAL>∏ x ∈ s, f x = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : α → β<VAR>s : Finset α<VAR>h : ∀ x ∈ s, f x = 0<GOAL>∑ x ∈ s, f x = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>h : Disjoint s₁ s₂<GOAL>∏ x ∈ s₁.disjUnion s₂ h, 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>AddCommMonoid β<VAR>h : Disjoint s₁ s₂<GOAL>∑ x ∈ s₁.disjUnion s₂ h, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>CommMonoid β<VAR>s : Finset ι<VAR>t : ι → Finset α<VAR>h : (↑s).PairwiseDisjoint t<GOAL>∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>AddCommMonoid β<VAR>s : Finset ι<VAR>t : ι → Finset α<VAR>h : (↑s).PairwiseDisjoint t<GOAL>∑ x ∈ s.disjiUnion t h, f x = ∑ i ∈ s, ∑ x ∈ t i, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<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>CommMonoid β<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>AddCommMonoid β<VAR>DecidableEq α<VAR>h : Disjoint 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>CommMonoid β<VAR>DecidableEq α<VAR>h : Disjoint 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>CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>(x : α) → Decidable ¬p x<VAR>f : α → β<GOAL>(∏ x ∈ Finset.filter p s, f x) * ∏ x ∈ Finset.filter (fun x => ¬p x) s, 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>(x : α) → Decidable ¬p x<VAR>f : α → β<GOAL>∑ x ∈ Finset.filter p s, f x + ∑ x ∈ Finset.filter (fun x => ¬p x) s, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>(List.map f s.toList).sum = s.sum f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>(List.map f s.toList).prod = s.prod f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>∑ x ∈ s, f (σ x) = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>∑ x ∈ s, f (σ x) x = ∑ x ∈ s, f x ((Equiv.symm σ) x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>∑ t ∈ (insert a s).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset, f (insert a t)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>CommMonoid β<VAR>DecidableEq α<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>AddCommMonoid β<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>∑ t ∈ (Finset.cons a s ha).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>CommMonoid β<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>∏ t ∈ (Finset.cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : Finset α → β<GOAL>∑ t ∈ s.powerset, f t = ∑ j ∈ Finset.range (s.card + 1), ∑ t ∈ Finset.powersetCard j s, f t
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : Finset α → β<GOAL>∏ t ∈ s.powerset, f t = ∏ j ∈ Finset.range (s.card + 1), ∏ t ∈ Finset.powersetCard j s, f t
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Fintype α<VAR>AddCommMonoid β<VAR>s t : Finset α<VAR>h : IsCompl s t<VAR>f : α → β<GOAL>∑ i ∈ s, f i + ∑ i ∈ t, f i = ∑ i : α, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Fintype α<VAR>CommMonoid β<VAR>s t : Finset α<VAR>h : IsCompl s t<VAR>f : α → β<GOAL>(∏ i ∈ s, f i) * ∏ i ∈ t, f i = ∏ i : α, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<GOAL>(∏ i ∈ s, f i) * ∏ i ∈ sᶜ, f i = ∏ i : α, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<GOAL>∑ i ∈ s, f i + ∑ i ∈ sᶜ, f i = ∑ i : α, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<GOAL>∑ i ∈ sᶜ, f i + ∑ i ∈ s, f i = ∑ i : α, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → β<GOAL>(∏ i ∈ sᶜ, f i) * ∏ i ∈ s, f i = ∏ i : α, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<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>CommMonoid β<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 g : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>h : s₁ ⊆ s₂<VAR>hg : ∀ x ∈ s₂ \ s₁, g x = 1<VAR>hfg : ∀ x ∈ s₁, f x = g x<GOAL>∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f g : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>h : s₁ ⊆ s₂<VAR>hg : ∀ x ∈ s₂ \ s₁, g x = 0<VAR>hfg : ∀ x ∈ s₁, f x = g x<GOAL>∑ i ∈ s₁, f i = ∑ i ∈ s₂, g i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>h : s₁ ⊆ s₂<VAR>hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 0<GOAL>∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s₁ s₂ : Finset α<VAR>f : α → β<VAR>CommMonoid β<VAR>h : s₁ ⊆ s₂<VAR>hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1<GOAL>∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>t : Finset γ<VAR>f : α ⊕ γ → β<GOAL>∑ x ∈ s.disjSum t, f x = ∑ x ∈ s, f (Sum.inl x) + ∑ x ∈ t, f (Sum.inr x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset α<VAR>t : Finset γ<VAR>f : α ⊕ γ → β<GOAL>∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr 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 : γ → β<GOAL>∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g 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 : γ → β<GOAL>∑ x ∈ s.disjSum t, Sum.elim f g x = ∑ x ∈ s, f x + ∑ x ∈ t, g x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>hs : (↑s).PairwiseDisjoint t<GOAL>∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>hs : (↑s).PairwiseDisjoint t<GOAL>∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>σ : α → Type u_6<VAR>s : Finset α<VAR>t : (a : α) → Finset (σ a)<VAR>f : Sigma σ → β<GOAL>∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>σ : α → Type u_6<VAR>s : Finset α<VAR>t : (a : α) → Finset (σ a)<VAR>f : Sigma σ → β<GOAL>∑ x ∈ s.sigma t, f x = ∑ a ∈ s, ∑ s ∈ t a, f ⟨a, s⟩
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>σ : α → Type u_6<VAR>s : Finset α<VAR>t : (a : α) → Finset (σ a)<VAR>f : (a : α) → σ a → β<GOAL>∏ a ∈ s, ∏ s ∈ t a, f a s = ∏ x ∈ s.sigma t, f x.fst x.snd
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>σ : α → Type u_6<VAR>s : Finset α<VAR>t : (a : α) → Finset (σ a)<VAR>f : (a : α) → σ a → β<GOAL>∑ a ∈ s, ∑ s ∈ t a, f a s = ∑ x ∈ s.sigma t, f x.fst x.snd
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : (a : ι) → a ∈ s → κ<VAR>hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t<VAR>i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂<VAR>i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b<VAR>h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)<GOAL>∏ x ∈ s, f x = ∏ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : (a : ι) → a ∈ s → κ<VAR>hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t<VAR>i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂<VAR>i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b<VAR>h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)<GOAL>∑ x ∈ s, f x = ∑ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : (a : ι) → a ∈ s → κ<VAR>j : (a : κ) → a ∈ t → ι<VAR>hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t<VAR>hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s<VAR>left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a<VAR>right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a<VAR>h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)<GOAL>∏ x ∈ s, f x = ∏ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : (a : ι) → a ∈ s → κ<VAR>j : (a : κ) → a ∈ t → ι<VAR>hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t<VAR>hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s<VAR>left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a<VAR>right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a<VAR>h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)<GOAL>∑ x ∈ s, f x = ∑ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : ι → κ<VAR>hi : ∀ a ∈ s, i a ∈ t<VAR>i_inj : Set.InjOn i ↑s<VAR>i_surj : Set.SurjOn i ↑s ↑t<VAR>h : ∀ a ∈ s, f a = g (i a)<GOAL>∑ x ∈ s, f x = ∑ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : ι → κ<VAR>hi : ∀ a ∈ s, i a ∈ t<VAR>i_inj : Set.InjOn i ↑s<VAR>i_surj : Set.SurjOn i ↑s ↑t<VAR>h : ∀ a ∈ s, f a = g (i a)<GOAL>∏ x ∈ s, f x = ∏ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : ι → κ<VAR>j : κ → ι<VAR>hi : ∀ a ∈ s, i a ∈ t<VAR>hj : ∀ a ∈ t, j a ∈ s<VAR>left_inv : ∀ a ∈ s, j (i a) = a<VAR>right_inv : ∀ a ∈ t, i (j a) = a<VAR>h : ∀ a ∈ s, f a = g (i a)<GOAL>∑ x ∈ s, f x = ∑ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : ι → κ<VAR>j : κ → ι<VAR>hi : ∀ a ∈ s, i a ∈ t<VAR>hj : ∀ a ∈ t, j a ∈ s<VAR>left_inv : ∀ a ∈ s, j (i a) = a<VAR>right_inv : ∀ a ∈ t, i (j a) = a<VAR>h : ∀ a ∈ s, f a = g (i a)<GOAL>∏ x ∈ s, f x = ∏ x ∈ t, g x
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι ≃ κ<VAR>hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t<VAR>hfg : ∀ i ∈ s, f i = g (e i)<GOAL>∏ i ∈ s, f i = ∏ i ∈ t, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι ≃ κ<VAR>hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t<VAR>hfg : ∀ i ∈ s, f i = g (e i)<GOAL>∑ i ∈ s, f i = ∑ i ∈ t, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Function.Bijective e<VAR>hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t<VAR>hfg : ∀ i ∈ s, f i = g (e i)<GOAL>∑ i ∈ s, f i = ∑ i ∈ t, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Function.Bijective e<VAR>hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t<VAR>hfg : ∀ i ∈ s, f i = g (e i)<GOAL>∏ i ∈ s, f i = ∏ i ∈ t, g i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Set.InjOn e ↑s<VAR>hest : Set.MapsTo e ↑s ↑t<VAR>h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1<VAR>h : ∀ i ∈ s, f i = g (e i)<GOAL>∏ i ∈ s, f i = ∏ j ∈ t, g j
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Set.InjOn e ↑s<VAR>hest : Set.MapsTo e ↑s ↑t<VAR>h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 0<VAR>h : ∀ i ∈ s, f i = g (e i)<GOAL>∑ i ∈ s, f i = ∑ j ∈ t, g j
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∏ j ∈ t, ∏ i ∈ Finset.filter (fun i => g i = j) s, f i = ∏ i ∈ Finset.filter (fun i => g i ∈ t) s, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∑ j ∈ t, ∑ i ∈ Finset.filter (fun i => g i = j) s, f i = ∑ i ∈ Finset.filter (fun i => g i ∈ t) s, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∏ j ∈ t, ∏ _i ∈ Finset.filter (fun i => g i = j) s, f j = ∏ i ∈ Finset.filter (fun i => g i ∈ t) s, f (g i)
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∑ j ∈ t, ∑ _i ∈ Finset.filter (fun i => g i = j) s, f j = ∑ i ∈ Finset.filter (fun i => g i ∈ t) s, f (g i)
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>h : ∀ i ∈ s, g i ∈ t<VAR>f : ι → α<GOAL>∏ j ∈ t, ∏ i ∈ Finset.filter (fun i => g i = j) s, f i = ∏ i ∈ s, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>h : ∀ i ∈ s, g i ∈ t<VAR>f : ι → α<GOAL>∑ j ∈ t, ∑ i ∈ Finset.filter (fun i => g i = j) s, f i = ∑ i ∈ s, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>h : ∀ i ∈ s, g i ∈ t<VAR>f : κ → α<GOAL>∑ j ∈ t, ∑ _i ∈ Finset.filter (fun i => g i = j) s, f j = ∑ i ∈ s, f (g i)
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>h : ∀ i ∈ s, g i ∈ t<VAR>f : κ → α<GOAL>∏ j ∈ t, ∏ _i ∈ Finset.filter (fun i => g i = j) s, f j = ∏ i ∈ s, f (g i)
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>DecidableEq κ<VAR>Fintype κ<VAR>s : Finset ι<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∑ j : κ, ∑ i ∈ Finset.filter (fun i => g i = j) s, f i = ∑ i ∈ s, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>DecidableEq κ<VAR>Fintype κ<VAR>s : Finset ι<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∏ j : κ, ∏ i ∈ Finset.filter (fun i => g i = j) s, f i = ∏ i ∈ s, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>CommMonoid α<VAR>DecidableEq κ<VAR>Fintype κ<VAR>s : Finset ι<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∏ j : κ, ∏ _i ∈ Finset.filter (fun i => g i = j) s, f j = ∏ i ∈ s, f (g i)
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>DecidableEq κ<VAR>Fintype κ<VAR>s : Finset ι<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∑ j : κ, ∑ _i ∈ Finset.filter (fun i => g i = j) s, f j = ∑ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq ι<VAR>Fintype ι<VAR>κ : ι → Type u_6<VAR>t : (i : ι) → Finset (κ i)<VAR>f : ((i : ι) → i ∈ Finset.univ → κ i) → β<GOAL>∑ x ∈ Finset.univ.pi t, f x = ∑ x ∈ Fintype.piFinset t, f fun a x_1 => x a
<VAR>ι : Type u_1<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq ι<VAR>Fintype ι<VAR>κ : ι → Type u_6<VAR>t : (i : ι) → Finset (κ i)<VAR>f : ((i : ι) → i ∈ Finset.univ → κ i) → β<GOAL>∏ x ∈ Finset.univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a x_1 => x a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α × α → β<GOAL>∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α × α → β<GOAL>∑ i ∈ s.diag, f i = ∑ i ∈ s, f (i, i)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>r : Finset (γ × α)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1<VAR>f : γ × α → β<GOAL>∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>r : Finset (γ × α)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1<VAR>f : γ × α → β<GOAL>∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (c, a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>r : Finset (γ × α)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1<VAR>f : γ → α → β<GOAL>∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f c a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>r : Finset (γ × α)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1<VAR>f : γ → α → β<GOAL>∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f c a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>r : Finset (α × γ)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2<VAR>f : α × γ → β<GOAL>∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (a, c)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>r : Finset (α × γ)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2<VAR>f : α × γ → β<GOAL>∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>r : Finset (α × γ)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2<VAR>f : α → γ → β<GOAL>∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f a c
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>r : Finset (α × γ)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2<VAR>f : α → γ → β<GOAL>∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f a c
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>g : γ → α<VAR>h : γ → β<VAR>eq : ∀ c ∈ s, f (g c) = ∑ x ∈ Finset.filter (fun c' => g c' = g c) s, h x<GOAL>∑ x ∈ Finset.image g s, f x = ∑ x ∈ s, h x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>g : γ → α<VAR>h : γ → β<VAR>eq : ∀ c ∈ s, f (g c) = ∏ x ∈ Finset.filter (fun c' => g c' = g c) s, h x<GOAL>∏ x ∈ Finset.image g s, f x = ∏ x ∈ s, h x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>f g : α → β<VAR>AddCommMonoid β<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>CommMonoid β<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>AddCommMonoid β<VAR>f g h i : α → β<GOAL>∑ a ∈ s, (f a + g a) + ∑ a ∈ s, (h a + i a) = ∑ a ∈ s, (f a + h a) + ∑ a ∈ s, (g a + i a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<VAR>f g h i : α → β<GOAL>(∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ × α → β<GOAL>∏ x ∈ s ×ˢ t, f x = ∏ x ∈ s, ∏ y ∈ t, f (x, y)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ × α → β<GOAL>∑ x ∈ s ×ˢ t, f x = ∑ x ∈ s, ∑ y ∈ t, f (x, y)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ → α → β<GOAL>∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ → α → β<GOAL>∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ x ∈ s, ∑ y ∈ t, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ × α → β<GOAL>∑ x ∈ s ×ˢ t, f x = ∑ y ∈ t, ∑ x ∈ s, f (x, y)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ × α → β<GOAL>∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ → α → β<GOAL>∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ y ∈ t, ∑ x ∈ s, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ → α → β<GOAL>∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>t' : Finset α<VAR>s' : α → Finset γ<VAR>h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'<VAR>f : γ → α → β<GOAL>∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>t' : Finset α<VAR>s' : α → Finset γ<VAR>h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'<VAR>f : γ → α → β<GOAL>∑ x ∈ s, ∑ y ∈ t x, f x y = ∑ y ∈ t', ∑ x ∈ s' y, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ → α → β<GOAL>∑ x ∈ s, ∑ y ∈ t, f x y = ∑ y ∈ t, ∑ x ∈ s, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>s : Finset γ<VAR>t : Finset α<VAR>f : γ → α → β<GOAL>∏ x ∈ s, ∏ y ∈ t, f x y = ∏ y ∈ t, ∏ x ∈ s, f x y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>r : β → γ → Prop<VAR>f : α → β<VAR>g : α → γ<VAR>s : Finset α<VAR>h₁ : r 0 0<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)