awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ c ^ i - 1 ≤ (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
(Nat.sub_one_lt_floor _).le

Premises used: LT.lt.le, Nat.sub_one_lt_floor
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
c₁ : (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹
c₂ : c ^ i - c ^ i * c⁻¹ ≤ c ^ i - 1
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
calc
    (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
    _ ≤ c ^ i - 1 := by
      gcongr
      simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi
    _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le

Premises used: HSub.hSub, LT.lt.le, Inv.inv, Nat.sub_one_lt_floor, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ 0 < 1 - c⁻¹

Tactic:
have A : 0 < 1 - c⁻¹ := sub_pos.2 (inv_lt_one_of_one_lt₀ hc)
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
h : ∀ (k : ℕ) (hk : k ∈ range N), (↑⌊c ^ k⌋₊ : ℝ) ≤ c ^ k
⊢ LE.le (α := ℝ) (∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)

Tactic:
gcongr with k hk
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
k : ℕ
hk : k ∈ range N
⊢ 0 ≤ c ^ k

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
k : ℕ
hk : k ∈ range N
⊢ (↑⌊c ^ k⌋₊ : ℝ) ≤ c ^ k

Tactic:
exact Nat.floor_le (by positivity)

Premises used: Nat.floor_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
h :
  ∀ i ∈ {i ∈ range N | j < c ^ i},
    1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
      HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2)
⊢ LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2))

Tactic:
gcongr with i
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : 1 * HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
h₁ : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
h₂ : 0 < HPow.hPow (β := ℕ) (c ^ i) 2
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2)

Tactic:
rw [mul_div_assoc', mul_one, div_le_div_iff₀]

Premises used: mul_div_assoc', div_le_div_iff₀, mul_one
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : LT.lt (α := ℝ) 0 (↑⌊c ^ i⌋₊ : ℝ)
⊢ 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2

Tactic:
apply sq_pos_of_pos

Premises used: sq_pos_of_pos
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ LT.lt (α := ℝ) 0 (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
zero_lt_one.trans_le ?_

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : LE.le (α := ℝ) 1 (↑⌊c ^ i⌋₊ : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
refine zero_lt_one.trans_le ?_

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ LE.le (α := ℝ) 1 (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]

Premises used: Nat.one_le_cast, one_le_pow₀, LT.lt.le, Nat.le_floor, Nat.cast_one
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < HPow.hPow (β := ℕ) (c ^ i) 2

Tactic:
sq_pos_of_pos (pow_pos cpos _)

Premises used: pow_pos, sq_pos_of_pos
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < HPow.hPow (β := ℕ) (c ^ i) 2

Tactic:
exact sq_pos_of_pos (pow_pos cpos _)

Premises used: pow_pos, sq_pos_of_pos
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) ((1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)) 2
⊢ 1 * HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2

Tactic:
rw [one_mul, ← mul_pow]

Premises used: mul_pow, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : c ^ i ≤ (1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)
⊢ HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) ((1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)) 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
⊢ c ^ i ≤ (1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]

Premises used: mul_comm, div_eq_inv_mul, le_div_iff₀
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
mul_pow_le_nat_floor_pow hc i

Premises used: mul_pow_le_nat_floor_pow
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
exact mul_pow_le_nat_floor_pow hc i

Premises used: mul_pow_le_nat_floor_pow
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
rw :
  HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2)
⊢ ∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2) ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2

Tactic:
rw [← mul_sum, ← mul_div_assoc']

Premises used: Finset.mul_sum, mul_div_assoc'
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
hbc :
  ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
⊢ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2

Tactic:
sum_div_pow_sq_le_div_sq N hj hc

Premises used: sum_div_pow_sq_le_div_sq
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2

Tactic:
exact sum_div_pow_sq_le_div_sq N hj hc

Premises used: sum_div_pow_sq_le_div_sq
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
e_a :
  HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) =
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3
⊢ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2 =
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) =
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3

Tactic:
field
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i :
  LE.le (α := ℝ) (∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
i₁ :
  LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2))
i₂ :
  ∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2) ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2
i₃ :
  HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2 =
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
⊢ ∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2

Tactic:
calc
    (∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤
        ∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2 := by
      gcongr with k hk; exact Nat.floor_le (by positivity)
    _ ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * ((1 : ℝ) / (c ^ i) ^ 2) := by
      gcongr with i
      rw [mul_div_assoc', mul_one, div_le_div_iff₀]; rotate_left
      · apply sq_pos_of_pos
        refine zero_lt_one.trans_le ?_
        simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]
      · exact sq_pos_of_pos (pow_pos cpos _)
      rw [one_mul, ← mul_pow]
      gcongr
      rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]
      exact mul_pow_le_nat_floor_pow hc i
    _ ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 := by
      rw [← mul_sum, ← mul_div_assoc']
      gcongr
      exact sum_div_pow_sq_le_div_sq N hj hc
    _ = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2 := by
      congr 1
      field

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.cast, Finset.range, Inv.inv, HPow.hPow, LT.lt, Nat.floor, OfNat.ofNat, Finset.filter, Finset.sum
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
rw : Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm.{u_1} (E := α) (↑x : α)) atTop atTop
⊢ Tendsto Nat.cast atTop (Bornology.cobounded α)

Tactic:
rw [← tendsto_norm_atTop_iff_cobounded]

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm.{u_1} (E := α) (↑x : α)) atTop atTop

Tactic:
simpa [norm_natCast_eq_mul_norm_one] using tendsto_natCast_atTop_atTop
    |>.atTop_mul_const (norm_pos_iff.mpr one_ne_zero)

Premises used: Iff.mpr, norm_natCast_eq_mul_norm_one, norm_pos_iff, Filter.Tendsto.atTop_mul_const, tendsto_natCast_atTop_atTop, one_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
rw : Tendsto (β := ℝ) (fun (x : ℤ) ↦ norm.{u_1} (E := α) (↑x : α)) (atBot ⊔ atTop) atTop
⊢ Tendsto Int.cast (atBot ⊔ atTop) (Bornology.cobounded α)

Tactic:
rw [← tendsto_norm_atTop_iff_cobounded]

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
⊢ Tendsto (β := ℝ) (fun (x : ℤ) ↦ norm.{u_1} (E := α) (↑x : α)) (atBot ⊔ atTop) atTop

Tactic:
simpa [norm_intCast_eq_abs_mul_norm_one] using tendsto_intCast_atTop_atTop
    |>.comp (tendsto_abs_atBot_atTop.sup tendsto_abs_atTop_atTop)
    |>.atTop_mul_const (norm_pos_iff.mpr one_ne_zero)

Premises used: Iff.mpr, norm_pos_iff, Filter.Tendsto.atTop_mul_const, Filter.tendsto_abs_atBot_atTop, Filter.Tendsto.sup, norm_intCast_eq_abs_mul_norm_one, Filter.Tendsto.comp, one_ne_zero, tendsto_intCast_atTop_atTop, Filter.tendsto_abs_atTop_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
⊢ Tendsto Int.cast atBot (Bornology.cobounded α)

Tactic:
tendsto_intCast_atBot_sup_atTop_cobounded.mono_left le_sup_left

Premises used: le_sup_left, tendsto_intCast_atBot_sup_atTop_cobounded, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
⊢ Tendsto Int.cast atTop (Bornology.cobounded α)

Tactic:
tendsto_intCast_atBot_sup_atTop_cobounded.mono_left le_sup_right

Premises used: tendsto_intCast_atBot_sup_atTop_cobounded, le_sup_right, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r₁ r₂ : ℝ
h₁ : 0 ≤ r₁
h₂ : r₁ < r₂
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ r₂ ^ n

Tactic:
have H : 0 < r₂ := h₁.trans_lt h₂
  (isLittleO_of_tendsto fun _ hn ↦ False.elim <| H.ne' <| eq_zero_of_pow_eq_zero hn) <|
    (tendsto_pow_atTop_nhds_zero_of_lt_one
      (div_nonneg h₁ (h₁.trans h₂.le)) ((div_lt_one H).2 h₂)).congr fun _ ↦ div_pow _ _ _

Premises used: Iff.mpr, False.elim, Asymptotics.isLittleO_of_tendsto, LT.lt.le, LT.lt.ne', div_lt_one, div_pow, tendsto_pow_atTop_nhds_zero_of_lt_one, Filter.Tendsto.congr, div_nonneg, eq_zero_of_pow_eq_zero, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r₁ r₂ : ℝ
h₁ : 0 ≤ r₁
h₂ : r₁ ≤ r₂
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ r₂ ^ n

Tactic:
h₂.eq_or_lt.elim (fun h ↦ h ▸ isBigO_refl _ _) fun h ↦ (isLittleO_pow_pow_of_lt_left h₁ h).isBigO

Premises used: LE.le.eq_or_lt, Eq.rec, Filter.atTop, Asymptotics.IsLittleO.isBigO, HPow.hPow, isLittleO_pow_pow_of_lt_left, Or.elim, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ r₂ ^ n

Tactic:
(IsLittleO.of_norm_left ?_).of_norm_right

Premises used: Asymptotics.IsLittleO.of_norm_left, Asymptotics.IsLittleO.of_norm_right
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖r₁ ^ x‖) fun (x : ℕ) ↦ ‖r₂ ^ x‖
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ r₂ ^ n

Tactic:
refine (IsLittleO.of_norm_left ?_).of_norm_right

Premises used: Asymptotics.IsLittleO.of_norm_left, Asymptotics.IsLittleO.of_norm_right
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖r₁ ^ x‖) fun (x : ℕ) ↦ ‖r₂ ^ x‖

Tactic:
(isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)

Premises used: isLittleO_pow_pow_of_lt_left, pow_abs, Asymptotics.IsLittleO.congr, abs_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖r₁ ^ x‖) fun (x : ℕ) ↦ ‖r₂ ^ x‖

Tactic:
exact (isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)

Premises used: isLittleO_pow_pow_of_lt_left, pow_abs, Asymptotics.IsLittleO.congr, abs_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
⊢ Set.Ico 0 R ⊆ Set.Ioo (-R) R

Tactic:
have A : Ico 0 R ⊆ Ioo (-R) R :=
    fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
⊢ Set.Ioo 0 R ⊆ Set.Ioo (-R) R

Tactic:
have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
1 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
tfae_have 1 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
tfae_have 2 → 1 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo (-R) R
H : IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
rcases : ∀ (b : ℝ) (hab : |a| < b) (hbR : b < R), ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩

Premises used: Iff.mpr, exists_between, abs_lt
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo (-R) R
H : IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
b : ℝ
hab : |a| < b
hbR : b < R
⊢ ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
      H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩

Premises used: le_abs_self, isLittleO_pow_pow_of_abs_lt_left, LT.lt.trans_le, And.intro, Exists.intro, Asymptotics.IsBigO.trans_isLittleO, LE.le.trans_lt, abs_nonneg