case a
F : Type ?u.416774
α : Type u_1
β : Type u_2
γ : Type ?u.416783
ι : Type ?u.416786
κ : Type ?u.416789
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ sup s fun b => {f b}) ↔ a ∈ image f s
F : Type ?u.416774
α : Type u_1
β : Type u_2
γ : Type ?u.416783
ι : Type ?u.416786
κ : Type ?u.416789
inst✝ : DecidableEq α
s : Finset β
f : β → α
⊢ (sup s fun b => {f b}) = image f s
ext a
case a
F : Type ?u.416774
α : Type u_1
β : Type u_2
γ : Type ?u.416783
ι : Type ?u.416786
κ : Type ?u.416789
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ v, v ∈ s ∧ a ∈ {f v}) ↔ ∃ a_1, a_1 ∈ s ∧ f a_1 = a
case a
F : Type ?u.416774
α : Type u_1
β : Type u_2
γ : Type ?u.416783
ι : Type ?u.416786
κ : Type ?u.416789
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ sup s fun b => {f b}) ↔ a ∈ image f s
rw [mem_sup, mem_image]
no goals
case a
F : Type ?u.416774
α : Type u_1
β : Type u_2
γ : Type ?u.416783
ι : Type ?u.416786
κ : Type ?u.416789
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ v, v ∈ s ∧ a ∈ {f v}) ↔ ∃ a_1, a_1 ∈ s ∧ f a_1 = a
simp only [mem_singleton, eq_comm]