awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto f l atTop
have rw : Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto.{u_1, u_2} (β := R) (Int.cast ∘ f) l atTop
Tactic: rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto f l atBot
have rw : Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto.{u_1, u_2} (β := R) (Int.cast ∘ f) l atBot
Tactic: rw [← @Int.comap_cast_atBot R, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in atTop, p (↑n : R)
have rw : ∀ᶠ (n : ℤ) in Filter.comap.{0, u_2} (β := R) Int.cast atTop, p (↑n : R)
Tactic: rw [← Int.comap_cast_atTop (R := R)]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in atBot, p (↑n : R)
have rw : ∀ᶠ (n : ℤ) in Filter.comap.{0, u_2} (β := R) Int.cast atBot, p (↑n : R)
Tactic: rw [← Int.comap_cast_atBot (R := R)]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto f l atTop
have rw : Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto.{u_1, u_2} (β := R) (Rat.cast ∘ f) l atTop
Tactic: rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto f l atBot
have rw : Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto.{u_1, u_2} (β := R) (Rat.cast ∘ f) l atBot
Tactic: rw [← @Rat.comap_cast_atBot R, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
R : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in atTop, p (↑n : R)
have rw : ∀ᶠ (n : ℚ) in Filter.comap.{0, u_2} (β := R) Rat.cast atTop, p (↑n : R)
Tactic: rw [← Rat.comap_cast_atTop (R := R)]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
R : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in atBot, p (↑n : R)
have rw : ∀ᶠ (n : ℚ) in Filter.comap.{0, u_2} (β := R) Rat.cast atBot, p (↑n : R)
Tactic: rw [← Rat.comap_cast_atBot (R := R)]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : IsDirectedOrder α
k : α
⊢ Eq.{u_1 + 1} (α := Filter α) (map (fun (a : α) ↦ a - k) atTop) atTop
have simp_rw : Eq.{u_1 + 1} (α := Filter α) (map (fun (a : α) ↦ a + -k) atTop) atTop
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ r * f x) l atTop
have refine : ∀ (b : R), ∀ᶠ (a : α) in l, b ≤ r * f a
Tactic: refine tendsto_atTop.2 fun b => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
have obtain : ∀ (n : ℕ) (hn : 1 ≤ n • r), ∀ᶠ (a : α) in l, b ≤ r * f a
Tactic: obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (hypothesis)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
have hn₁ : 1 ≤ r * (↑n : R)
Tactic: rw [nsmul_eq_mul'] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
have h : ∀ (x : α) (hx : (↑n : R) * max b 0 ≤ f x), b ≤ r * f x
Tactic: filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
⊢ b ≤ 1 * max b 0
have rw : b ≤ max b 0
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
⊢ b ≤ 1 * max b 0
have rw : b ≤ max b 0
Tactic: { rw [one_mul]
      exact le_max_left _ _ }
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
⊢ 1 * max b 0 ≤ r * (↑n : R) * max b 0
have ha : 0 ≤ max b 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
⊢ r * (↑n : R) * max b 0 = r * ((↑n : R) * max b 0)
have rw : r * ((↑n : R) * max b 0) = r * ((↑n : R) * max b 0)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
⊢ r * ((↑n : R) * max b 0) ≤ r * f x
have ha : 0 ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
⊢ b ≤ r * f x
have b₁ : b ≤ 1 * max b 0
Tactic: calc
    b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
b₁ : b ≤ 1 * max b 0
⊢ b ≤ r * f x
have b₂ : 1 * max b 0 ≤ r * (↑n : R) * max b 0
Tactic: calc
    b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
b₁ : b ≤ 1 * max b 0
b₂ : 1 * max b 0 ≤ r * (↑n : R) * max b 0
⊢ b ≤ r * f x
have b₃ : r * (↑n : R) * max b 0 = r * ((↑n : R) * max b 0)
Tactic: calc
    b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * (↑n : R)
x : α
hx : (↑n : R) * max b 0 ≤ f x
b₁ : b ≤ 1 * max b 0
b₂ : 1 * max b 0 ≤ r * (↑n : R) * max b 0
b₃ : r * (↑n : R) * max b 0 = r * ((↑n : R) * max b 0)
⊢ b ≤ r * f x
have b₄ : r * ((↑n : R) * max b 0) ≤ r * f x
Tactic: calc
    b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x * r) l atTop
have refine : ∀ (b : R), ∀ᶠ (a : α) in l, b ≤ f a * r
Tactic: refine tendsto_atTop.2 fun b => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
have obtain : ∀ (n : ℕ) (hn : 1 ≤ n • r), ∀ᶠ (a : α) in l, b ≤ f a * r
Tactic: obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ 1 ≤ (↑n : R) * r
have rwa : ∀ (hn : 1 ≤ (↑n : R) * r), 1 ≤ (↑n : R) * r
Tactic: rwa [nsmul_eq_mul] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (hypothesis)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
have hn' : 1 ≤ (↑n : R) * r
Tactic: have hn' : 1 ≤ (n : R) * r := by rwa [nsmul_eq_mul] at hn
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
have h : ∀ (x : α) (hx : max b 0 * (↑n : R) ≤ f x), b ≤ f x * r
Tactic: filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
⊢ b ≤ max b 0 * 1
have rw : b ≤ max b 0
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
⊢ b ≤ max b 0 * 1
have rw : b ≤ max b 0
Tactic: { rw [mul_one]
      exact le_max_left _ _ }
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
⊢ max b 0 * 1 ≤ max b 0 * ((↑n : R) * r)
have ha : 0 ≤ max b 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
⊢ max b 0 * ((↑n : R) * r) = max b 0 * (↑n : R) * r
have rw : max b 0 * ((↑n : R) * r) = max b 0 * ((↑n : R) * r)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
⊢ max b 0 * (↑n : R) * r ≤ f x * r
have ha : 0 ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
⊢ b ≤ f x * r
have b₁ : b ≤ max b 0 * 1
Tactic: calc
    b ≤ max b 0 * 1 := by
    { rw [mul_one]
      exact le_max_left _ _ }
    _ ≤ max b 0 * (n * r) := by gcongr
    _ = max b 0 * n * r := by rw [mul_assoc]
    _ ≤ f x * r := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
b₁ : b ≤ max b 0 * 1
⊢ b ≤ f x * r
have b₂ : max b 0 * 1 ≤ max b 0 * ((↑n : R) * r)
Tactic: calc
    b ≤ max b 0 * 1 := by
    { rw [mul_one]
      exact le_max_left _ _ }
    _ ≤ max b 0 * (n * r) := by gcongr
    _ = max b 0 * n * r := by rw [mul_assoc]
    _ ≤ f x * r := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
b₁ : b ≤ max b 0 * 1
b₂ : max b 0 * 1 ≤ max b 0 * ((↑n : R) * r)
⊢ b ≤ f x * r
have b₃ : max b 0 * ((↑n : R) * r) = max b 0 * (↑n : R) * r
Tactic: calc
    b ≤ max b 0 * 1 := by
    { rw [mul_one]
      exact le_max_left _ _ }
    _ ≤ max b 0 * (n * r) := by gcongr
    _ = max b 0 * n * r := by rw [mul_assoc]
    _ ≤ f x * r := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ (↑n : R) * r
x : α
hx : max b 0 * (↑n : R) ≤ f x
b₁ : b ≤ max b 0 * 1
b₂ : max b 0 * 1 ≤ max b 0 * ((↑n : R) * r)
b₃ : max b 0 * ((↑n : R) * r) = max b 0 * (↑n : R) * r
⊢ b ≤ f x * r
have b₄ : max b 0 * (↑n : R) * r ≤ f x * r
Tactic: calc
    b ≤ max b 0 * 1 := by
    { rw [mul_one]
      exact le_max_left _ _ }
    _ ≤ max b 0 * (n * r) := by gcongr
    _ = max b 0 * n * r := by rw [mul_assoc]
    _ ≤ f x * r := by gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x * r) l atBot
have simp : ∀ (hf : Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ -f x) l atTop),
  Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ -f x * r) l atTop
Tactic: simp only [← tendsto_neg_atTop_iff, ← neg_mul] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : IsOrderedCancelAddMonoid R
inst_3 : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atTop
have refine : ∀ (s : R), ∀ᶠ (a : α) in l, s ≤ f a • r
Tactic: refine tendsto_atTop.mpr fun s => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : IsOrderedCancelAddMonoid R
inst_3 : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
have obtain : ∀ (n : ℕ) (hn : s ≤ n • r), ∀ᶠ (a : α) in l, s ≤ f a • r
Tactic: obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atTop
have refine : ∀ (s : R), ∀ᶠ (a : α) in l, s ≤ f a • r
Tactic: refine tendsto_atTop.mpr fun s => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
have obtain : ∀ (n : ℕ) (hn : s ≤ n • r), ∀ᶠ (a : α) in l, s ≤ f a • r
Tactic: obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (hypothesis)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
have hn₁ : s ≤ HSMul.hSMul (α := ℤ) (↑n : ℤ) r
Tactic: replace hn : s ≤ (n : ℤ) • r := by simpa
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Archimedean (goal)
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atBot
have simp : ∀ (hf : Tendsto (β := ℤ) (fun (x : α) ↦ -f x) l atTop), Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ -f x • r) l atTop
Tactic: simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
⊢ HasBasis atTop (fun (x : α) ↦ a < x) Ioi
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
⊢ HasBasis atTop (fun (x : α) ↦ a < x) Ioi
have refine : ∀ (b : α), True → ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
Tactic: refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
b : α
h : True
⊢ ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
have obtain : ∀ (c : α) (hac : a ≤ c) (hbc : b ≤ c), ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
Tactic: obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
b : α
h : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
have obtain : ∀ (d : α) (hcd : c < d), ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
Tactic: obtain ⟨d, hcd⟩ := exists_gt c
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
⊢ HasBasis atTop (fun (x : α) ↦ a ≤ x) Ici
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
this : Nonempty α
⊢ HasBasis atTop (fun (x : α) ↦ a ≤ x) Ici
have refine : ∀ (b : α), True → ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b
Tactic: refine atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
this : Nonempty α
b : α
h : True
⊢ ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b
have obtain : ∀ (c : α) (hac : a ≤ c) (hbc : b ≤ c), ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b
Tactic: obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_6
inst : Preorder α
⊢ NeBot.{u_6} (α := α) atTop ↔ Nonempty α ∧ IsDirectedOrder α
have refine : ∀ (h : NeBot.{u_6} (α := α) atTop) (x y : α), ∃ (c : α), x ≤ c ∧ y ≤ c
Tactic: refine ⟨fun h ↦ ⟨nonempty_of_neBot atTop, ⟨fun x y ↦ ?_⟩⟩, fun ⟨h₁, h₂⟩ ↦ atTop_neBot⟩
-- 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 : Nonempty α
r : α → β → Prop
⊢ (∃ (b : β), ∀ᶠ (a : α) in atTop, r a b) ↔ ∀ᶠ (a₀ : α) in atTop, ∃ (b : β), ∀ a ≥ a₀, r a b
have simp_rw : (∃ (a : α) (b : β), ∀ b_1 ≥ a, r b_1 b) ↔ ∃ (a : α), ∀ b ≥ a, ∃ (b_1 : β), ∀ a ≥ b, r a b_1
Tactic: simp_rw [eventually_atTop, ← exists_comm (α := α)]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
Goal:
P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
have h₁ : ∀ (a : ℕ), ∃ b > a, P b
Tactic: rw [frequently_atTop'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
Goal:
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in atTop, P n k
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
have h₁ : ∀ (n a : ℕ), ∃ b > a, P n b
Tactic: simp only [frequently_atTop'] at h
Cleared hypotheses: h