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

case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ Set.seq s t ∈ map g f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
⊢ seq (pure g) f = map g 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.293780
ι : Sort x
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ Set.seq {g} s ∈ seq (pure g) f
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ g '' s ∈ seq (pure g) f
rw [← singleton_seq]
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g} ∈ pure g
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ Set.seq {g} s ∈ seq (pure g) f
apply seq_mem_seq _ hs
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g} ∈ pure g
exact singleton_mem_pure
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ g '' t ⊆ Set.seq s t
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ Set.seq s t ∈ map g f
refine' sets_of_superset (map g f) (image_mem_map ht) _
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ Set.seq s t
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ g '' t ⊆ Set.seq s t
rintro b ⟨a, ha, rfl⟩
no goals
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.293780
ι : Sort x
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ Set.seq s t
exact ⟨g, hs, a, ha, rfl⟩