Sums and products over preimages of finite sets.

theorem Finset.prod_preimage' {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [CommMonoid β] (f : ι → κ) [DecidablePred fun (x : κ) => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) : ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ filter (fun (x : κ) => x ∈ Set.range f) s, g x

theorem Finset.sum_preimage' {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [AddCommMonoid β] (f : ι → κ) [DecidablePred fun (x : κ) => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) : ∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ filter (fun (x : κ) => x ∈ Set.range f) s, g x

theorem Finset.prod_preimage {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [CommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1) : ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

theorem Finset.sum_preimage {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [AddCommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 0) : ∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ s, g x

theorem Finset.prod_preimage_of_bij {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [CommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) : ∏ x ∈ s.preimage f ⋯, g (f x) = ∏ x ∈ s, g x

theorem Finset.sum_preimage_of_bij {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [AddCommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) : ∑ x ∈ s.preimage f ⋯, g (f x) = ∑ x ∈ s, g x