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

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

State before:
α : Type u_1
s t✝ u : Set α
β : Type u_1
t : Set β
f : α → Set β
h : ∀ (x : α), x ∈ s → (f x).Subset t
y : β
x : α
hxs : x ∈ s
hfxy : y ∈ f x
⊢ y ∈ t
Tactic:
exact h x hxs y hfxy
State after:
no goals