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

State before:
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
⊢ (Set.pureIf a p).bind f = (f a).inter (Set.const p)
Tactic:
apply Set.ext
State after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
⊢ ∀ (x : β), x ∈ (Set.pureIf a p).bind f ↔ x ∈ (f a).inter (Set.const p)

State before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
⊢ ∀ (x : β), x ∈ (Set.pureIf a p).bind f ↔ x ∈ (f a).inter (Set.const p)
Tactic:
intro y
State after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f ↔ y ∈ (f a).inter (Set.const p)

State before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f ↔ y ∈ (f a).inter (Set.const p)
Tactic:
constructor
State after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f → y ∈ (f a).inter (Set.const p)

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (f a).inter (Set.const p) → y ∈ (Set.pureIf a p).bind f

State before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f → y ∈ (f a).inter (Set.const p)
Tactic:
intro ⟨_, ⟨rfl, hp⟩, h⟩
State after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
hp : p
h : y ∈ f a
⊢ y ∈ (f a).inter (Set.const p)

State before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
hp : p
h : y ∈ f a
⊢ y ∈ (f a).inter (Set.const p)
Tactic:
refine ⟨h, hp⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (f a).inter (Set.const p) → y ∈ (Set.pureIf a p).bind f
Tactic:
intro ⟨h, hp⟩
State after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
h : y ∈ f a
hp : y ∈ Set.const p
⊢ y ∈ (Set.pureIf a p).bind f

State before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
h : y ∈ f a
hp : y ∈ Set.const p
⊢ y ∈ (Set.pureIf a p).bind f
Tactic:
refine ⟨a, ⟨rfl, hp⟩, h⟩
State after:
no goals