-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma isBigO_atTop_F_int_zero_sub (a : UnitAddCircle) : ∃ p, 0 < p ∧
    (fun t ↦ F_int 0 a t - (if a = 0 then 1 else 0)) =O[atTop] fun t ↦ exp (-p * t)

Proof state:
a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico

Result:
case intro.intro
a : ℝ
ha : a ∈ Ico 0 1
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Proof state:
case intro.intro
a : ℝ
ha : a ∈ Ico 0 1
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_zero_sub ha.1

Result:
case intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
this :
  (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ p ⊓ q ≤ p

case intro.intro.intro.intro.intro.intro.refine_2.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
this :
  (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ p ⊓ q ≤ q

Tactic:
exacts [min_le_left .., min_le_right ..]

Result:
no goals

Proof state:
case intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_zero_sub (sub_nonneg.mpr ha.2.le)

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
refine ⟨_, lt_min hp hq, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
⊢ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-(p ⊓ q) * t)

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
simp_rw [AddCircle.coe_eq_zero_iff_of_mem_Ico ha]

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Proof state:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t => rexp (-q * t)
⊢ 1 - a ≠ 0

Tactic:
linarith [ha.2]

Result:
no goals

Proof state:
case h
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_nat 0 a t + F_nat 0 (1 - a) t - if a = 0 then 1 else 0) =
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
this :
  (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-(p ⊓ q) * t)

Tactic:
refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_)) <;>
apply isBigO_exp_neg_mul_of_le

Result:
case intro.intro.intro.intro.intro.intro.refine_1.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
this :
  (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ p ⊓ q ≤ p

case intro.intro.intro.intro.intro.intro.refine_2.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
this :
  (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ p ⊓ q ≤ q

Proof state:
case h
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_int 0 (↑a) t - if a = 0 then 1 else 0) = (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t

Tactic:
rw [F_int_eq_of_mem_Icc 0 (Ico_subset_Icc_self ha) ht]

Result:
case h
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_nat 0 a t + F_nat 0 (1 - a) t - if a = 0 then 1 else 0) =
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t