case h
α✝ : Type ?u.163313
β✝ : Type ?u.163316
γ : Type ?u.163319
ι : Sort ?u.163322
ι' : Sort ?u.163325
ι₂ : Sort ?u.163328
κ : ι → Sort ?u.163333
κ₁ : ι → Sort ?u.163338
κ₂ : ι → Sort ?u.163343
κ' : ι' → Sort ?u.163348
α : Type u_1
β : Type u_2
f : α → β
x : β
⊢ (x ∈ ⋃ (x : α), {f x}) ↔ x ∈ range f
α✝ : Type ?u.163313
β✝ : Type ?u.163316
γ : Type ?u.163319
ι : Sort ?u.163322
ι' : Sort ?u.163325
ι₂ : Sort ?u.163328
κ : ι → Sort ?u.163333
κ₁ : ι → Sort ?u.163338
κ₂ : ι → Sort ?u.163343
κ' : ι' → Sort ?u.163348
α : Type u_1
β : Type u_2
f : α → β
⊢ (⋃ (x : α), {f x}) = range f
ext x
no goals
case h
α✝ : Type ?u.163313
β✝ : Type ?u.163316
γ : Type ?u.163319
ι : Sort ?u.163322
ι' : Sort ?u.163325
ι₂ : Sort ?u.163328
κ : ι → Sort ?u.163333
κ₁ : ι → Sort ?u.163338
κ₂ : ι → Sort ?u.163343
κ' : ι' → Sort ?u.163348
α : Type u_1
β : Type u_2
f : α → β
x : β
⊢ (x ∈ ⋃ (x : α), {f x}) ↔ x ∈ range f
simp [@eq_comm _ x]