-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem HasAntitoneBasis.subbasis_with_rel {f : Filter α} {s : ℕ → Set α}
    (hs : f.HasAntitoneBasis s) {r : ℕ → ℕ → Prop} (hr : ∀ m, ∀ᶠ n in atTop, r m n) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ (∀ ⦃m n⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Proof state:
case intro
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ 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)

Tactic:
simp only [forall_mem_image, forall_and, mem_Iio] at hφ

Result:
case intro
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ 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)

Proof state:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
rcases seq_of_forall_finite_exists fun t ht => (this t ht).exists with ⟨φ, hφ⟩

Result:
case intro
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ 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)

Proof state:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
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 _)

Result:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Proof state:
case intro
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ 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)

Tactic:
exact ⟨φ, forall_swap.2 hφ.1, forall_swap.2 hφ.2⟩

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
rsuffices ⟨φ, hφ, hrφ⟩ : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ m n, m < n → r (φ m) (φ n)

Result:
case intro.intro
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis 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)) ∧ f.HasAntitoneBasis (s ∘ φ)

α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Proof state:
case intro.intro
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis 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)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩

Result:
no goals