-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma isBigO_atTop_F_nat_one {a : ℝ} (ha : 0 ≤ a) : ∃ p, 0 < p ∧
    F_nat 1 a =O[atTop] fun t ↦ exp (-p * t)

Proof state:
case inr
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)

Tactic:
refine ⟨π * a ^ 2, mul_pos pi_pos <| pow_pos ha' _, IsBigO.add ?_ ?_⟩

Result:
case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2) =O[atTop] fun t => rexp (-(π * a ^ 2) * t)

case inr.refine_2
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-(π * a ^ 2) * t)

Proof state:
a : ℝ
ha : 0 ≤ a
⊢ ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)

Tactic:
have aux' : IsBigO atTop (fun t : ℝ ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) (fun _ ↦ (1 : ℝ)) := by
  simpa only [inv_pow, one_pow] using isBigO_one_aux.pow 2

Result:
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
⊢ ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)

Proof state:
case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2) =O[atTop] fun t => rexp (-(π * a ^ 2) * t)

Tactic:
conv_rhs => enter [t]; rw [← mul_one (rexp _)]

Result:
case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2) =O[atTop] fun t => rexp (-(π * a ^ 2) * t) * 1

Proof state:
case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-π * (a ^ 2 + 1) * x)‖ ≤ rexp (-(π * a ^ 2) * x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * (a ^ 2 + 1) * t)‖ ≤ rexp (-(π * a ^ 2) * t)

Proof state:
case h
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
t : ℝ
ht : 0 < t
⊢ -π * (a ^ 2 + 1) * t ≤ -(π * a ^ 2) * t

Tactic:
nlinarith [pi_pos]

Result:
no goals

Proof state:
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
⊢ ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)

Tactic:
rcases eq_or_lt_of_le ha with rfl | ha'

Result:
case inl
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha : 0 ≤ 0
⊢ ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (0 ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            0 * rexp (-π * 0 ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)

case inr
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)

Proof state:
case inl
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha : 0 ≤ 0
⊢ ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (0 ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            0 * rexp (-π * 0 ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)

Tactic:
exact ⟨_, pi_pos, by simpa only [zero_pow two_ne_zero, zero_add, mul_one, zero_mul, zero_div,
  add_zero] using (isBigO_refl _ _).mul aux'⟩

Result:
no goals