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

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

State before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ y ∈ t >>= f
Tactic:
exists x
State after:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t ∧ y ∈ f x

State before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t ∧ y ∈ f x
Tactic:
constructor
State after:
case left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t

case right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ y ∈ f x

State before:
case left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t
Tactic:
exact hst x hx
State after:
no goals

State before:
case right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ y ∈ f x
Tactic:
exact h
State after:
no goals