awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
hs : Monotone s
f g : (a : α) → β a
a : α
inl :
  ∀ (i : ι) (hi : a ∈ s i),
    ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
have inr : ∀ (ha : ¬∃ (i : ι), a ∈ s i),
  ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
Tactic: rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
hs : Monotone s
f g : (a : α) → β a
a : α
i : ι
hi : a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
have inl : ∀ (j : ι) (hij : i ≤ j), (s j).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
Tactic: refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ (i : ι), a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
have inr : ∀ (i : ι), (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
Tactic: filter_upwards with i
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋂ (i : ι), s i) f g a
have h : ∀ (x : ι), ((compl ∘ s) x).piecewise (β := β) g f a = (s x).piecewise (β := β) f g a
Tactic: convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
h : ∀ (x : ι), ((compl ∘ s) x).piecewise (β := β) g f a = (s x).piecewise (β := β) f g a
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋂ (i : ι), s i) f g a
have h₁ : ∀ (x : ι), piecewise (β := β) (⋃ (i : ι), (compl ∘ s) i) g f a = piecewise (β := β) (⋂ (i : ι), s i) f g a
Tactic: convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋂ (i : ι), s i) f g a
have h : ∀ (x : ι), ((compl ∘ s) x).piecewise (β := β) g f a = (s x).piecewise (β := β) f g a
Tactic: classical
  convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
  · convert! congr_fun (Set.piecewise_compl (s _) g f) a
  · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
h : ∀ (x : ι), ((compl ∘ s) x).piecewise (β := β) g f a = (s x).piecewise (β := β) f g a
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋂ (i : ι), s i) f g a
have h₁ : ∀ (x : ι), piecewise (β := β) (⋃ (i : ι), (compl ∘ s) i) g f a = piecewise (β := β) (⋂ (i : ι), s i) f g a
Tactic: classical
  convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
  · convert! congr_fun (Set.piecewise_compl (s _) g f) a
  · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Disjoint (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop
have rcases : ∀ (x y : α) (hne : x ≠ y), Disjoint.{u_3} (α := Filter α) atBot atTop
Tactic: rcases exists_pair_ne α with ⟨x, y, hne⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Disjoint (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop
have pos : ∀ (hle : x ≤ y), Disjoint.{u_3} (α := Filter α) atBot atTop
Tactic: by_cases hle : x ≤ y
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Disjoint (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
pos : ∀ (hle : x ≤ y), Disjoint.{u_3} (α := Filter α) atBot atTop
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop
have neg : ∀ (hle : ¬x ≤ y), Disjoint.{u_3} (α := Filter α) atBot atTop
Tactic: by_cases hle : x ≤ y
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Disjoint (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop
have pos : Disjoint (Iic x) (Ici y)
Tactic: refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Disjoint (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop
have neg : Disjoint (Iic y) (Ici x)
Tactic: refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r
have refine : ∀ (hrf : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop) (hr : r ≤ 0), False
Tactic: refine ⟨fun hrf => not_le.mp fun hr => ?_, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop
hr : r ≤ 0
⊢ False
have rcases : ∀ (x : β) (hx : 0 ≤ f x) (hrx : 0 < r * f x), False
Tactic: rcases ((h.eventually_ge_atTop 0).and (hrf.eventually_gt_atTop 0)).exists with ⟨x, hx, hrx⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
⊢ Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c
have refine_1 : ∀ (h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop), n ≠ 0
Tactic: refine ⟨fun h => ⟨?_, ?_⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
refine_1 : ∀ (h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop), n ≠ 0
⊢ Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c
have refine_2 : ∀ (h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop), 0 < c
Tactic: refine ⟨fun h => ⟨?_, ?_⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop
⊢ 0 < c
have refine_2 : ∀ (k : α) (hck : 0 < c * k ^ n) (hk : 0 ≤ k), 0 < c
Tactic: rcases ((h.eventually_gt_atTop 0).and (eventually_ge_atTop 0)).exists with ⟨k, hck, hk⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℤ
hn : 0 < n
⊢ Tendsto (β := α) (fun (x : α) ↦ x ^ n) atTop atTop
have lift : ∀ (n : ℕ) (hn : LT.lt (α := ℤ) 0 (↑n : ℤ)), Tendsto (β := α) (fun (x : α) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ)) atTop atTop
Tactic: lift n to ℕ using hn.le
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k : α
hk : 0 < k
a b : α
h : b ≥ 1
⊢ a / k ≤ b ↔ a ≤ (fun (b : α) ↦ k * b) b
have rw : a ≤ k * b ↔ a ≤ (fun (b : α) ↦ k * b) b
Tactic: rw [div_le_iff₀' hk]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
h : b ≥ 1
⊢ b ≤ (fun (b : α) ↦ k * b) b / k
have hb : k ≠ 0
Tactic: rw [mul_div_assoc, mul_div_cancel₀]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
have inl : ∀ (hr : r < 0),
  Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Tactic: rcases lt_trichotomy r 0 with (hr | rfl | hr)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
inl :
  ∀ (hr : r < 0),
    Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
have inr : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ 0 * f x) l atTop ↔
  LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atTop ∨ LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atBot
Tactic: rcases lt_trichotomy r 0 with (hr | rfl | hr)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Field (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
inl :
  ∀ (hr : r < 0),
    Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
inr :
  Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ 0 * f x) l atTop ↔
    LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atTop ∨ LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
have inr₁ : ∀ (hr : 0 < r),
  Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Tactic: rcases lt_trichotomy r 0 with (hr | rfl | hr)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x
have refine : ∀ (h : ∀ᶠ (x : α) in atTop, p x), ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
Tactic: refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
have rcases : ∀ (S : Set α) (hSf : S.Finite) (hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x),
  ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
Tactic: rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
have refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋂ (i : (↑S : Type u_3)), (fun (x : (↑S : Type u_3)) ↦ Ici (↑x : α)) i) x)
  (y : α) (hy : x ≤ y), p y
Tactic: refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x
x : α
hx : Membership.mem (γ := Set α) (⋂ (i : (↑S : Type u_3)), (fun (x : (↑S : Type u_3)) ↦ Ici (↑x : α)) i) x
y : α
hy : x ≤ y
⊢ p y
have hS₁ : ∀ ⦃x : α⦄, (∀ (i : α) (i_1 : i ∈ S), x ∈ Ici i) → p x
Tactic: simp only [mem_iInter] at hS hx
Cleared hypotheses: hS, hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x
x : α
hx : Membership.mem (γ := Set α) (⋂ (i : (↑S : Type u_3)), (fun (x : (↑S : Type u_3)) ↦ Ici (↑x : α)) i) x
y : α
hy : x ≤ y
hS₁ : ∀ ⦃x : α⦄, (∀ (i : α) (i_1 : i ∈ S), x ∈ Ici i) → p x
⊢ p y
have hx₁ : ∀ (i : (↑S : Type u_3)), x ∈ Ici (↑i : α)
Tactic: simp only [mem_iInter] at hS hx
Cleared hypotheses: hS, hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
have h_evtl₁ : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
Tactic: rw [← Filter.eventually_forall_le_atBot] at h_evtl
Cleared hypotheses: h_evtl
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ n ≥ N, ∀ k < n, u k < u n
have obtain : ∀ (k : ℕ) (hku : ∀ l ≤ N, u l ≤ u k), ∃ n ≥ N, ∀ k < n, u k < u n
Tactic: obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k :=
    exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
⊢ ∃ n ≥ N, ∀ k < n, u k < u n
have ex : ∃ n ≥ N, u k < u n
Tactic: have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
⊢ ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k
have rcases : ∀ (n : ℕ) (hn_min : ∀ m < n, ¬(m ≥ N ∧ u k < u m)) (hnN : n ≥ N) (hnk : u k < u n),
  ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k
Tactic: rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hn_min : ∀ m < n, ¬(m ≥ N ∧ u k < u m)
hnN : n ≥ N
hnk : u k < u n
⊢ ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k
have hn_min₁ : ∀ m < n, ∀ (_ : m ≥ N), u m ≤ u k
Tactic: push Not at hn_min
Cleared hypotheses: hn_min
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
⊢ ∃ n ≥ N, ∀ k < n, u k < u n
have obtain : ∀ (n : ℕ) (hnN : n ≥ N) (hnk : u k < u n) (hn_min : ∀ m < n, N ≤ m → u m ≤ u k), ∃ n ≥ N, ∀ k < n, u k < u n
Tactic: obtain ⟨n : ℕ, hnN : n ≥ N, hnk : u k < u n, hn_min : ∀ m, m < n → N ≤ m → u m ≤ u k⟩ :
      ∃ n ≥ N, u k < u n ∧ ∀ m, m < n → N ≤ m → u m ≤ u k := by
    rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
    push Not at hn_min
    exact ⟨n, hnN, hnk, hn_min⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, N ≤ m → u m ≤ u k
⊢ ∃ n ≥ N, ∀ k < n, u k < u n
have right : ∀ k < n, u k < u n
Tactic: use n, hnN
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
⊢ ∀ᶠ (a : ℕ) in atTop, p a
have simp : ∀ (hp : ∀ k < n, ∃ (a : ℕ), ∀ b ≥ a, p (n * b + k)), ∃ (a : ℕ), ∀ b ≥ a, p b
Tactic: simp only [eventually_atTop] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∃ (a : ℕ), ∀ b ≥ a, p (n * b + k)
⊢ ∃ (a : ℕ), ∀ b ≥ a, p b
have choose! : ∀ (N : (k : ℕ) → ℕ) (hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)), ∃ (a : ℕ), ∀ b ≥ a, p b
Tactic: choose! N hN using hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
⊢ ∃ (a : ℕ), ∀ b ≥ a, p b
have refine : ∀ (b : ℕ) (hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x), p b
Tactic: refine ⟨(Finset.range n).sup (n * N ·), fun b hb => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
⊢ p b
have rw : p (n * (b / n) + b % n)
Tactic: rw [← Nat.div_add_mod b n]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
⊢ p (n * (b / n) + b % n)
have have : ∀ (hlt : b % n < n), p (n * (b / n) + b % n)
Tactic: have hlt := Nat.mod_lt b hn.bot_lt
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
hlt : b % n < n
⊢ p (n * (b / n) + b % n)
have refine : b / n ≥ N (b % n)
Tactic: refine hN _ hlt _ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
hlt : b % n < n
⊢ b / n ≥ N (b % n)
have rw : n * N (b % n) ≤ b
Tactic: rw [ge_iff_le, Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
α : 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 ∘ φ)
have rsuffices : ∀ (φ : ℕ → ℕ) (hφ : StrictMono φ) (hrφ : ∀ (m n : ℕ), m < n → 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)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
rsuffices :
  ∀ (φ : ℕ → ℕ) (hφ : StrictMono φ) (hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)
have rsuffices₁ : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
Tactic: rsuffices ⟨φ, hφ, hrφ⟩ : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ m n, m < n → r (φ m) (φ n)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
α : 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)
have this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, 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 _)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
α : 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)
have rcases : ∀ (φ : ℕ → ℕ) (hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → 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φ⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
α : 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)
have hφ₁ : (∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → φ x_1 < φ x) ∧ ∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → r (φ x_1) (φ x)
Tactic: simp only [forall_mem_image, forall_and, mem_Iio] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, c ^ n < (n - d)!
have rw : ∃ (a : ℕ), ∀ b ≥ a, c ^ b < (b - d)!
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d : ℕ
⊢ ∃ (a : ℕ), ∀ b ≥ a, c ^ b < (b - d)!
have refine : ∀ b ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1), c ^ b < (b - d)!
Tactic: refine ⟨2 * (c ^ 2 + d + 1), ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d n : ℕ
hn : n ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
⊢ c ^ n < (n - d)!
have obtain : ∀ (d' : ℕ) (hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)),
  c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
Tactic: obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
have inl : ∀ (hn : 2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1) + d' ≥ 2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1)),
  HPow.hPow (α := ℕ) 0 (2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1) + d') <
    (2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1) + d' - d)!
Tactic: obtain (rfl | c0) := c.eq_zero_or_pos
Cleared hypotheses: c, hn