α : Type u_1
β : Type u_2
f : α → List β
b : β
l : List α
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a
α : Type u_1
β : Type u_2
f : α → List β
b : β
l : List α
⊢ b ∈ List.bind l f ↔ ∃ a, a ∈ l ∧ b ∈ f a
simp [List.bind, mem_join]
no goals
α : Type u_1
β : Type u_2
f : α → List β
b : β
l : List α
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a
exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩