-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem isLittleO_log_norm_re (hl : IsExpCmpFilter l) : (fun z => Real.log ‖z‖) =o[l] re :=
  calc
    (fun z => Real.log ‖z‖) =O[l] fun z => Real.log (√2) + Real.log (max z.re |z.im|) :=
      .of_norm_eventuallyLE <|
        (hl.tendsto_re.eventually_ge_atTop 1).mono fun z hz => by
          have h2 : 0 < √2

Proof state:
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Tactic:
rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
  ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
  abs_of_pos (one_pos.trans h₁)]

Result:
no goals

Proof state:
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Tactic:
norm_cast at *

Result:
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ᶠ (x : ℂ) in l, ↑n * ‖Real.log (x.re ⊔ |x.im|)‖ ≤ ‖x.re‖

Tactic:
filter_upwards [isLittleO_iff_nat_mul_le'.1 hl.isLittleO_log_re_re n,
  hl.abs_im_pow_eventuallyLE_exp_re n,
  hl.tendsto_re.eventually_gt_atTop 1] with z hre him h₁

Result:
case h
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ (fun x => ‖Real.log ‖x‖‖) z ≤ (fun z => Real.log √2 + Real.log (z.re ⊔ |z.im|)) z

Tactic:
simp only [Real.norm_of_nonneg (Real.log_nonneg hz')]

Result:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (z.re ⊔ |z.im|)

Proof state:
case h.inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Tactic:
rwa [max_eq_left hle]

Result:
no goals

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ ‖z‖ ≤ √2 * (|z.re| ⊔ |z.im|)

case h
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ 0 < ‖z‖

case h₁
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ 0 < √2 * (z.re ⊔ |z.im|)

case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ √2 ≠ 0

case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ z.re ⊔ |z.im| ≠ 0

Tactic:
exacts [norm_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne']

Result:
no goals

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ 0 < √2

Tactic:
simp

Result:
no goals

Proof state:
case h
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Tactic:
rcases le_total |z.im| z.re with hle | hle

Result:
case h.inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ (fun x => ‖Real.log ‖x‖‖) z ≤ (fun z => Real.log √2 + Real.log (z.re ⊔ |z.im|)) z

Tactic:
have h2 : 0 < √2 := by simp

Result:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
⊢ (fun x => ‖Real.log ‖x‖‖) z ≤ (fun z => Real.log √2 + Real.log (z.re ⊔ |z.im|)) z

Proof state:
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Tactic:
have H : 1 < |z.im| := h₁.trans_le hle

Result:
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (z.re ⊔ |z.im|)‖ ≤ ‖z.re‖

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ Real.log ‖z‖ ≤ Real.log √2 + Real.log (z.re ⊔ |z.im|)

Tactic:
rw [← Real.log_mul, Real.log_le_log_iff, ← abs_of_nonneg (le_trans zero_le_one hz)]

Result:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ ‖z‖ ≤ √2 * (|z.re| ⊔ |z.im|)

case h
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ 0 < ‖z‖

case h₁
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ 0 < √2 * (z.re ⊔ |z.im|)

case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ √2 ≠ 0

case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ z.re ⊔ |z.im| ≠ 0

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
⊢ (fun x => ‖Real.log ‖x‖‖) z ≤ (fun z => Real.log √2 + Real.log (z.re ⊔ |z.im|)) z

Tactic:
have hz' : 1 ≤ ‖z‖ := hz.trans (re_le_norm z)

Result:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
⊢ (fun x => ‖Real.log ‖x‖‖) z ≤ (fun z => Real.log √2 + Real.log (z.re ⊔ |z.im|)) z

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
⊢ (fun x => ‖Real.log ‖x‖‖) z ≤ (fun z => Real.log √2 + Real.log (z.re ⊔ |z.im|)) z

Tactic:
have hm₀ : 0 < max z.re |z.im| := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)

Result:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < z.re ⊔ |z.im|
⊢ (fun x => ‖Real.log ‖x‖‖) z ≤ (fun z => Real.log √2 + Real.log (z.re ⊔ |z.im|)) z