case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun g => g a) '' s ∈ seq f (pure a)

case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ Set.seq s t ∈ map (fun g => g a) f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
⊢ seq f (pure a) = map (fun g => g a) f
refine' le_antisymm (le_map fun s hs => _) (le_seq fun s hs t ht => _)
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ Set.seq s {a} ∈ seq f (pure a)
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun g => g a) '' s ∈ seq f (pure a)
rw [← seq_singleton]
no goals
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ Set.seq s {a} ∈ seq f (pure a)
exact seq_mem_seq hs singleton_mem_pure
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ (fun g => g a) '' s ⊆ Set.seq s t
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ Set.seq s t ∈ map (fun g => g a) f
refine' sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) _
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
g : α → β
hg : g ∈ s
⊢ (fun g => g a) g ∈ Set.seq s t
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ (fun g => g a) '' s ⊆ Set.seq s t
rintro b ⟨g, hg, rfl⟩
no goals
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294266
ι : Sort x
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
g : α → β
hg : g ∈ s
⊢ (fun g => g a) g ∈ Set.seq s t
exact ⟨g, hg, a, ht, rfl⟩