awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
inr :
  ∀ᶠ (b : ℝ) in atTop,
    ∀ (a : ℂ), a.re = b → a ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (a.re * c) ≤ max B 0 * expR (c * |a.re|)
⊢ (comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))).EventuallyLE (β := ℝ)
    (fun (x : ℂ) ↦ norm (E := ℝ) (((fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)) ∘ cexp) x)) fun (z : ℂ) ↦
    expR (max B 0 * expR (c * |z.re|))

Tactic:
simp only [EventuallyLE, eventually_inf_principal, eventually_comap, comp_apply,
        Real.norm_of_nonneg (Real.exp_pos _).le, norm_exp, ← Real.exp_mul, Real.exp_le_exp]

Premises used: Filter.eventually_inf_principal, Real.exp_mul, LT.lt.le, Real.exp_le_exp, Complex.norm_exp, Function.comp_apply, Filter.eventually_comap, Filter.EventuallyLE, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
h : z ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)
⊢ z ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)

Tactic:
_
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
h :
  ∀ (x : ℝ) (hx : 0 ≤ x) (z : ℂ) (hz : z.re = x),
    z ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)
⊢ ∀ᶠ (b : ℝ) in atTop,
    ∀ (a : ℂ), a.re = b → a ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (a.re * c) ≤ max B 0 * expR (c * |a.re|)

Tactic:
filter_upwards [eventually_ge_atTop 0] with x hx z hz _

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
h_1 : z ∈ im ⁻¹' Ioo 0 (π / 2)
h : B * expR (c * x) ≤ max B 0 * expR (c * x)
⊢ B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)

Tactic:
rw [hz, abs_of_nonneg hx, mul_comm _ c]

Premises used: mul_comm, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
h_1 : z ∈ im ⁻¹' Ioo 0 (π / 2)
h : B ≤ max B 0
⊢ B * expR (c * x) ≤ max B 0 * expR (c * x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
h : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ B ≤ max B 0

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ_1 : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = 0
⊢ ζ.im = 0

Tactic:
hζ
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ_1 : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = 0
inr : ∀ (ζ : ℝ), ‖(f ∘ cexp) (↑ζ : ℂ)‖ ≤ C
⊢ ‖(f ∘ cexp) ζ‖ ≤ C

Tactic:
lift ζ to ℝ using hζ
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℝ
inr : ‖f (↑(expR ζ) : ℂ)‖ ≤ C
⊢ ‖(f ∘ cexp) (↑ζ : ℂ)‖ ≤ C

Tactic:
rw [comp_apply, ← ofReal_exp]

Premises used: Complex.ofReal_exp, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℝ
⊢ ‖f (↑(expR ζ) : ℂ)‖ ≤ C

Tactic:
hre _ (Real.exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℝ
⊢ ‖f (↑(expR ζ) : ℂ)‖ ≤ C

Tactic:
exact hre _ (Real.exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ_1 : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
inr : ‖f ((↑(expR ζ.re) : ℂ) * I)‖ ≤ C
⊢ ‖(f ∘ cexp) ζ‖ ≤ C

Tactic:
rw [← re_add_im ζ, hζ, comp_apply, exp_add_mul_I, ← ofReal_cos, ← ofReal_sin,
      Real.cos_pi_div_two, Real.sin_pi_div_two, ofReal_zero, ofReal_one, one_mul, zero_add, ←
      ofReal_exp]

Premises used: Real.sin_pi_div_two, Complex.exp_add_mul_I, Real.cos_pi_div_two, Complex.ofReal_one, Complex.ofReal_exp, zero_add, Complex.ofReal_zero, Complex.ofReal_cos, Complex.ofReal_sin, Function.comp_apply, Complex.re_add_im, one_mul
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ_1 : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖f ((↑(expR ζ.re) : ℂ) * I)‖ ≤ C

Tactic:
him _ (Real.exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ_1 : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖f ((↑(expR ζ.re) : ℂ) * I)‖ ≤ C

Tactic:
exact him _ (Real.exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = 0
him : ∀ (x : ℝ), 0 ≤ x → f ((↑x : ℂ) * I) = 0
⊢ EqOn f 0 {z : ℂ | 0 ≤ z.re ∧ 0 ≤ z.im}

Tactic:
fun _z hz =>
  norm_le_zero_iff.1 <|
    quadrant_I hd hB (fun x hx => norm_le_zero_iff.2 <| hre x hx)
      (fun x hx => norm_le_zero_iff.2 <| him x hx) hz.1 hz.2

Premises used: Iff.mpr, Set.EqOn, And.right, And.left, norm_le_zero_iff, PhragmenLindelof.quadrant_I, Iff.mp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hdf : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hBf : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hdg : DiffContOnCl ℂ g (Ioi 0 ×ℂ Ioi 0)
hBg : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = g (↑x : ℂ)
him : ∀ (x : ℝ), 0 ≤ x → f ((↑x : ℂ) * I) = g ((↑x : ℂ) * I)
⊢ EqOn f g {z : ℂ | 0 ≤ z.re ∧ 0 ≤ z.im}

Tactic:
fun _z hz =>
  sub_eq_zero.1 <|
    eq_zero_on_quadrant_I (hdf.sub hdg) (isBigO_sub_exp_rpow hBf hBg)
      (fun x hx => sub_eq_zero.2 <| hre x hx) (fun x hx => sub_eq_zero.2 <| him x hx) hz

Premises used: Iff.mpr, sub_eq_zero, Set.EqOn, DiffContOnCl.sub, PhragmenLindelof.isBigO_sub_exp_rpow, Iff.mp, PhragmenLindelof.eq_zero_on_quadrant_I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ∃ (z' : ℂ), z' * I = z

Tactic:
⟨z / I, div_mul_cancel₀ _ I_ne_zero⟩

Premises used: div_mul_cancel₀, HDiv.hDiv, Complex.I_ne_zero, Exists.intro, Complex.I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
obtain : ∀ (z : ℂ) (hz_re : (z * I).re ≤ 0) (hz_im : 0 ≤ (z * I).im), ‖f (z * I)‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
obtain ⟨z, rfl⟩ : ∃ z', z' * I = z := ⟨z / I, div_mul_cancel₀ _ I_ne_zero⟩

Premises used: rfl, Complex.I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
⊢ 0 ≤ z.im

Tactic:
simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im

Premises used: neg_nonpos, Complex.mul_I_re, Complex.mul_I_im
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
hz_re₁ : 0 ≤ z.im
⊢ 0 ≤ z.re

Tactic:
simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im

Premises used: neg_nonpos, Complex.mul_I_re, Complex.mul_I_im
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
change : ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
⊢ ‖f (z * I)‖ ≤ C

Tactic:
change ‖(f ∘ (· * I)) z‖ ≤ C

Premises used: HMul.hMul, Function.comp, Complex.I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
w : ℂ
hw : w ∈ Ioi 0 ×ℂ Ioi 0
⊢ (fun (x : ℂ) ↦ x * I) w ∈ Iio 0 ×ℂ Ioi 0

Tactic:
simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using hw.symm

Premises used: Set.mem_Iio, neg_lt_zero, Complex.mul_I_re, And.symm, Complex.mem_reProdIm, Complex.mul_I_im
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
⊢ MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)

Tactic:
have H : MapsTo (· * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using hw.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
rcases :
  ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
    (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
    ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C

Tactic:
rcases hB with ⟨c, hc, B, hO⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C

Tactic:
quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him
    (fun x hx => ?_) hz_im hz_re

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, And.intro, PhragmenLindelof.quadrant_I, Exists.intro
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_1 : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ fun (x : ℂ) ↦ x * I) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_2 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ fun (x : ℂ) ↦ x * I) ((↑x : ℂ) * I)‖ ≤ C
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C

Tactic:
refine quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him
    (fun x hx => ?_) hz_im hz_re

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, And.intro, PhragmenLindelof.quadrant_I, Exists.intro
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ fun (x : ℂ) ↦ x * I) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
simpa only [Function.comp_def, norm_mul, norm_I, mul_one]
      using hO.comp_tendsto ((tendsto_mul_right_cobounded I_ne_zero).inf H.tendsto)

Premises used: Set.MapsTo.tendsto, Complex.I_ne_zero, norm_mul, Function.comp_def, Complex.norm_I, Asymptotics.IsBigO.comp_tendsto, mul_one, Filter.Tendsto.inf, Filter.tendsto_mul_right_cobounded
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
refine_2 : ‖f (↑(-x) : ℂ)‖ ≤ C
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) ((↑x : ℂ) * I)‖ ≤ C

Tactic:
rw [comp_apply, mul_assoc, I_mul_I, mul_neg_one, ← ofReal_neg]

Premises used: mul_assoc, Complex.ofReal_neg, Complex.I_mul_I, Function.comp_apply, mul_neg_one
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑(-x) : ℂ)‖ ≤ C

Tactic:
hre _ (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑(-x) : ℂ)‖ ≤ C

Tactic:
exact hre _ (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, f (↑x : ℂ) = 0
him : ∀ (x : ℝ), 0 ≤ x → f ((↑x : ℂ) * I) = 0
⊢ EqOn f 0 {z : ℂ | z.re ≤ 0 ∧ 0 ≤ z.im}

Tactic:
fun _z hz =>
  norm_le_zero_iff.1 <|
    quadrant_II hd hB (fun x hx => norm_le_zero_iff.2 <| hre x hx)
      (fun x hx => norm_le_zero_iff.2 <| him x hx) hz.1 hz.2

Premises used: Iff.mpr, Set.EqOn, PhragmenLindelof.quadrant_II, And.right, And.left, norm_le_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hdf : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hBf : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hdg : DiffContOnCl ℂ g (Iio 0 ×ℂ Ioi 0)
hBg : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, f (↑x : ℂ) = g (↑x : ℂ)
him : ∀ (x : ℝ), 0 ≤ x → f ((↑x : ℂ) * I) = g ((↑x : ℂ) * I)
⊢ EqOn f g {z : ℂ | z.re ≤ 0 ∧ 0 ≤ z.im}

Tactic:
fun _z hz =>
  sub_eq_zero.1 <| eq_zero_on_quadrant_II (hdf.sub hdg) (isBigO_sub_exp_rpow hBf hBg)
    (fun x hx => sub_eq_zero.2 <| hre x hx) (fun x hx => sub_eq_zero.2 <| him x hx) hz

Premises used: Iff.mpr, sub_eq_zero, Set.EqOn, PhragmenLindelof.eq_zero_on_quadrant_II, DiffContOnCl.sub, PhragmenLindelof.isBigO_sub_exp_rpow, Iff.mp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : z.im ≤ 0
⊢ ∃ (z' : ℂ), -z' = z

Tactic:
⟨-z, neg_neg z⟩

Premises used: neg_neg, Exists.intro, Neg.neg