Theorem: Set.bind_assoc (GMLInit/Data/Set/Basic.lean)

State before:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
⊢ (s.bind f).bind g = s.bind fun x => (f x).bind g
Tactic:
apply Set.ext
State after:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
⊢ ∀ (x : γ), x ∈ (s.bind f).bind g ↔ x ∈ s.bind fun x => (f x).bind g

State before:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
⊢ ∀ (x : γ), x ∈ (s.bind f).bind g ↔ x ∈ s.bind fun x => (f x).bind g
Tactic:
intro z
State after:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g ↔ z ∈ s.bind fun x => (f x).bind g

State before:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g ↔ z ∈ s.bind fun x => (f x).bind g
Tactic:
constructor
State after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g → z ∈ s.bind fun x => (f x).bind g

case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ (z ∈ s.bind fun x => (f x).bind g) → z ∈ (s.bind f).bind g

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g → z ∈ s.bind fun x => (f x).bind g
Tactic:
intro ⟨y, ⟨x, hx, hy⟩, hz⟩
State after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
y : β
x : α
hx : x ∈ s
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ s.bind fun x => (f x).bind g

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
y : β
x : α
hx : x ∈ s
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ s.bind fun x => (f x).bind g
Tactic:
refine ⟨x, hx, ⟨y, hy, hz⟩⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ (z ∈ s.bind fun x => (f x).bind g) → z ∈ (s.bind f).bind g
Tactic:
intro ⟨x, hx, ⟨y, hy, hz⟩⟩
State after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
x : α
hx : x ∈ s
y : β
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ (s.bind f).bind g

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
x : α
hx : x ∈ s
y : β
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ (s.bind f).bind g
Tactic:
refine ⟨y, ⟨x, hx, hy⟩, hz⟩
State after:
no goals