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

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

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

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

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

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

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

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

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