F : Type ?u.415321
α✝ : Type ?u.415324
β✝ : Type ?u.415327
γ : Type ?u.415330
ι : Type ?u.415333
κ : Type ?u.415336
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ ∃ v, v ∈ s ∧ x ∈ (f v).val
F : Type ?u.415321
α✝ : Type ?u.415324
β✝ : Type ?u.415327
γ : Type ?u.415330
ι : Type ?u.415333
κ : Type ?u.415336
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
change _ ↔ ∃ v ∈ s, x ∈ (f v).val
F : Type ?u.415321
α✝ : Type ?u.415324
β✝ : Type ?u.415327
γ : Type ?u.415330
ι : Type ?u.415333
κ : Type ?u.415336
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ x ∈ sup s fun x => Multiset.toFinset (f x).val
F : Type ?u.415321
α✝ : Type ?u.415324
β✝ : Type ?u.415327
γ : Type ?u.415330
ι : Type ?u.415333
κ : Type ?u.415336
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ ∃ v, v ∈ s ∧ x ∈ (f v).val
rw [← Multiset.mem_sup, ← Multiset.mem_toFinset, sup_toFinset]
no goals
F : Type ?u.415321
α✝ : Type ?u.415324
β✝ : Type ?u.415327
γ : Type ?u.415330
ι : Type ?u.415333
κ : Type ?u.415336
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ x ∈ sup s fun x => Multiset.toFinset (f x).val
simp_rw [val_toFinset]