α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(image f (preimage s f hf)) = ↑(filter (fun x => x ∈ Set.range f) s)
simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range,
  ← Set.sep_mem_eq]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}
rfl