awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Int.cast atTop, p (↑n : R)

Tactic:
h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Int.cast atTop, p (↑n : R)

Tactic:
exact h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw : ∀ᶠ (n : ℤ) in Filter.comap.{0, u_2} (β := R) Int.cast atBot, p (↑n : R)
⊢ ∀ᶠ (n : ℤ) in atBot, p (↑n : R)

Tactic:
rw [← Int.comap_cast_atBot (R := R)]

Premises used: Int.comap_cast_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Int.cast atBot, p (↑n : R)

Tactic:
h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Int.cast atBot, p (↑n : R)

Tactic:
exact h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
r : R
n : ℕ
hn : r ≤ (↑n : R)
⊢ r ≤ (↑(↑n : ℚ) : R)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
r : R
n : ℕ
hn : -r ≤ (↑n : R)
⊢ (↑(-(↑n : ℚ)) : R) ≤ r

Tactic:
simpa [neg_le]

Premises used: neg_le
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 α
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
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, Rat.comap_cast_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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.{u_1, u_2} (β := R) (Rat.cast ∘ f) l atTop

Tactic:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 α
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
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto f l atBot

Tactic:
rw [← @Rat.comap_cast_atBot R, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, Rat.comap_cast_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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.{u_1, u_2} (β := R) (Rat.cast ∘ f) l atBot

Tactic:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw : ∀ᶠ (n : ℚ) in Filter.comap.{0, u_2} (β := R) Rat.cast atTop, p (↑n : R)
⊢ ∀ᶠ (n : ℚ) in atTop, p (↑n : R)

Tactic:
rw [← Rat.comap_cast_atTop (R := R)]

Premises used: Rat.comap_cast_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Rat.cast atTop, p (↑n : R)

Tactic:
h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Rat.cast atTop, p (↑n : R)

Tactic:
exact h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw : ∀ᶠ (n : ℚ) in Filter.comap.{0, u_2} (β := R) Rat.cast atBot, p (↑n : R)
⊢ ∀ᶠ (n : ℚ) in atBot, p (↑n : R)

Tactic:
rw [← Rat.comap_cast_atBot (R := R)]

Premises used: Rat.comap_cast_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Rat.cast atBot, p (↑n : R)

Tactic:
h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 Filter.comap.{0, u_2} (β := R) Rat.cast atBot, p (↑n : R)

Tactic:
exact h.comap _

Premises used: Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
⊢ HasAntitoneBasis.{u_2, 0} (α := R) atTop fun (n : ℕ) ↦ Ici (↑n : R)

Tactic:
hasAntitoneBasis_atTop.comp_mono Nat.mono_cast tendsto_natCast_atTop_atTop

Premises used: Set.Ici, Nat.mono_cast, setOf, Filter.hasAntitoneBasis_atTop, Filter.HasAntitoneBasis.comp_mono, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
⊢ HasCountableBasis.{u_2, 0} (α := R) atTop (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ Ici (↑n : R)

Tactic:
⟨atTop_hasAntitoneBasis_of_archimedean.1, to_countable _⟩

Premises used: Filter.HasCountableBasis.mk, Filter.HasAntitoneBasis.toHasBasis, Set.to_countable, atTop_hasAntitoneBasis_of_archimedean
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
⊢ IsCountablyGenerated.{u_2} (α := R) atTop

Tactic:
atTop_hasCountableBasis_of_archimedean.isCountablyGenerated

Premises used: atTop_hasCountableBasis_of_archimedean, Filter.HasCountableBasis.isCountablyGenerated
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
⊢ IsCountablyGenerated.{u_2} (α := R) atBot

Tactic:
atBot_hasCountableBasis_of_archimedean.isCountablyGenerated

Premises used: Filter.HasCountableBasis.isCountablyGenerated, atBot_hasCountableBasis_of_archimedean
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : IsDirectedOrder α
k : α
⊢ ∀ (a c : α), c ≥ 0 → (a + k ≤ c ↔ a ≤ (fun (a : α) ↦ a - k) c)

Tactic:
simp [le_sub_iff_add_le]

Premises used: le_sub_iff_add_le
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : IsDirectedOrder α
k : α
⊢ ∀ c ≥ 0, c ≤ (fun (a : α) ↦ a - k) c + k

Tactic:
simp
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : IsDirectedOrder α
k : α
simp_rw : Eq.{u_1 + 1} (α := Filter α) (map (fun (a : α) ↦ a + -k) atTop) atTop
⊢ Eq.{u_1 + 1} (α := Filter α) (map (fun (a : α) ↦ a - k) atTop) atTop

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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

Tactic:
apply map_add_atTop_eq

Premises used: Filter.map_add_atTop_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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

Tactic:
tendsto_atTop.2 fun b => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
refine : ∀ (b : R), ∀ᶠ (a : α) in l, b ≤ r * f a
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ r * f x) l atTop

Tactic:
refine tendsto_atTop.2 fun b => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
obtain : ∀ (n : ℕ) (hn : 1 ≤ n • r), ∀ᶠ (a : α) in l, b ≤ r * f a
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a

Tactic:
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr

Premises used: Archimedean.arch, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 ≤ r * (↑n : R)

Tactic:
rw [nsmul_eq_mul'] at hn

Premises used: nsmul_eq_mul'
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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)
h : ∀ (x : α) (hx : (↑n : R) * max b 0 ≤ f x), b ≤ r * f x
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a

Tactic:
filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx

Premises used: HMul.hMul, Filter.tendsto_atTop, Nat.cast, Max.max, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw : b ≤ max b 0
⊢ b ≤ 1 * max b 0

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 ≤ max b 0

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 ≤ max b 0

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw rw₁ rw₂ : b ≤ max b 0
⊢ b ≤ 1 * max b 0

Tactic:
{ rw [one_mul]
      exact le_max_left _ _ }

Premises used: le_max_left, one_mul
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
ha : 0 ≤ max b 0
⊢ 1 * max b 0 ≤ r * (↑n : R) * max b 0

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw rw₁ : r * ((↑n : R) * max b 0) = r * ((↑n : R) * max b 0)
⊢ r * (↑n : R) * max b 0 = r * ((↑n : R) * max b 0)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
ha : 0 ≤ r
⊢ r * ((↑n : R) * max b 0) ≤ r * f x

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 * ((↑n : R) * max b 0) ≤ r * f x
⊢ b ≤ 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

Premises used: HMul.hMul, Nat.cast, Max.max, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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

Tactic:
tendsto_atTop.2 fun b => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
refine : ∀ (b : R), ∀ᶠ (a : α) in l, b ≤ f a * r
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x * r) l atTop

Tactic:
refine tendsto_atTop.2 fun b => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
obtain : ∀ (n : ℕ) (hn : 1 ≤ n • r), ∀ᶠ (a : α) in l, b ≤ f a * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r

Tactic:
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr

Premises used: Archimedean.arch, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (hn : 1 ≤ (↑n : R) * r), 1 ≤ (↑n : R) * r
⊢ 1 ≤ (↑n : R) * r

Tactic:
rwa [nsmul_eq_mul] at hn

Premises used: nsmul_eq_mul
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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

Tactic:
have hn' : 1 ≤ (n : R) * r := by rwa [nsmul_eq_mul] at hn
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
h : ∀ (x : α) (hx : max b 0 * (↑n : R) ≤ f x), b ≤ f x * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r

Tactic:
filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx

Premises used: HMul.hMul, Filter.tendsto_atTop, Nat.cast, Max.max, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw : b ≤ max b 0
⊢ b ≤ max b 0 * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw rw₁ rw₂ : b ≤ max b 0
⊢ b ≤ max b 0 * 1

Tactic:
{ rw [mul_one]
      exact le_max_left _ _ }

Premises used: mul_one, le_max_left
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
ha : 0 ≤ max b 0
⊢ max b 0 * 1 ≤ max b 0 * ((↑n : R) * r)

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
rw rw₁ : max b 0 * ((↑n : R) * r) = max b 0 * ((↑n : R) * r)
⊢ max b 0 * ((↑n : R) * r) = max b 0 * (↑n : R) * r

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
ha : 0 ≤ r
⊢ max b 0 * (↑n : R) * r ≤ f x * r

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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₄ : max b 0 * (↑n : R) * r ≤ f x * r
⊢ b ≤ 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

Premises used: HMul.hMul, Nat.cast, Max.max, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 : r < 0
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x * r) l atBot

Tactic:
simpa only [tendsto_neg_atTop_iff, mul_neg] using hf.atTop_mul_const' (neg_pos.mpr hr)

Premises used: Iff.mpr, neg_pos, Filter.Tendsto.atTop_mul_const', Filter.tendsto_neg_atTop_iff, mul_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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
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
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x * r) l atBot

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_mul] at hf ⊢

Premises used: neg_mul, Filter.tendsto_neg_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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.{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:
hf.atTop_mul_const' hr

Premises used: Filter.Tendsto.atTop_mul_const'
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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.{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:
exact hf.atTop_mul_const' hr

Premises used: Filter.Tendsto.atTop_mul_const'
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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 : r < 0
hf : Tendsto f l atBot
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x * r) l atTop

Tactic:
simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)

Premises used: Iff.mpr, Filter.Tendsto.atBot_mul_const', neg_pos, Filter.tendsto_neg_atBot_iff, mul_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
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

Tactic:
tendsto_atTop.mpr fun s => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop