simp [arg_eq_zero_iff]
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
⊢ (↑x).arg = 0
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
⊢ 0 ≤ x