α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
haveI := Classical.decEq γ
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
calc
  (∏ x in preimage s f hf, g (f x)) = ∏ x in image f (preimage s f hf), g x :=
    Eq.symm <| prod_image <| by simpa only [mem_preimage, InjOn] using hf
  _ = ∏ x in s.filter fun x => x ∈ Set.range f, g x := by rw [image_preimage]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∀ (x : α), x ∈ preimage s f hf → ∀ (y : α), y ∈ preimage s f hf → f x = f y → x = y
simpa only [mem_preimage, InjOn] using hf
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∏ x in image f (preimage s f hf), g x = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
rw [image_preimage]