no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in s, g x
classical
  rw [prod_preimage', prod_filter_of_ne]
  exact fun x hx => Not.imp_symm (hg x hx)
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∀ (x : γ), x ∈ s → g x ≠ 1 → x ∈ Set.range f
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in s, g x
rw [prod_preimage', prod_filter_of_ne]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∀ (x : γ), x ∈ s → g x ≠ 1 → x ∈ Set.range f
exact fun x hx => Not.imp_symm (hg x hx)