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

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

State before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
⊢ ∀ (x : β), (x ∈ s.bind fun x => Set.pure (f x)) ↔ x ∈ Set.map f s
Tactic:
intro y
State after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) ↔ y ∈ Set.map f s

State before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) ↔ y ∈ Set.map f s
Tactic:
constructor
State after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) → y ∈ Set.map f s

case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ y ∈ Set.map f s → y ∈ s.bind fun x => Set.pure (f x)

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) → y ∈ Set.map f s
Tactic:
intro ⟨x, hx, (h : y = f x)⟩
State after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : y = f x
⊢ y ∈ Set.map f s

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : y = f x
⊢ y ∈ Set.map f s
Tactic:
refine ⟨x, hx, h.symm⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ y ∈ Set.map f s → y ∈ s.bind fun x => Set.pure (f x)
Tactic:
intro ⟨x, hx, h⟩
State after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ s.bind fun x => Set.pure (f x)

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ s.bind fun x => Set.pure (f x)
Tactic:
refine ⟨x, hx, h.symm⟩
State after:
no goals