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

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