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
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
obtain : ∀ (z : ℂ) (hz_re : (-z).re ≤ 0) (hz_im : (-z).im ≤ 0), ‖f (-z)‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
obtain ⟨z, rfl⟩ : ∃ z', -z' = z := ⟨-z, neg_neg z⟩

Premises used: rfl
-- 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 ×ℂ 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
z : ℂ
hz_re : (-z).re ≤ 0
hz_im : (-z).im ≤ 0
⊢ 0 ≤ z.re

Tactic:
simp only [neg_re, neg_im, neg_nonpos] at hz_re hz_im

Premises used: neg_nonpos, Complex.neg_re, Complex.neg_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 ×ℂ 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
z : ℂ
hz_re : (-z).re ≤ 0
hz_im : (-z).im ≤ 0
hz_re₁ : 0 ≤ z.re
⊢ 0 ≤ z.im

Tactic:
simp only [neg_re, neg_im, neg_nonpos] at hz_re hz_im

Premises used: neg_nonpos, Complex.neg_re, Complex.neg_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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
change : ‖(f ∘ Neg.neg) z‖ ≤ C
⊢ ‖f (-z)‖ ≤ C

Tactic:
change ‖(f ∘ Neg.neg) z‖ ≤ C

Premises used: Function.comp, Neg.neg
-- 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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
w : ℂ
hw : w ∈ Ioi 0 ×ℂ Ioi 0
⊢ -w ∈ Iio 0 ×ℂ Iio 0

Tactic:
simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, mem_Iio] using hw

Premises used: Set.mem_Iio, neg_lt_zero, Complex.neg_re, Complex.mem_reProdIm, Complex.neg_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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
⊢ MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)

Tactic:
have H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0) := by
    intro w hw
    simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, mem_Iio] using hw
-- 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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C

Tactic:
quadrant_I (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_)
      hz_re hz_im

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, PhragmenLindelof.quadrant_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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_2 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C
refine_3 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ Neg.neg) ((↑x : ℂ) * I)‖ ≤ C
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C

Tactic:
refine
    quadrant_I (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_)
      hz_re hz_im

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, PhragmenLindelof.quadrant_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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
refine_1 :
  ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
    (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
    ∃ c < 2,
      ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖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 ×ℂ Iio 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
⟨c, hc, B, ?_⟩

Premises used: And.intro, 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 ×ℂ Iio 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_1 : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
refine ⟨c, hc, B, ?_⟩
-- 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 ×ℂ Iio 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
simpa only [Function.comp_def, norm_neg]
      using hO.comp_tendsto (Filter.tendsto_neg_cobounded.inf H.tendsto)

Premises used: Set.MapsTo.tendsto, Function.comp_def, norm_neg, Asymptotics.IsBigO.comp_tendsto, Filter.Tendsto.inf, Filter.tendsto_neg_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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
refine_2 : ‖f (↑(-x) : ℂ)‖ ≤ C
⊢ ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C

Tactic:
rw [comp_apply, ← ofReal_neg]

Premises used: Complex.ofReal_neg, 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 (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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑(-x) : ℂ)‖ ≤ C

Tactic:
hre (-x) (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos, Neg.neg
-- 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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑(-x) : ℂ)‖ ≤ C

Tactic:
exact hre (-x) (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos, Neg.neg
-- 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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
refine_3 : ‖f ((↑(-x) : ℂ) * I)‖ ≤ C
⊢ ‖(f ∘ Neg.neg) ((↑x : ℂ) * I)‖ ≤ C

Tactic:
rw [comp_apply, ← neg_mul, ← ofReal_neg]

Premises used: Complex.ofReal_neg, Function.comp_apply, neg_mul
-- 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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f ((↑(-x) : ℂ) * I)‖ ≤ C

Tactic:
him (-x) (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos, Neg.neg
-- 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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f ((↑(-x) : ℂ) * I)‖ ≤ C

Tactic:
exact him (-x) (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos, Neg.neg
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
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 : ℂ) = 0
him : ∀ x ≤ 0, f ((↑x : ℂ) * I) = 0
⊢ EqOn f 0 {z : ℂ | z.re ≤ 0 ∧ z.im ≤ 0}

Tactic:
fun _z hz =>
  norm_le_zero_iff.1 <| quadrant_III 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, PhragmenLindelof.quadrant_III, Set.EqOn, 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 ×ℂ Iio 0)
hBf : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hdg : DiffContOnCl ℂ g (Iio 0 ×ℂ Iio 0)
hBg : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, f (↑x : ℂ) = g (↑x : ℂ)
him : ∀ x ≤ 0, f ((↑x : ℂ) * I) = g ((↑x : ℂ) * I)
⊢ EqOn f g {z : ℂ | z.re ≤ 0 ∧ z.im ≤ 0}

Tactic:
fun _z hz =>
  sub_eq_zero.1 <| eq_zero_on_quadrant_III (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_III
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_re : 0 ≤ z.re
hz_im : z.im ≤ 0
⊢ ∃ (z' : ℂ), -z' = z

Tactic:
⟨-z, neg_neg z⟩

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

Tactic:
obtain ⟨z, rfl⟩ : ∃ z', -z' = z := ⟨-z, neg_neg z⟩

Premises used: rfl
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ (-z).re
hz_im : (-z).im ≤ 0
⊢ z.re ≤ 0

Tactic:
simp only [neg_re, neg_im, neg_nonpos, neg_nonneg] at hz_re hz_im

Premises used: neg_nonpos, neg_nonneg, Complex.neg_re, Complex.neg_im
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ (-z).re
hz_im : (-z).im ≤ 0
hz_re₁ : z.re ≤ 0
⊢ 0 ≤ z.im

Tactic:
simp only [neg_re, neg_im, neg_nonpos, neg_nonneg] at hz_re hz_im

Premises used: neg_nonpos, neg_nonneg, Complex.neg_re, Complex.neg_im
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
change : ‖(f ∘ Neg.neg) z‖ ≤ C
⊢ ‖f (-z)‖ ≤ C

Tactic:
change ‖(f ∘ Neg.neg) z‖ ≤ C

Premises used: Function.comp, Neg.neg
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
w : ℂ
hw : w ∈ Iio 0 ×ℂ Ioi 0
⊢ -w ∈ Ioi 0 ×ℂ Iio 0

Tactic:
simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, neg_pos, mem_Ioi, mem_Iio] using hw

Premises used: Set.mem_Iio, neg_pos, Set.mem_Ioi, neg_lt_zero, Complex.neg_re, Complex.mem_reProdIm, Complex.neg_im
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)

Tactic:
have H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, neg_pos, mem_Ioi, mem_Iio] using hw
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C

Tactic:
quadrant_II
    (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_) hz_re hz_im

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, PhragmenLindelof.quadrant_II
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_2 : ∀ (x : ℝ) (hx : x ≤ 0), ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C
refine_3 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ Neg.neg) ((↑x : ℂ) * I)‖ ≤ C
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C

Tactic:
refine quadrant_II
    (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_) hz_re hz_im

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, PhragmenLindelof.quadrant_II
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
refine_1 :
  ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
    (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
    ∃ c < 2,
      ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖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 (Ioi 0 ×ℂ Iio 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
⟨c, hc, B, ?_⟩

Premises used: And.intro, 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 (Ioi 0 ×ℂ Iio 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_1 : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
refine ⟨c, hc, B, ?_⟩
-- 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 ×ℂ Iio 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
simpa only [Function.comp_def, norm_neg]
      using hO.comp_tendsto (Filter.tendsto_neg_cobounded.inf H.tendsto)

Premises used: Set.MapsTo.tendsto, Function.comp_def, norm_neg, Asymptotics.IsBigO.comp_tendsto, Filter.Tendsto.inf, Filter.tendsto_neg_cobounded
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : x ≤ 0
refine_2 : ‖f (↑(-x) : ℂ)‖ ≤ C
⊢ ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C

Tactic:
rw [comp_apply, ← ofReal_neg]

Premises used: Complex.ofReal_neg, 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : x ≤ 0
⊢ ‖f (↑(-x) : ℂ)‖ ≤ C

Tactic:
hre (-x) (neg_nonneg.2 hx)

Premises used: Iff.mpr, neg_nonneg, Neg.neg
-- 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 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : x ≤ 0
⊢ ‖f (↑(-x) : ℂ)‖ ≤ C

Tactic:
exact hre (-x) (neg_nonneg.2 hx)

Premises used: Iff.mpr, neg_nonneg, Neg.neg