[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h₁ : NeBot f
h₂ : ∀ (g : Filter α), NeBot g → g ≤ f → f ≤ g
g : Filter α
neBot'✝ : NeBot g
le_of_le✝ : ∀ (g_1 : Filter α), NeBot g_1 → g_1 ≤ g → g ≤ g_1
x✝ : ↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ } = ↑{ toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ } = { toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
g : Filter α
hg : NeBot (g ⊓ ↑f)
⊢ NeBot (↑f ⊓ g)
[PROOFSTEP]
rwa [inf_comm]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬↑f ≤ g
[PROOFSTEP]
rw [← inf_neBot_iff, neBot_iff, Ne.def, not_not, disjoint_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
hsc : ¬sᶜ ∈ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 sᶜᶜ = ⊥
[PROOFSTEP]
rwa [compl_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
⊢ sᶜ ∈ f ↔ ¬s ∈ f
[PROOFSTEP]
rw [← compl_not_mem_iff, compl_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h : ∀ (s : Set α), ¬sᶜ ∈ f ↔ s ∈ f
hf : f = ⊥
⊢ False
[PROOFSTEP]
simp [hf] at h 
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
u : Ultrafilter α
f g : Filter α
⊢ ¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)
[PROOFSTEP]
simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
⊢ s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f
[PROOFSTEP]
simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
⊢ (∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x
[PROOFSTEP]
simp only [imp_iff_not_or, eventually_or, eventually_not]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
s : Set (Set α)
hs : Set.Finite s
⊢ ⋃₀ ∅ ∈ f ↔ ∃ t, t ∈ ∅ ∧ t ∈ f
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝¹ t : Set α
p q : α → Prop
s : Set (Set α)
hs : Set.Finite s
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
his : ⋃₀ s✝ ∈ f ↔ ∃ t, t ∈ s✝ ∧ t ∈ f
⊢ ⋃₀ insert a✝ s✝ ∈ f ↔ ∃ t, t ∈ insert a✝ s✝ ∧ t ∈ f
[PROOFSTEP]
simp [union_mem_iff, his, or_and_right, exists_or]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
is : Set β
s : β → Set α
his : Set.Finite is
⊢ ⋃ (i : β) (_ : i ∈ is), s i ∈ f ↔ ∃ i, i ∈ is ∧ s i ∈ f
[PROOFSTEP]
simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), bex_image_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
u : Ultrafilter β
inj : Injective m
large : range m ∈ u
g : Filter α
hg : NeBot g
hgu : g ≤ Filter.comap m ↑u
⊢ Filter.comap m ↑u ≤ g
[PROOFSTEP]
simp only [← u.unique (map_le_iff_le_comap.2 hgu), comap_map inj, le_rfl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) (_ : Injective id)
⊢ range id ∈ f
[PROOFSTEP]
rw [range_id]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) (_ : Injective id)
⊢ univ ∈ f
[PROOFSTEP]
exact univ_mem
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ comap f inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) (_ : Injective (n ∘ m))
⊢ range (n ∘ m) ∈ f
[PROOFSTEP]
rw [range_comp]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ comap f inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) (_ : Injective (n ∘ m))
⊢ n '' range m ∈ f
[PROOFSTEP]
exact image_mem_of_mem_comap large₀ large₁
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
α✝ : Type ?u.19487
a : α✝
s : Set α✝
⊢ ¬sᶜ ∈ pure a ↔ s ∈ pure a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = ↑(pure a)
[PROOFSTEP]
rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : s ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
[PROOFSTEP]
rw [← biUnion_of_singleton s] at h' 
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : ⋃ (x : α) (_ : x ∈ s), {x} ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
[PROOFSTEP]
rcases(Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : ⋃ (x : α) (_ : x ∈ s), {x} ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
[PROOFSTEP]
exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
f : Ultrafilter α
m : α → Ultrafilter β
s : Set β
⊢ (¬sᶜ ∈ Filter.bind ↑f fun x => ↑(m x)) ↔ s ∈ Filter.bind ↑f fun x => ↑(m x)
[PROOFSTEP]
simp only [mem_bind', mem_coe, ← compl_mem_iff_not_mem, compl_setOf, compl_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
[PROOFSTEP]
refine' ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => _⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
⊢ False
[PROOFSTEP]
set g : Filter (sᶜ : Set α) := comap (↑) f
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ False
[PROOFSTEP]
haveI : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_setOf])
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ ¬(range Subtype.val)ᶜ ∈ f
[PROOFSTEP]
simpa [compl_setOf]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑sᶜ := comap Subtype.val f
this : NeBot g
⊢ False
[PROOFSTEP]
simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : Filter α
s : Set α
a : α
f f' : Filter α
⊢ ⨆ (g : Ultrafilter α) (_ : ↑g ≤ f), ↑g ≤ f' ↔ f ≤ f'
[PROOFSTEP]
simp only [iSup_le_iff, ← le_iff_ultrafilter]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : Filter α
s : Set α
a : α
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂
[PROOFSTEP]
simpa only [tendsto_iff_comap] using le_iff_ultrafilter
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Filter α), NeBot f → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
[PROOFSTEP]
refine' ⟨fun H f hf => H f f.neBot hf, _⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f) → ∀ (f : Filter α), NeBot f → f ≤ g → p f
[PROOFSTEP]
intro H f hf hfg
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : NeBot f
hfg : f ≤ g
⊢ p f
[PROOFSTEP]
exact hp (of_le f) (H _ ((of_le f).trans hfg))
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
let f := Filter.comap m g ⊓ 𝓟 s
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
have : s ∈ f := mem_inf_of_right (mem_principal_self s)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this✝ : NeBot f
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
exact le_def.mp (of_le _) s this
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g
[PROOFSTEP]
let f := Filter.comap m g ⊓ 𝓟 s
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal h) = g
[PROOFSTEP]
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ map m (ofComapInfPrincipal h) = g
[PROOFSTEP]
apply eq_of_le
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g
[PROOFSTEP]
calc
  Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
  _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
  _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
  _ ≤ ↑g ⊓ (𝓟 <| m '' s) := (inf_le_inf_right _ map_comap_le)
  _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ Filter.map m (Filter.comap m ↑g) ⊓ Filter.map m (𝓟 s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)
[PROOFSTEP]
rw [map_principal]
