awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
P : ℕ → ℕ → Prop
h : ∀ (n a : ℕ), ∃ b > a, P n b
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
have choose : ∀ (u : (n a : ℕ) → ℕ) (hu : ∀ (n a : ℕ), u n a > a) (hu' : ∀ (n a : ℕ), P n (u n a)),
  ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
Tactic: choose u hu hu' using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
have h : (StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v) ∧
  ∀ (n : ℕ), P n ((fun (n : ℕ) ↦ (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)) n)
Tactic: use (fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v : ℕ → ℕ)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ (StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v) ∧
    ∀ (n : ℕ), P n ((fun (n : ℕ) ↦ (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)) n)
have h : StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
h : StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (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) ∧
    ∀ (n : ℕ), P n ((fun (n : ℕ) ↦ (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)) n)
have h₁ : ∀ (n : ℕ), P n (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v
have 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 : ℕ)
Tactic: apply strictMono_nat_of_lt_succ
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ P n (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
have h : P 0 (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) 0 (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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)
⊢ P n (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
have h₁ : ∀ (n : ℕ), P (n + 1) (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
F : Filter β
u : α → β
inst_2 : Nonempty α
⊢ (F ⊓ map u atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
have simp_rw : (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b ≥ a, p (u b)) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
Tactic: simp_rw [inf_neBot_iff_frequently_left, frequently_map, frequently_atTop]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
u : α → β
inst_2 : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a' ≥ a, b ≤ u a'
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
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 α
⊢ ∃ a' ≥ a, b ≤ u a'
have this₁ : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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 : β
⊢ ∃ a' ≥ a, b < u a'
have obtain : ∀ (b' : β) (hb' : b < b'), ∃ a' ≥ a, b < u a'
Tactic: obtain ⟨b', hb'⟩ := exists_gt b
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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' ≥ a, b < u a'
have rcases : ∀ (a' : α) (ha' : a' ≥ a) (ha'' : b' ≤ u a'), ∃ a' ≥ a, b < u a'
Tactic: rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
f : α → β
s : Set β
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
have simp_rw : atTop ≤ comap f (𝓟 s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
Tactic: simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
have simp_rw₁ : atTop ≤ 𝓟 (f ⁻¹' s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
Tactic: simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
have simp_rw₂ : Membership.mem (γ := Filter α) atTop (f ⁻¹' s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
Tactic: simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
have simp_rw₃ : (∃ (a : α), ∀ b ≥ a, b ∈ f ⁻¹' s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
Tactic: simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
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
⊢ map f atTop = atTop
have this : Nonempty α
Tactic: have : Nonempty α := (hgi b le_rfl).nonempty
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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 α
⊢ map f atTop = atTop
have choose! : ∀ (g : (c : β) → α) (hfg : ∀ c ≥ b, f (g c) = c) (hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c), map f atTop = atTop
Tactic: choose! g hfg hgle using hgi
Cleared hypotheses: hgi
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
have refine_1 : ∀ (c : β), ∃ (a : α), c ≤ f a
Tactic: refine le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
⊢ map f atTop = atTop
have refine_2 : atTop ≤ map f atTop
Tactic: refine le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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 : β
⊢ ∃ (a : α), c ≤ f a
have refine_1 : ∀ (d : β) (hcd : c ≤ d) (hbd : b ≤ d), ∃ (a : α), c ≤ f a
Tactic: rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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 α
⊢ atTop ≤ map f atTop
have refine_2 : ∀ (i' : α), True → Membership.mem (γ := Filter β) atTop (f '' Ici i')
Tactic: rw [(atTop_basis.map f).ge_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
⊢ Membership.mem (γ := Filter β) atTop (f '' Ici a)
have h : ∀ (c : β) (hac : f a ≤ c) (hbc : b ≤ c), c ∈ f '' Ici a
Tactic: filter_upwards [eventually_ge_atTop (f a), eventually_ge_atTop b] with c hac hbc
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop) atTop
have 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
Tactic: choose f hl hr using exists_ge_ge (α := α)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop) atTop
have this : 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 _ _)⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
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)
have this₁ : Directed (ι := { x : α // x ∈ s }) (fun (x1 x2 : α) ↦ x1 ≤ x2) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
Tactic: rw [directedOn_iff_directed] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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))
⊢ IsDirectedOrder.{u_3} (↑s : Type u_3)
have rwa : IsDirected.{u_3 + 1} (↑s : Type u_3) fun (x1 x2 : (↑s : Type u_3)) ↦ x1 ≤ x2
Tactic: rwa [IsDirectedOrder, ← directed_id_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
⊢ IsDirectedOrder.{u_3} (↑s : Type u_3)
have rwa₁ : Directed (fun (x1 x2 : (↑s : Type u_3)) ↦ x1 ≤ x2) id
Tactic: rwa [IsDirectedOrder, ← directed_id_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop) atTop
have this₁ : IsDirectedOrder.{u_3} (↑s : Type u_3)
Tactic: have : IsDirectedOrder s := by
    rw [directedOn_iff_directed] at this
    rwa [IsDirectedOrder, ← directed_id_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
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
have refine : ∀ (c : α) (hc : c ≥ a), ∃ (x : { x : α // x ∈ s }), (↑x : α) = c ∧ ∀ (a : { x : α // x ∈ s }), (↑a : α) ≤ c ↔ a ≤ x
Tactic: refine map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
⊢ Eq (α := Filter ℤ) (map Nat.cast atTop) atTop
have refine : ∀ (n : ℤ) (hn : n ≥ 0), ∃ (x : ℕ), (↑x : ℤ) = n ∧ ∀ (a : ℕ), (↑a : ℤ) ≤ n ↔ a ≤ x
Tactic: refine map_atTop_eq_of_gc_preorder (fun _ _ ↦ Int.ofNat_le.2) 0 fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
n : ℤ
hn : n ≥ 0
⊢ ∃ (x : ℕ), (↑x : ℤ) = n ∧ ∀ (a : ℕ), (↑a : ℤ) ≤ n ↔ a ≤ x
have lift : ∀ (n : ℕ), ∃ (x : ℕ), Eq (α := ℤ) (↑x : ℤ) (↑n : ℤ) ∧ ∀ (a : ℕ), LE.le (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔ a ≤ x
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
have inl : ∀ (h : IsEmpty.{u_3 + 1} (↑(Ioi a) : Type u_3)),
  Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
Tactic: rcases isEmpty_or_nonempty (Ioi a) with h | ⟨⟨b, hb⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
inl :
  ∀ (h : IsEmpty.{u_3 + 1} (↑(Ioi a) : Type u_3)),
    Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
have inr : ∀ (b : α) (hb : b ∈ Ioi a),
  Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
Tactic: rcases isEmpty_or_nonempty (Ioi a) with h | ⟨⟨b, hb⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
have inr : Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop
  (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a))
    (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop))
Tactic: rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
inr :
  Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a))
      (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop))
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
have inr₁ : Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop atTop
Tactic: rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop)
have rw : Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop
  (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a))
    (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop))
Tactic: rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
rw :
  Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a))
      (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop))
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop)
have rw₁ : Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop atTop
Tactic: rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ioi a) : Type u_3)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
have rw : Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) ↔
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
Tactic: rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ioi a) : Type u_3)
l : Filter β
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
have rw₁ : Tendsto (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a) ∘ f) l atTop ↔
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
Tactic: rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ioi a) : Type u_3)
l : Filter β
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
rw₁ :
  Tendsto (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a) ∘ f) l atTop ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
have rw₂ : Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop ↔
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
Tactic: rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ici a) : Type u_3)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
have rw : Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) ↔
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
Tactic: rw [atTop_Ici_eq, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ici a) : Type u_3)
l : Filter β
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
have rw₁ : Tendsto (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) ∘ f) l atTop ↔
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
Tactic: rw [atTop_Ici_eq, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ici a) : Type u_3)
l : Filter β
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
rw₁ :
  Tendsto (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) ∘ f) l atTop ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
have rw₂ : Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop ↔
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
Tactic: rw [atTop_Ici_eq, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l
have rw : Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
  Tendsto f (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) l
Tactic: rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
f : α → β
l : Filter β
rw :
  Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto f (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) l
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l
have rw₁ : Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
  Tendsto (α := { x : α // x ∈ Ioi a }) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop l
Tactic: rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]