Theorem: Set.val_subset_bind (GMLInit/Data/Set/Subset.lean)

State before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
⊢ x ∈ s → (f x).Subset (s >>= f)
Tactic:
intro hxs y hfxy
State after:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
hxs : x ∈ s
y : β
hfxy : y ∈ f x
⊢ y ∈ s >>= f

State before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
hxs : x ∈ s
y : β
hfxy : y ∈ f x
⊢ y ∈ s >>= f
Tactic:
exists x
State after:
no goals