exists a
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ y ∈ (fun f => Set.map f (s.insertIf a p)) f
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a ∈ s.insertIf a p ∧ f a = y