[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℕ) in atTop, p ↑n
[PROOFSTEP]
rw [← Nat.comap_cast_atTop (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℕ) in Filter.comap Nat.cast atTop, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : r ≤ ↑n
⊢ r ≤ ↑↑n
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r
[PROOFSTEP]
simpa [neg_le] using hn
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot
[PROOFSTEP]
rw [← @Int.comap_cast_atBot R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in atTop, p ↑n
[PROOFSTEP]
rw [← Int.comap_cast_atTop (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in atBot, p ↑n
[PROOFSTEP]
rw [← Int.comap_cast_atBot (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
r : R
n : ℕ
hn : r ≤ ↑n
⊢ r ≤ ↑↑n
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r
[PROOFSTEP]
simpa [neg_le]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot
[PROOFSTEP]
rw [← @Rat.comap_cast_atBot R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in atTop, p ↑n
[PROOFSTEP]
rw [← Rat.comap_cast_atTop (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in atBot, p ↑n
[PROOFSTEP]
rw [← Rat.comap_cast_atBot (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n
[PROOFSTEP]
exact
  h.comap
    _
      -- porting note: new lemma
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atTop
[PROOFSTEP]
refine' tendsto_atTop.2 fun b => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
[PROOFSTEP]
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
[PROOFSTEP]
rw [nsmul_eq_mul'] at hn 
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
[PROOFSTEP]
filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx
[GOAL]
case h
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ r * f x
[PROOFSTEP]
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
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ 1 * max b 0
[PROOFSTEP]
{ rw [one_mul]
  exact le_max_left _ _
}
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ 1 * max b 0
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ max b 0
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ 1 * max b 0 ≤ r * ↑n * max b 0
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * ↑n * max b 0 = r * (↑n * max b 0)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * (↑n * max b 0) ≤ r * f x
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atTop
[PROOFSTEP]
refine' tendsto_atTop.2 fun b => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
[PROOFSTEP]
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
[PROOFSTEP]
have hn' : 1 ≤ (n : R) * r := by rwa [nsmul_eq_mul] at hn 
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ 1 ≤ ↑n * r
[PROOFSTEP]
rwa [nsmul_eq_mul] at hn 
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
[PROOFSTEP]
filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx
[GOAL]
case h
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ f x * r
[PROOFSTEP]
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
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1
[PROOFSTEP]
{ rw [mul_one]
  exact le_max_left _ _
}
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * 1 ≤ max b 0 * (↑n * r)
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * (↑n * r) = max b 0 * ↑n * r
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * ↑n * r ≤ f x * r
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atBot
[PROOFSTEP]
simpa only [tendsto_neg_atTop_iff, mul_neg] using hf.atTop_mul_const' (neg_pos.mpr hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atBot
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← neg_mul] at hf ⊢
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x * r) l atTop
[PROOFSTEP]
exact hf.atTop_mul_const' hr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atTop
[PROOFSTEP]
simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atTop
[PROOFSTEP]
refine' tendsto_atTop.mpr fun s => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
[PROOFSTEP]
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : 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
[PROOFSTEP]
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul hr.le ha)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℕ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atBot
[PROOFSTEP]
simpa using hf.atTop_nsmul_const (neg_pos.2 hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atTop
[PROOFSTEP]
refine' tendsto_atTop.mpr fun s => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
[PROOFSTEP]
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : 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
[PROOFSTEP]
replace hn : s ≤ (n : ℤ) • r
[GOAL]
case hn
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ s ≤ ↑n • r
[PROOFSTEP]
simpa
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : 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
[PROOFSTEP]
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul hr.le ha)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atBot
[PROOFSTEP]
simpa using hf.atTop_zsmul_const (neg_pos.2 hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x • r) l atBot
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x • r) l atTop
[PROOFSTEP]
exact hf.atTop_zsmul_const hr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x • r) l atTop
[PROOFSTEP]
simpa using hf.atBot_zsmul_const (neg_pos.2 hr)
