ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)

case this
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)
suffices : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ m n, m < n → r (φ m) (φ n)
case this
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
case this
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
have : ∀ t : Set ℕ, t.Finite → ∀ᶠ n in atTop, ∀ m ∈ t, m < n ∧ r m n := fun t ht =>
  (eventually_all_finite ht).2 fun m _ => (eventually_gt_atTop m).and (hr _)
case this.intro
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
φ : ℕ → ℕ
hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
case this
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
rcases seq_of_forall_finite_exists fun t ht => (this t ht).exists with ⟨φ, hφ⟩
case this.intro
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
φ : ℕ → ℕ
hφ : (∀ (x x_1 : ℕ), x_1 < x → φ x_1 < φ x) ∧ ∀ (x x_1 : ℕ), x_1 < x → r (φ x_1) (φ x)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
case this.intro
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
φ : ℕ → ℕ
hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
simp only [ball_image_iff, forall_and, mem_Iio] at hφ
no goals
case this.intro
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
φ : ℕ → ℕ
hφ : (∀ (x x_1 : ℕ), x_1 < x → φ x_1 < φ x) ∧ ∀ (x x_1 : ℕ), x_1 < x → r (φ x_1) (φ x)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
exact ⟨φ, forall_swap.2 hφ.1, forall_swap.2 hφ.2⟩
case intro.intro
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
φ : ℕ → ℕ
hφ : StrictMono φ
hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)
rcases this with ⟨φ, hφ, hrφ⟩
no goals
case intro.intro
ι : Type ?u.362344
ι' : Type ?u.362347
α : Type u_1
β : Type ?u.362353
γ : Type ?u.362356
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
φ : ℕ → ℕ
hφ : StrictMono φ
hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)
exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩