α : Type u
β : Type v
γ : Type w
δ : Type ?u.276092
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t : Set β
f : Filter β
m : α → β
hf : NeBot f
s : Set α
hs : m '' s ∈ f
⊢ ¬sᶜ ∈ comap m f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.276092
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t : Set β
f : Filter β
m : α → β
hf : NeBot f
s : Set α
hs : m '' s ∈ f
⊢ NeBot (comap m f ⊓ 𝓟 s)
refine' ⟨compl_compl s ▸ mt mem_of_eq_bot _⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.276092
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
f : Filter β
m : α → β
hf : NeBot f
s : Set α
hs : m '' s ∈ f
t : Set β
ht : t ∈ f
hts : m ⁻¹' t ⊆ sᶜ
⊢ False
α : Type u
β : Type v
γ : Type w
δ : Type ?u.276092
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t : Set β
f : Filter β
m : α → β
hf : NeBot f
s : Set α
hs : m '' s ∈ f
⊢ ¬sᶜ ∈ comap m f
rintro ⟨t, ht, hts⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.276092
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
f : Filter β
m : α → β
hf : NeBot f
s : Set α
hs : m '' s ∈ f
t : Set β
ht : t ∈ f
hts : m ⁻¹' t ⊆ sᶜ
x : α
hxs : x ∈ s
hxt : m x ∈ t
⊢ False
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.276092
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
f : Filter β
m : α → β
hf : NeBot f
s : Set α
hs : m '' s ∈ f
t : Set β
ht : t ∈ f
hts : m ⁻¹' t ⊆ sᶜ
⊢ False
rcases hf.nonempty_of_mem (inter_mem hs ht) with ⟨_, ⟨x, hxs, rfl⟩, hxt⟩
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.276092
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
f : Filter β
m : α → β
hf : NeBot f
s : Set α
hs : m '' s ∈ f
t : Set β
ht : t ∈ f
hts : m ⁻¹' t ⊆ sᶜ
x : α
hxs : x ∈ s
hxt : m x ∈ t
⊢ False
exact absurd hxs (hts hxt)