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 : ℝ
hd : d < π / 2 / b
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 ε)
⊢ DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))

Tactic:
replace hd : DiffContOnCl ℂ (fun w => g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b)) :=
    (hgd.diffContOnCl.smul hfd).mono inter_subset_right
-- 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))
⊢ ‖g ε z • f z‖ ≤ C

Tactic:
norm_le_of_forall_mem_frontier_norm_le ((isBounded_Ioo _ _).reProdIm (isBounded_Ioo _ _)) hd
      (fun w hw => _) _

Premises used: Bornology.IsBounded.reProdIm, Metric.isBounded_Ioo, Complex.norm_le_of_forall_mem_frontier_norm_le
-- 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))
h : ∀ (w : ℂ) (hw : w ∈ frontier (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))), ‖g ε w • f w‖ ≤ C
h₁ : z ∈ closure (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
⊢ ‖g ε z • f z‖ ≤ C

Tactic:
convert!
    norm_le_of_forall_mem_frontier_norm_le ((isBounded_Ioo _ _).reProdIm (isBounded_Ioo _ _)) hd
      (fun w hw => _) _

Premises used: Bornology.IsBounded.reProdIm, Metric.isBounded_Ioo, Complex.norm_le_of_forall_mem_frontier_norm_le
-- 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))
w : ℂ
hw : w ∈ frontier (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
⊢ w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)

Tactic:
rw [frontier_reProdIm, closure_Ioo (neg_lt_self hR₀).ne, frontier_Ioo hab, closure_Ioo hab.ne,
      frontier_Ioo (neg_lt_self hR₀)] at hw

Premises used: frontier_Ioo, neg_lt_self, Complex.frontier_reProdIm, LT.lt.ne, closure_Ioo
-- 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))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
pos : ∀ (him : w.im = a - b ∨ w.im = a + b), ‖g ε w • f w‖ ≤ C
neg : ∀ (him : ¬(w.im = a - b ∨ w.im = a + b)), ‖g ε w • f w‖ ≤ C
⊢ ‖g ε w • f w‖ ≤ C

Tactic:
by_cases him : w.im = a - b ∨ w.im = a + b

Premises used: Complex.im
-- 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))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : w.im = a - b ∨ w.im = a + b
pos : ‖g ε w‖ * ‖f w‖ ≤ 1 * C
⊢ ‖g ε w • f w‖ ≤ C

Tactic:
rw [norm_smul, ← one_mul C]

Premises used: norm_smul, one_mul
-- 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))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : w.im = a - b ∨ w.im = a + b
pos : ‖g ε w‖ ≤ 1
pos₁ : ‖f w‖ ≤ C
⊢ ‖g ε w‖ * ‖f w‖ ≤ 1 * C

Tactic:
gcongr
-- 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))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : w.im = a - b ∨ w.im = a + b
⊢ ‖g ε w‖ ≤ 1

Tactic:
hg₁ _ him
-- 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))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : w.im = a - b ∨ w.im = a + b
⊢ ‖f w‖ ≤ C

Tactic:
him.by_cases (hle_a _) (hle_b _)

Premises used: Or.by_cases
-- 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))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : w.im = a - b ∨ w.im = a + b
⊢ ‖g ε w‖ ≤ 1

Tactic:
exacts [hg₁ _ him, him.by_cases (hle_a _) (hle_b _)]

Premises used: Or.by_cases
-- 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))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : ¬(w.im = a - b ∨ w.im = a + b)
⊢ w ∈ {-R, R} ×ℂ Icc (a - b) (a + b)

Tactic:
replace hw : w ∈ {-R, R} ×ℂ Icc (a - b) (a + b) := hw.resolve_left fun h ↦ him h.2
-- 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))
w : ℂ
him : ¬(w.im = a - b ∨ w.im = a + b)
hw : w ∈ {-R, R} ×ℂ Icc (a - b) (a + b)
⊢ w.im = a - b ∨ w.im = a + b ∨ w.im ∈ Ioo (a - b) (a + b)

Tactic:
have hw' := eq_endpoints_or_mem_Ioo_of_mem_Icc hw.2
-- 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))
w : ℂ
him : ¬(w.im = a - b ∨ w.im = a + b)
hw : w ∈ {-R, R} ×ℂ Icc (a - b) (a + b)
hw' : w.im = a - b ∨ w.im = a + b ∨ w.im ∈ Ioo (a - b) (a + b)
⊢ (w.im = a - b ∨ w.im = a + b) ∨ w.im ∈ Ioo (a - b) (a + b)

Tactic:
rw [← or_assoc] at hw'

Premises used: or_assoc
-- 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))
w : ℂ
him : ¬(w.im = a - b ∨ w.im = a + b)
hw : w ∈ {-R, R} ×ℂ Icc (a - b) (a + b)
hw' : (w.im = a - b ∨ w.im = a + b) ∨ w.im ∈ Ioo (a - b) (a + b)
⊢ ‖g ε w • f w‖ ≤ C

Tactic:
hR _ ((abs_eq hR₀.le).2 hw.1.symm) (hw'.resolve_left him)

Premises used: Iff.mpr, abs_eq, LT.lt.le, Or.resolve_left, Or.symm, And.left
-- 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))
w : ℂ
him : ¬(w.im = a - b ∨ w.im = a + b)
hw : w ∈ {-R, R} ×ℂ Icc (a - b) (a + b)
hw' : (w.im = a - b ∨ w.im = a + b) ∨ w.im ∈ Ioo (a - b) (a + b)
⊢ ‖g ε w • f w‖ ≤ C

Tactic:
exact hR _ ((abs_eq hR₀.le).2 hw.1.symm) (hw'.resolve_left him)

Premises used: Iff.mpr, abs_eq, LT.lt.le, Or.resolve_left, Or.symm, And.left
-- 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))
h : z ∈ Icc (-R) R ×ℂ Icc (a - b) (a + b)
⊢ z ∈ closure (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))

Tactic:
rw [closure_reProdIm, closure_Ioo hab.ne, closure_Ioo (neg_lt_self hR₀).ne]

Premises used: Complex.closure_reProdIm, neg_lt_self, LT.lt.ne, closure_Ioo