Theorem: Function.Injective.image_iInter_eq (Jordan/Mathlib/Set.lean)

State before:
α✝ : Type u_1
α : Type u_3
β : Type u_4
G : Type ?u.14473
X : Type ?u.14476
ι : Sort u_2
κ : ι → Sort ?u.14484
inst✝ : Nonempty ι
f : α → β
hf : Injective f
s : ι → Set α
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i
Tactic:
rw [Set.InjOn.image_iInter_eq (Set.injOn_of_injective hf _)]
State after:
no goals