case inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.268461
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
hα : IsEmpty α
⊢ NeBot (comap Prod.snd f) ↔ Nonempty α ∧ NeBot f

case inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.268461
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
hα : Nonempty α
⊢ NeBot (comap Prod.snd f) ↔ Nonempty α ∧ NeBot f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.268461
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
⊢ NeBot (comap Prod.snd f) ↔ Nonempty α ∧ NeBot f
cases' isEmpty_or_nonempty α with hα hα
case inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.268461
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
hα : IsEmpty α
⊢ ¬NeBot ⊥ ↔ ¬(Nonempty α ∧ NeBot f)
case inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.268461
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
hα : IsEmpty α
⊢ NeBot (comap Prod.snd f) ↔ Nonempty α ∧ NeBot f
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
no goals
case inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.268461
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
hα : IsEmpty α
⊢ ¬NeBot ⊥ ↔ ¬(Nonempty α ∧ NeBot f)
simp
no goals
case inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.268461
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
hα : Nonempty α
⊢ NeBot (comap Prod.snd f) ↔ Nonempty α ∧ NeBot f
simp [comap_neBot_iff_frequently, hα]