case refine'_1
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

case refine'_2
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_exists_freq : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ᶠ (n : ι) in l, p n
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
refine' ⟨fun h_freq => _, fun h_exists_freq => _⟩
case refine'_1
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
case refine'_1
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
have : NeBot (l ⊓ 𝓟 { x : ι | p x }) := by simpa [neBot_iff, inf_principal_eq_bot]
case refine'_1.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx : Tendsto x atTop (l ⊓ 𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
case refine'_1
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
obtain ⟨x, hx⟩ := exists_seq_tendsto (l ⊓ 𝓟 { x : ι | p x })
case refine'_1.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx : Tendsto x atTop l ∧ Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
case refine'_1.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx : Tendsto x atTop (l ⊓ 𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
rw [tendsto_inf] at hx
case refine'_1.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
case refine'_1.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx : Tendsto x atTop l ∧ Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
cases' hx with hx_l hx_p
case refine'_1.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ᶠ (n : ℕ) in atTop, p (x n)
case refine'_1.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
refine' ⟨x, hx_l, _⟩
case refine'_1.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : ∀ᶠ (a : ℕ) in atTop, x a ∈ {x | p x}
⊢ ∃ᶠ (n : ℕ) in atTop, p (x n)
case refine'_1.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ᶠ (n : ℕ) in atTop, p (x n)
rw [tendsto_principal] at hx_p
no goals
case refine'_1.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : ∀ᶠ (a : ℕ) in atTop, x a ∈ {x | p x}
⊢ ∃ᶠ (n : ℕ) in atTop, p (x n)
exact hx_p.frequently
no goals
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
⊢ NeBot (l ⊓ 𝓟 {x | p x})
simpa [neBot_iff, inf_principal_eq_bot]
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ᶠ (n : ι) in l, p n
case refine'_2
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_exists_freq : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ᶠ (n : ι) in l, p n
obtain ⟨x, hx_tendsto, hx_freq⟩ := h_exists_freq
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{x_1 | ¬p (x x_1)} ∈ atTop
⊢ ¬{x | ¬p x} ∈ l
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ᶠ (n : ι) in l, p n
simp_rw [Filter.Frequently, Filter.Eventually] at hx_freq⊢
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{x_1 | ¬p (x x_1)} ∈ atTop
this : {n | ¬p (x n)} = {n | x n ∈ {y | ¬p y}}
⊢ ¬{x | ¬p x} ∈ l
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{x_1 | ¬p (x x_1)} ∈ atTop
⊢ ¬{x | ¬p x} ∈ l
have : { n : ℕ | ¬p (x n) } = { n | x n ∈ { y | ¬p y } } := rfl
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{y | ¬p y} ∈ map (fun n => x n) atTop
this : {n | ¬p (x n)} = {n | x n ∈ {y | ¬p y}}
⊢ ¬{x | ¬p x} ∈ l
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{x_1 | ¬p (x x_1)} ∈ atTop
this : {n | ¬p (x n)} = {n | x n ∈ {y | ¬p y}}
⊢ ¬{x | ¬p x} ∈ l
rw [this, ← mem_map'] at hx_freq
no goals
case refine'_2.intro.intro
ι✝ : Type ?u.368461
ι' : Type ?u.368464
α : Type ?u.368467
β : Type ?u.368470
γ : Type ?u.368473
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{y | ¬p y} ∈ map (fun n => x n) atTop
this : {n | ¬p (x n)} = {n | x n ∈ {y | ¬p y}}
⊢ ¬{x | ¬p x} ∈ l
exact mt (@hx_tendsto _) hx_freq