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_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
R : ℝ
hzR : |z.re| < R
hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C
hR₀ : 0 < R
hgd : Differentiable ℂ (g ε)
hd : DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
⊢ z ∈ Icc (-R) R ×ℂ Icc (a - b) (a + b)

Tactic:
⟨abs_le.1 hzR.le, ⟨hza.le, hzb.le⟩⟩

Premises used: Set.Mem, abs_le, setOf, LT.lt.le, Set.inter, Complex.reProdIm, And.intro, Iff.mp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
R : ℝ
hzR : |z.re| < R
hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C
hR₀ : 0 < R
hgd : Differentiable ℂ (g ε)
hd : DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
⊢ z ∈ Icc (-R) R ×ℂ Icc (a - b) (a + b)

Tactic:
exact ⟨abs_le.1 hzR.le, ⟨hza.le, hzb.le⟩⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
ha : ∀ (z : ℂ), z.im = a → f z = 0
hb : ∀ (z : ℂ), z.im = b → f z = 0
⊢ EqOn f 0 (im ⁻¹' Icc a b)

Tactic:
fun _z hz =>
  norm_le_zero_iff.1 <| horizontal_strip hd hB (fun z hz => (ha z hz).symm ▸ norm_zero.le)
    (fun z hz => (hb z hz).symm ▸ norm_zero.le) hz.1 hz.2

Premises used: norm_zero, Eq.rec, Eq.le, Set.EqOn, And.right, And.left, norm_le_zero_iff, Iff.mp, PhragmenLindelof.horizontal_strip, Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f g : ℂ → E
hdf : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hBf :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hdg : DiffContOnCl ℂ g (im ⁻¹' Ioo a b)
hBg :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) g fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
ha : ∀ (z : ℂ), z.im = a → f z = g z
hb : ∀ (z : ℂ), z.im = b → f z = g z
⊢ EqOn f g (im ⁻¹' Icc a b)

Tactic:
fun _z hz =>
  sub_eq_zero.1 (eq_zero_on_horizontal_strip (hdf.sub hdg) (isBigO_sub_exp_exp hBf hBg)
    (fun w hw => sub_eq_zero.2 (ha w hw)) (fun w hw => sub_eq_zero.2 (hb w hw)) hz)

Premises used: Iff.mpr, sub_eq_zero, PhragmenLindelof.eq_zero_on_horizontal_strip, Set.EqOn, PhragmenLindelof.isBigO_sub_exp_exp, DiffContOnCl.sub, Iff.mp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
this : ‖f (z * I * -I)‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
simpa [mul_assoc] using this

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
suffices : ‖f (z * I * -I)‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
suffices ‖f (z * I * -I)‖ ≤ C by simpa [mul_assoc] using this
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z_1 : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z_1.re
hzb : z_1.re ≤ b
z : ℂ
hz : z ∈ im ⁻¹' Ioo a b
⊢ (fun (x : ℂ) ↦ x * -I) z ∈ re ⁻¹' Ioo a b

Tactic:
simpa using hz
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
⊢ MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)

Tactic:
have H : MapsTo (· * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b) := fun z hz ↦ by simpa using hz
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ ‖f (z * I * -I)‖ ≤ C

Tactic:
horizontal_strip (f := fun z ↦ f (z * -I))
    (hfd.comp (differentiable_id.mul_const _).diffContOnCl H) ?_ (fun z hz => hle_a _ ?_)
    (fun z hz => hle_b _ ?_) ?_ ?_

Premises used: Differentiable.diffContOnCl, HMul.hMul, DiffContOnCl.comp, PhragmenLindelof.horizontal_strip, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
refine_1 :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (fun (z : ℂ) ↦ f (z * -I))
        fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
refine_2 : ∀ (z : ℂ) (hz : z.im = a), (z * -I).re = a
refine_3 : ∀ (z : ℂ) (hz : z.im = b), (z * -I).re = b
refine_4 : a ≤ (z * I).im
refine_5 : (z * I).im ≤ b
⊢ ‖f (z * I * -I)‖ ≤ C

Tactic:
refine horizontal_strip (f := fun z ↦ f (z * -I))
    (hfd.comp (differentiable_id.mul_const _).diffContOnCl H) ?_ (fun z hz => hle_a _ ?_)
    (fun z hz => hle_b _ ?_) ?_ ?_

Premises used: Differentiable.diffContOnCl, HMul.hMul, DiffContOnCl.comp, PhragmenLindelof.horizontal_strip, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
refine_1 :
  ∀ (c : ℝ) (hc : c < π / (b - a)) (B : ℝ)
    (hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))),
    ∃ c < π / (b - a),
      ∃ (B : ℝ),
        IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (fun (z : ℂ) ↦ f (z * -I))
          fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
⊢ ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (fun (z : ℂ) ↦ f (z * -I))
        fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))

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
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
⊢ ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (fun (z : ℂ) ↦ f (z * -I))
        fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))

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
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
refine_1 :
  IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (fun (z : ℂ) ↦ f (z * -I))
    fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
⊢ ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (fun (z : ℂ) ↦ f (z * -I))
        fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))

Tactic:
refine ⟨c, hc, B, ?_⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
⊢ Tendsto (fun (x : ℂ) ↦ x * -I) (comap (β := ℝ) (fun (x : ℂ) ↦ |x.re|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b))
    (comap (β := ℝ) (fun (x : ℂ) ↦ |x.im|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b))

Tactic:
(tendsto_comap_iff.2 ?_).inf H.tendsto

Premises used: Iff.mpr, Set.MapsTo.tendsto, Filter.tendsto_comap_iff, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
refine :
  Tendsto (α := ℂ) (β := ℝ) ((fun (x : ℂ) ↦ |x.im|) ∘ fun (x : ℂ) ↦ x * -I)
    (comap (β := ℝ) (fun (x : ℂ) ↦ |x.re|) atTop) atTop
⊢ Tendsto (fun (x : ℂ) ↦ x * -I) (comap (β := ℝ) (fun (x : ℂ) ↦ |x.re|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b))
    (comap (β := ℝ) (fun (x : ℂ) ↦ |x.im|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b))

Tactic:
refine (tendsto_comap_iff.2 ?_).inf H.tendsto

Premises used: Iff.mpr, Set.MapsTo.tendsto, Filter.tendsto_comap_iff, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
⊢ Tendsto (α := ℂ) (β := ℝ) ((fun (x : ℂ) ↦ |x.im|) ∘ fun (x : ℂ) ↦ x * -I)
    (comap (β := ℝ) (fun (x : ℂ) ↦ |x.re|) atTop) atTop

Tactic:
simpa [Function.comp_def] using tendsto_comap

Premises used: Filter.tendsto_comap, Function.comp_def
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
⊢ Tendsto (fun (x : ℂ) ↦ x * -I) (comap (β := ℝ) (fun (x : ℂ) ↦ |x.re|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b))
    (comap (β := ℝ) (fun (x : ℂ) ↦ |x.im|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b))

Tactic:
have : Tendsto (· * -I) (comap (|re ·|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b))
        (comap (|im ·|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) := by
      refine (tendsto_comap_iff.2 ?_).inf H.tendsto
      simpa [Function.comp_def] using tendsto_comap
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
this :
  Tendsto (fun (x : ℂ) ↦ x * -I) (comap (β := ℝ) (fun (x : ℂ) ↦ |x.re|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b))
    (comap (β := ℝ) (fun (x : ℂ) ↦ |x.im|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b))
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) (fun (z : ℂ) ↦ f (z * -I))
    fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))

Tactic:
simpa [Function.comp_def] using hO.comp_tendsto this

Premises used: Function.comp_def, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z_1 : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z_1.re
hzb : z_1.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = a
⊢ (z * -I).re = a

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z_1 : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z_1.re
hzb : z_1.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = b
⊢ (z * -I).re = b

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ a ≤ (z * I).im

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun (x : ℂ) ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ (z * I).im ≤ b

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
ha : ∀ (z : ℂ), z.re = a → f z = 0
hb : ∀ (z : ℂ), z.re = b → f z = 0
⊢ EqOn f 0 (re ⁻¹' Icc a b)

Tactic:
fun _z hz =>
  norm_le_zero_iff.1 <| vertical_strip hd hB (fun z hz => (ha z hz).symm ▸ norm_zero.le)
    (fun z hz => (hb z hz).symm ▸ norm_zero.le) hz.1 hz.2

Premises used: norm_zero, Eq.rec, PhragmenLindelof.vertical_strip, Eq.le, Set.EqOn, And.right, And.left, norm_le_zero_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f g : ℂ → E
hdf : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hBf :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
hdg : DiffContOnCl ℂ g (re ⁻¹' Ioo a b)
hBg :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)) g fun (z : ℂ) ↦ expR (B * expR (c * |z.im|))
ha : ∀ (z : ℂ), z.re = a → f z = g z
hb : ∀ (z : ℂ), z.re = b → f z = g z
⊢ EqOn f g (re ⁻¹' Icc a b)

Tactic:
fun _z hz =>
  sub_eq_zero.1 (eq_zero_on_vertical_strip (hdf.sub hdg) (isBigO_sub_exp_exp hBf hBg)
    (fun w hw => sub_eq_zero.2 (ha w hw)) (fun w hw => sub_eq_zero.2 (hb w hw)) hz)

Premises used: Iff.mpr, sub_eq_zero, PhragmenLindelof.eq_zero_on_vertical_strip, Set.EqOn, PhragmenLindelof.isBigO_sub_exp_exp, DiffContOnCl.sub, 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 (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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
inl : ∀ (hz_re : 0 ≤ re 0) (hz_im : 0 ≤ im 0), ‖f 0‖ ≤ C
inr : ∀ (hzne : z ≠ 0), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
rcases eq_or_ne z 0 with (rfl | hzne)

Premises used: eq_or_ne, OfNat.ofNat, 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 ×ℂ 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
hz_re : 0 ≤ re 0
hz_im : 0 ≤ im 0
⊢ ‖f 0‖ ≤ C

Tactic:
hre 0 le_rfl

Premises used: le_rfl, 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)
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
hz_re : 0 ≤ re 0
hz_im : 0 ≤ im 0
⊢ ‖f 0‖ ≤ C

Tactic:
exact hre 0 le_rfl

Premises used: le_rfl, OfNat.ofNat
-- 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 ×ℂ 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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
⊢ ∃ (ζ : ℂ), ζ.im ∈ Icc 0 (π / 2) ∧ cexp ζ = z

Tactic:
⟨log z, ?_, exp_log hzne⟩

Premises used: Complex.log, And.intro, Exists.intro, Complex.exp_log
-- 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 ×ℂ 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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
refine : (log z).im ∈ Icc 0 (π / 2)
⊢ ∃ (ζ : ℂ), ζ.im ∈ Icc 0 (π / 2) ∧ cexp ζ = z

Tactic:
refine ⟨log z, ?_, exp_log hzne⟩
-- 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 ×ℂ 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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
rw : z.arg ∈ Icc 0 (π / 2)
⊢ (log z).im ∈ Icc 0 (π / 2)

Tactic:
rw [log_im]

Premises used: Complex.log_im
-- 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 ×ℂ 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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
⊢ z.arg ∈ Icc 0 (π / 2)

Tactic:
⟨arg_nonneg_iff.2 hz_im, arg_le_pi_div_two_iff.2 (Or.inl hz_re)⟩

Premises used: Iff.mpr, Complex.arg_le_pi_div_two_iff, Set.Mem, setOf, Set.Icc, And.intro, Or.inl, Complex.arg_nonneg_iff