case a
α : Type u
β : Type v
γ : Type w
δ : Type ?u.244483
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s✝ : Set α
t : Set β
inst✝ : NeBot f
c : β
s : Set β
⊢ s ∈ map (fun x => c) f ↔ s ∈ pure c
α : Type u
β : Type v
γ : Type w
δ : Type ?u.244483
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
inst✝ : NeBot f
c : β
⊢ map (fun x => c) f = pure c
ext s
no goals
case a
α : Type u
β : Type v
γ : Type w
δ : Type ?u.244483
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s✝ : Set α
t : Set β
inst✝ : NeBot f
c : β
s : Set β
⊢ s ∈ map (fun x => c) f ↔ s ∈ pure c
by_cases h : c ∈ s <;> simp [h]