α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ bind q f ↔ ∃ a _h, b ∈ f a
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ bind q f ↔ ∃ a, a ∈ q ∧ b ∈ f a
simp_rw [← exists_prop]
no goals
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ bind q f ↔ ∃ a _h, b ∈ f a
exact Set.mem_iUnion₂