constructor
case h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h✝ : y ∈ (Set.map f s).insertIf (f a) p
h : y = f a
hp : p
⊢ y ∈ (Set.map (fun f => f a) f✝).inter (Set.const p)
case h.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h✝ : y ∈ (Set.map f s).insertIf (f a) p
h : y = f a
hp : p
⊢ y ∈ Set.map (fun f => f a) f✝

case h.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h✝ : y ∈ (Set.map f s).insertIf (f a) p
h : y = f a
hp : p
⊢ y ∈ Set.const p