case inl
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ NeBot (comap (eval i) f) ↔ (∀ (j : ι), Nonempty (α j)) ∧ NeBot f

case inr
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ NeBot (comap (eval i) f) ↔ (∀ (j : ι), Nonempty (α j)) ∧ NeBot f
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
⊢ NeBot (comap (eval i) f) ↔ (∀ (j : ι), Nonempty (α j)) ∧ NeBot f
cases' isEmpty_or_nonempty (∀ j, α j) with H H
case inl
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ¬NeBot ⊥ ↔ ¬((∀ (j : ι), Nonempty (α j)) ∧ NeBot f)
case inl
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ NeBot (comap (eval i) f) ↔ (∀ (j : ι), Nonempty (α j)) ∧ 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.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ¬NeBot ⊥ ↔ ¬((∀ (j : ι), Nonempty (α j)) ∧ NeBot f)
simp [← Classical.nonempty_pi]
case inr
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
this : ∀ (j : ι), Nonempty (α j)
⊢ NeBot (comap (eval i) f) ↔ (∀ (j : ι), Nonempty (α j)) ∧ NeBot f
case inr
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ NeBot (comap (eval i) f) ↔ (∀ (j : ι), Nonempty (α j)) ∧ NeBot f
have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H
no goals
case inr
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.269920
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
this : ∀ (j : ι), Nonempty (α j)
⊢ NeBot (comap (eval i) f) ↔ (∀ (j : ι), Nonempty (α j)) ∧ NeBot f
simp [comap_neBot_iff_frequently, *]