awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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|))
have 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|))
Tactic: refine ⟨c, hc, B, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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))
have refine : Tendsto (α := ℂ) (β := ℝ) ((fun (x : ℂ) ↦ |x.im|) ∘ fun (x : ℂ) ↦ x * -I) (comap (β := ℝ) (fun (x : ℂ) ↦ |x.re|) atTop)
  atTop
Tactic: refine (tendsto_comap_iff.2 ?_).inf H.tendsto
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
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|))
⊢ 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|))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
⊢ ‖f z‖ ≤ C
have inl : ∀ (hz_re : 0 ≤ re 0) (hz_im : 0 ≤ im 0), ‖f 0‖ ≤ C
Tactic: rcases eq_or_ne z 0 with (rfl | hzne)
Cleared hypotheses: z, hz_re, hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
⊢ ‖f z‖ ≤ C
have inr : ∀ (hzne : z ≠ 0), ‖f z‖ ≤ C
Tactic: rcases eq_or_ne z 0 with (rfl | hzne)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
have refine : (log z).im ∈ Icc 0 (π / 2)
Tactic: refine ⟨log z, ?_, exp_log hzne⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
⊢ (log z).im ∈ Icc 0 (π / 2)
have rw : z.arg ∈ Icc 0 (π / 2)
Tactic: rw [log_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
⊢ ‖f z‖ ≤ C
have inr : ∀ (ζ : ℂ) (hζ : ζ.im ∈ Icc 0 (π / 2)) (hz_re : 0 ≤ (cexp ζ).re) (hz_im : 0 ≤ (cexp ζ).im) (hzne : cexp ζ ≠ 0),
  ‖f (cexp ζ)‖ ≤ C
Tactic: obtain ⟨ζ, hζ, rfl⟩ : ∃ ζ : ℂ, ζ.im ∈ Icc 0 (π / 2) ∧ exp ζ = z := by
    refine ⟨log z, ?_, exp_log hzne⟩
    rw [log_im]
    exact ⟨arg_nonneg_iff.2 hz_im, arg_le_pi_div_two_iff.2 (Or.inl hz_re)⟩
Cleared hypotheses: z, hz_re, hz_im, hzne
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
⊢ ‖f (cexp ζ)‖ ≤ C
have inr : ‖(f ∘ cexp) ζ‖ ≤ C
Tactic: change ‖(f ∘ exp) ζ‖ ≤ C
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ cexp z ∈ Ioi 0 ×ℂ Ioi 0
have rw : 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im
Tactic: rw [mem_reProdIm, exp_re, exp_im, mem_Ioi, mem_Ioi]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ -(π / 2) < z.im
have linarith : z.im ≤ -(π / 2) → 2 / 2 = 1
Tactic: linarith [hz.1, hz.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
linarith : z.im ≤ -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) < z.im
have linarith₁ : z.im ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hz.1, hz.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
linarith : z.im ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : z.im ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) < z.im
have linarith₂ : z.im ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith [hz.1, hz.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
linarith : z.im ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : z.im ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.im ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : z.im ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : z.im ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.im ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) < z.im
have linarith₆ : z.im ≤ -(π / 2) → 2 * z.im - -(1 * π) + 4 * (0 - z.im) + (2 * z.im - 1 * π) = 0
Tactic: linarith [hz.1, hz.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
linarith : z.im ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : z.im ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.im ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : z.im ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : z.im ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.im ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : z.im ≤ -(π / 2) → 2 * z.im - -(1 * π) + 4 * (0 - z.im) + (2 * z.im - 1 * π) = 0
⊢ -(π / 2) < z.im
have linarith₇ : z.im ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith [hz.1, hz.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im
have this : 0 < Real.cos z.im
Tactic: have : 0 < Real.cos z.im := Real.cos_pos_of_mem_Ioo ⟨by linarith [hz.1, hz.2], hz.2⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this : 0 < Real.cos z.im
⊢ 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im
have this₁ : 0 < Real.sin z.im
Tactic: have : 0 < Real.sin z.im :=
      Real.sin_pos_of_mem_Ioo ⟨hz.1, hz.2.trans (half_lt_self Real.pi_pos)⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this_1 : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im
have left : 0 < expR z.re * Real.cos z.im
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this_1 : 0 < Real.cos z.im
this : 0 < Real.sin z.im
left : 0 < expR z.re * Real.cos z.im
⊢ 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im
have right : 0 < expR z.re * Real.sin z.im
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
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
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
⊢ ‖(f ∘ cexp) ζ‖ ≤ C
have H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
Tactic: have H : MapsTo exp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0) := fun z hz ↦ by
    rw [mem_reProdIm, exp_re, exp_im, mem_Ioi, mem_Ioi]
    have : 0 < Real.cos z.im := Real.cos_pos_of_mem_Ioo ⟨by linarith [hz.1, hz.2], hz.2⟩
    have : 0 < Real.sin z.im :=
      Real.sin_pos_of_mem_Ioo ⟨hz.1, hz.2.trans (half_lt_self Real.pi_pos)⟩
    constructor <;> positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
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)
⊢ ‖(f ∘ cexp) ζ‖ ≤ C
have inr : ∃ c < π / (π / 2 - 0),
  ∃ (B : ℝ),
    IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
      expR (B * expR (c * |z.re|))
Tactic: refine horizontal_strip (hd.comp differentiable_exp.diffContOnCl H) ?_ ?_ ?_ hζ.1 hζ.2
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
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)
inr :
  ∃ c < π / (π / 2 - 0),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
⊢ ‖(f ∘ cexp) ζ‖ ≤ C
have inr₁ : ∀ (z : ℂ), z.im = 0 → ‖(f ∘ cexp) z‖ ≤ C
Tactic: refine horizontal_strip (hd.comp differentiable_exp.diffContOnCl H) ?_ ?_ ?_ hζ.1 hζ.2
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
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)
inr :
  ∃ c < π / (π / 2 - 0),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
inr₁ : ∀ (z : ℂ), z.im = 0 → ‖(f ∘ cexp) z‖ ≤ C
⊢ ‖(f ∘ cexp) ζ‖ ≤ C
have inr₂ : ∀ (z : ℂ), z.im = π / 2 → ‖(f ∘ cexp) z‖ ≤ C
Tactic: refine horizontal_strip (hd.comp differentiable_exp.diffContOnCl H) ?_ ?_ ?_ hζ.1 hζ.2
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
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 < π / (π / 2 - 0),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
have inr : ∃ c < 2,
  ∃ (B : ℝ),
    IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
      expR (B * expR (c * |z.re|))
Tactic: rw [sub_zero, div_div_cancel₀ Real.pi_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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
ζ : ℂ
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 < 2,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
have inr : ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
  (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
  ∃ c < 2,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
Tactic: rcases hB with ⟨c, hc, B, hO⟩
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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)
⊢ ∃ c < 2,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
have inr : IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
  expR (max B 0 * expR (c * |z.re|))
Tactic: refine ⟨c, hc, max B 0, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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)
⊢ IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
    expR (max B 0 * expR (c * |z.re|))
have inr : IsBigO (F := ℝ) (comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2)) ⊔ comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp)
  fun (z : ℂ) ↦ expR (max B 0 * expR (c * |z.re|))
Tactic: rw [← comap_comap, comap_abs_atTop, comap_sup, inf_sup_right]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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)
⊢ IsBigO (F := ℝ) (comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2)) ⊔ comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp)
    fun (z : ℂ) ↦ expR (max B 0 * expR (c * |z.re|))
have inr : IsBigO (F := ℝ) (comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦ expR (max B 0 * expR (c * |z.re|))
Tactic: refine IsBigO.sup ?_ <| (hO.comp_tendsto <| tendsto_exp_comap_re_atTop.inf H.tendsto).trans <|
      .of_norm_eventuallyLE ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
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 :
  IsBigO (F := ℝ) (comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
    expR (max B 0 * expR (c * |z.re|))
⊢ IsBigO (F := ℝ) (comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2)) ⊔ comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp)
    fun (z : ℂ) ↦ expR (max B 0 * expR (c * |z.re|))
have inr₁ : (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: refine IsBigO.sup ?_ <| (hO.comp_tendsto <| tendsto_exp_comap_re_atTop.inf H.tendsto).trans <|
      .of_norm_eventuallyLE ?_