no goals
α : Type u_2
β : Type ?u.199050
γ : Type ?u.199053
ι✝ : Sort ?u.199056
ι' : Sort ?u.199059
ι₂ : Sort ?u.199062
κ : ι✝ → Sort ?u.199067
κ₁ : ι✝ → Sort ?u.199072
κ₂ : ι✝ → Sort ?u.199077
κ' : ι' → Sort ?u.199082
ι : Sort u_1
f : ι → α
a : α
⊢ a ∈ range f ↔ a ∈ ⋃ (i : ι), {f i}
simp [@eq_comm α a]