awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
h :
  ∀ (n : ℕ),
    LT.lt (α := ℕ) (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)
      (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)
⊢ StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v

Tactic:
apply strictMono_nat_of_lt_succ

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ LT.lt (α := ℕ) (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)
    (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)

Tactic:
apply hu
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
h : P 0 (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) 0 (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
h₁ : ∀ (n : ℕ), P (n + 1) (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
⊢ P n (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)

Tactic:
cases n
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ P 0 (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) 0 (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)

Tactic:
simp [hu']
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ P (n + 1) (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)

Tactic:
simp [hu']
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

Tactic:
extraction_forall_of_frequently fun n => (h n).frequently

Premises used: Filter.extraction_forall_of_frequently, Filter.Eventually.frequently
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, P n k
⊢ ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k

Tactic:
simp [eventually_atTop, h]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
F : Filter β
u : α → β
inst_2 : Nonempty α
simp_rw :
  (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b ≥ a, p (u b)) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
⊢ (F ⊓ map u atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U

Tactic:
simp_rw [inf_neBot_iff_frequently_left, frequently_map, frequently_atTop]

Premises used: Filter.frequently_atTop, Filter.frequently_map, Filter.inf_neBot_iff_frequently_left
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
F : Filter β
u : α → β
inst_2 : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b ≥ a, p (u b)) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U

Tactic:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this : Nonempty α
⊢ ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x

Tactic:
have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x :=
    (eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this_1 : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a' ≥ a, b ≤ u a'

Tactic:
this.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this_1 : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a' ≥ a, b ≤ u a'

Tactic:
exact this.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
h : Tendsto u atTop atBot
⊢ ∀ (a : α) (b : β), ∃ a' ≥ a, u a' ≤ b

Tactic:
exists_le_of_tendsto_atTop (β := βᵒᵈ) h

Premises used: Filter.exists_le_of_tendsto_atTop, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
inst_3 : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b : β
obtain : ∀ (b' : β) (hb' : b < b'), ∃ a' ≥ a, b < u a'
⊢ ∃ a' ≥ a, b < u a'

Tactic:
obtain ⟨b', hb'⟩ := exists_gt b

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
inst_3 : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
rcases : ∀ (a' : α) (ha' : a' ≥ a) (ha'' : b' ≤ u a'), ∃ a' ≥ a, b < u a'
⊢ ∃ a' ≥ a, b < u a'

Tactic:
rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩

Premises used: Filter.exists_le_of_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
inst_3 : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a' ≥ a
ha'' : b' ≤ u a'
⊢ ∃ a' ≥ a, b < u a'

Tactic:
⟨a', ha', lt_of_lt_of_le hb' ha''⟩

Premises used: And.intro, Exists.intro, lt_of_lt_of_le
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
inst_3 : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a' ≥ a
ha'' : b' ≤ u a'
⊢ ∃ a' ≥ a, b < u a'

Tactic:
exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
inst_3 : NoMinOrder β
h : Tendsto u atTop atBot
⊢ ∀ (a : α) (b : β), ∃ a' ≥ a, u a' < b

Tactic:
exists_lt_of_tendsto_atTop (β := βᵒᵈ) h

Premises used: Filter.exists_lt_of_tendsto_atTop, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
F : Filter β
u : α → β
⊢ (F ⊓ map u atBot).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≤ N, u n ∈ U

Tactic:
inf_map_atTop_neBot_iff (α := αᵒᵈ)

Premises used: Set.Mem, setOf, Filter.inf_map_atTop_neBot_iff, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
f : α → β
l : Filter β
⊢ Tendsto f atTop l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≥ a, f b ∈ s

Tactic:
simp only [tendsto_def, mem_atTop_sets, mem_preimage]

Premises used: Filter.tendsto_def, Filter.mem_atTop_sets, Set.mem_preimage
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
f : α → β
s : Set β
simp_rw : atTop ≤ comap f (𝓟 s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
simp_rw₁ : atTop ≤ 𝓟 (f ⁻¹' s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
simp_rw₂ : Membership.mem (γ := Filter α) atTop (f ⁻¹' s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
simp_rw₃ : (∃ (a : α), ∀ b ≥ a, b ∈ f ⁻¹' s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s

Tactic:
simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]

Premises used: Filter.le_principal_iff, Filter.mem_atTop_sets, Filter.tendsto_iff_comap, Filter.comap_principal, Set.mem_preimage
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
f : α → β
inst_3 : Preorder β
⊢ Tendsto f atTop atTop ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → b ≤ f a

Tactic:
tendsto_iInf.trans <| forall_congr' fun _ => tendsto_atTop_principal

Premises used: Filter.tendsto_atTop_principal, Filter.atTop, forall_congr', Iff.trans, Filter.tendsto_iInf
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
f : α → β
inst_3 : Preorder β
⊢ Tendsto f atTop atBot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → f a ≤ b

Tactic:
tendsto_atTop_atTop (β := βᵒᵈ)

Premises used: setOf, Filter.tendsto_atTop_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
f : α → β
inst_3 : Preorder β
hf : Monotone f
⊢ Tendsto f atTop atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a

Tactic:
tendsto_atTop_atTop.trans <| forall_congr' fun _ => exists_congr fun a =>
    ⟨fun h => h a (le_refl a), fun h _a' ha' => le_trans h <| hf ha'⟩

Premises used: le_refl, Filter.tendsto_atTop_atTop, exists_congr, Iff.intro, forall_congr', Iff.trans, le_trans
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
f : α → β
inst_3 : Preorder β
hf : Antitone f
⊢ Tendsto f atTop atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b

Tactic:
tendsto_atTop_atTop_iff_of_monotone (β := βᵒᵈ) hf

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.tendsto_atTop_atTop_iff_of_monotone
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
f : α → β
l : Filter β
⊢ Tendsto f atBot l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≤ a, f b ∈ s

Tactic:
tendsto_atTop' (α := αᵒᵈ)

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.tendsto_atTop'
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
f : α → β
s : Set β
⊢ Tendsto f atBot (𝓟 s) ↔ ∃ (N : α), ∀ n ≤ N, f n ∈ s

Tactic:
tendsto_atTop_principal (α := αᵒᵈ) (β := βᵒᵈ)

Premises used: Filter.tendsto_atTop_principal, Set.Mem, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
f : α → β
inst_3 : Preorder β
⊢ Tendsto f atBot atTop ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, b ≤ f a

Tactic:
tendsto_atTop_atTop (α := αᵒᵈ)

Premises used: setOf, Filter.tendsto_atTop_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
f : α → β
inst_3 : Preorder β
⊢ Tendsto f atBot atBot ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, f a ≤ b

Tactic:
tendsto_atTop_atTop (α := αᵒᵈ) (β := βᵒᵈ)

Premises used: setOf, Filter.tendsto_atTop_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
f : α → β
inst_3 : Preorder β
hf : Monotone f
⊢ Tendsto f atBot atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b

Tactic:
tendsto_atBot_atBot.trans <| forall_congr' fun _ => exists_congr fun a =>
    ⟨fun h => h a (le_refl a), fun h _a' ha' => le_trans (hf ha') h⟩

Premises used: le_refl, exists_congr, Iff.intro, forall_congr', Iff.trans, le_trans, Filter.tendsto_atBot_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
f : α → β
inst_3 : Preorder β
hf : Antitone f
⊢ Tendsto f atBot atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a

Tactic:
tendsto_atBot_atBot_iff_of_monotone (β := βᵒᵈ) hf

Premises used: Set.Ici, Filter.tendsto_atBot_atBot_iff_of_monotone, setOf, Filter.atTop, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
F : Filter α
V : ℕ → Set α
h : ∀ (n : ℕ), V n ∈ F
u : ℕ → α
hu : Tendsto u atTop F
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), u (φ n) ∈ V n

Tactic:
extraction_forall_of_eventually'
    (fun n => tendsto_atTop'.mp hu _ (h n) : ∀ n, ∃ N, ∀ k ≥ N, u k ∈ V n)

Premises used: Filter.extraction_forall_of_eventually', Iff.mp, Filter.tendsto_atTop'
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
hgi : ∀ c ≥ b, ∃ (x : α), f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x
⊢ Nonempty α

Tactic:
have : Nonempty α := (hgi b le_rfl).nonempty
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
hgi : ∀ c ≥ b, ∃ (x : α), f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x
this : Nonempty α
choose! :
  ∀ (g : (c : β) → α) (hfg : ∀ c ≥ b, f (g c) = c) (hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c), map f atTop = atTop
⊢ map f atTop = atTop

Tactic:
choose! g hfg hgle using hgi
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ map f atTop = atTop

Tactic:
le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_

Premises used: le_antisymm, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
refine_1 : ∀ (c : β), ∃ (a : α), c ≤ f a
refine_2 : atTop ≤ map f atTop
⊢ map f atTop = atTop

Tactic:
refine le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_

Premises used: le_antisymm, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
c : β
refine_1 : ∀ (d : β) (hcd : c ≤ d) (hbd : b ≤ d), ∃ (a : α), c ≤ f a
⊢ ∃ (a : α), c ≤ f a

Tactic:
rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩

Premises used: exists_ge_ge
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
c d : β
hcd : c ≤ d
hbd : b ≤ d
⊢ ∃ (a : α), c ≤ f a

Tactic:
⟨g d, hcd.trans (hfg d hbd).ge⟩

Premises used: Eq.ge, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
c d : β
hcd : c ≤ d
hbd : b ≤ d
⊢ ∃ (a : α), c ≤ f a

Tactic:
exact ⟨g d, hcd.trans (hfg d hbd).ge⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨g b⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this_1 : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
refine_2 : ∀ (i' : α), True → Membership.mem (γ := Filter β) atTop (f '' Ici i')
⊢ atTop ≤ map f atTop

Tactic:
rw [(atTop_basis.map f).ge_iff]

Premises used: Filter.atTop_basis, Filter.HasBasis.map, Filter.HasBasis.ge_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this_1 : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
refine_2 : True → Membership.mem (γ := Filter β) atTop (f '' Ici a)
⊢ True → Membership.mem (γ := Filter β) atTop (f '' Ici a)

Tactic:
_
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this_1 : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
h_1 : True
h : ∀ (c : β) (hac : f a ≤ c) (hbc : b ≤ c), c ∈ f '' Ici a
⊢ Membership.mem (γ := Filter β) atTop (f '' Ici a)

Tactic:
filter_upwards [eventually_ge_atTop (f a), eventually_ge_atTop b] with c hac hbc

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this_1 : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
h : True
c : β
hac : f a ≤ c
hbc : b ≤ c
⊢ c ∈ f '' Ici a

Tactic:
⟨g c, (hgle _ hbc _).1 hac, hfg _ hbc⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Iff.mp, Set.image
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this_1 : Nonempty α
g : (c : β) → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
h : True
c : β
hac : f a ≤ c
hbc : b ≤ c
⊢ c ∈ f '' Ici a

Tactic:
exact ⟨g c, (hgle _ hbc _).1 hac, hfg _ hbc⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : PartialOrder β
inst_3 : IsDirectedOrder β
f : α → β
g : β → α
b : β
hf : Monotone f
gc : ∀ (a : α), ∀ c ≥ b, f a ≤ c ↔ a ≤ g c
hgi : ∀ c ≥ b, c ≤ f (g c)
⊢ map f atTop = atTop

Tactic:
map_atTop_eq_of_gc_preorder hf b fun c hc ↦
    ⟨g c, le_antisymm ((gc _ _ hc).2 le_rfl) (hgi c hc), (gc · c hc)⟩

Premises used: Iff.mpr, le_rfl, le_antisymm, And.intro, Exists.intro, Filter.map_atTop_eq_of_gc_preorder
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Preorder β
inst_3 : IsCodirectedOrder β
f : α → β
hf : Monotone f
b : β
hgi : ∀ c ≤ b, ∃ (x : α), f x = c ∧ ∀ (a : α), c ≤ f a ↔ x ≤ a
⊢ map f atBot = atBot

Tactic:
map_atTop_eq_of_gc_preorder (α := αᵒᵈ) (β := βᵒᵈ) hf.dual _ hgi

Premises used: setOf, Monotone.dual, Filter.atBot, Filter.map_atTop_eq_of_gc_preorder, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : PartialOrder β
inst_3 : IsCodirectedOrder β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α), ∀ b ≤ b', b ≤ f a ↔ g b ≤ a
hgi : ∀ b ≤ b', f (g b) ≤ b
⊢ map f atBot = atBot

Tactic:
map_atTop_eq_of_gc (α := αᵒᵈ) (β := βᵒᵈ) _ _ hf.dual gc hgi

Premises used: setOf, Monotone.dual, Filter.atBot, Set.Iic, OrderDual, Filter.map_atTop_eq_of_gc
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
choose :
  ∀ (f : (a b : α) → α) (hl : ∀ (a b : α), a ≤ f a b) (hr : ∀ (a b : α), b ≤ f a b),
    Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop) atTop
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop) atTop

Tactic:
choose f hl hr using exists_ge_ge (α := α)

Premises used: exists_ge_ge
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
have : DirectedOn (· ≤ ·) s := fun x _ y _ ↦
    ⟨f a (f x y), h <| hl _ _, (hl x y).trans (hr _ _), (hr x y).trans (hr _ _)⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Directed (ι := { x : α // x ∈ s }) (fun (x1 x2 : α) ↦ x1 ≤ x2) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
rw [directedOn_iff_directed] at this

Premises used: directedOn_iff_directed
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (ι := { x : α // x ∈ s }) (fun (x1 x2 : α) ↦ x1 ≤ x2) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
rwa : IsDirected.{u_3 + 1} (↑s : Type u_3) fun (x1 x2 : (↑s : Type u_3)) ↦ x1 ≤ x2
rwa₁ rwa₂ rwa₃ rwa₄ : Directed (fun (x1 x2 : (↑s : Type u_3)) ↦ x1 ≤ x2) id
⊢ IsDirectedOrder.{u_3} (↑s : Type u_3)

Tactic:
rwa [IsDirectedOrder, ← directed_id_iff]

Premises used: directed_id_iff, IsDirectedOrder
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsDirectedOrder.{u_3} (↑s : Type u_3)

Tactic:
have : IsDirectedOrder s := by
    rw [directedOn_iff_directed] at this
    rwa [IsDirectedOrder, ← directed_id_iff]
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
this : IsDirectedOrder.{u_3} (↑s : Type u_3)
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop) atTop

Tactic:
map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_

Premises used: Subtype.mono_coe, Filter.map_atTop_eq_of_gc_preorder
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
this : IsDirectedOrder.{u_3} (↑s : Type u_3)
refine :
  ∀ (c : α) (hc : c ≥ a), ∃ (x : { x : α // x ∈ s }), (↑x : α) = c ∧ ∀ (a : { x : α // x ∈ s }), (↑a : α) ≤ c ↔ a ≤ x
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop) atTop

Tactic:
refine map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_

Premises used: Subtype.mono_coe, Filter.map_atTop_eq_of_gc_preorder