-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem exp_polynomial_approx_aux (f : ℤ[X]) (s : ℂ) :
    ∃ c ≥ 0,
      ∀ p ≠ 0, ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p

Tactic:
refine le_trans ?_ (pow_le_pow_left₀ (abs_nonneg _) h _)

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ^ p

Proof state:
case neg
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : 1 < x * ‖s‖
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p

Tactic:
exact pow_le_pow_right₀ hx1.le (Nat.sub_le _ _)

Result:
no goals

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |x * ‖s‖ ⊔ 1| ^ p

Tactic:
rw [← mul_pow, abs_of_nonneg (by positivity), max_def]

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p

Tactic:
specialize h (max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) (Set.mem_image_of_mem _ hx)

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p

Proof state:
case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1

Tactic:
exact pow_le_one₀ (mul_nonneg hx.1.le (norm_nonneg _)) hx1

Result:
no goals

Proof state:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ 0 ≤ x * ‖s‖ ⊔ 1

Tactic:
positivity

Result:
no goals

Proof state:
f : ℤ[X]
s : ℂ
⊢ Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)

Tactic:
have h :
  (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1 ⊆
    (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Icc 0 1 :=
  Set.image_subset _ Set.Ioc_subset_Icc_self

Result:
f : ℤ[X]
s : ℂ
h :
  (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1 ⊆
    (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Icc 0 1
⊢ Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ^ p

Tactic:
simp_rw [Polynomial.map_mul, Polynomial.map_pow, map_X, eval_mul, eval_pow, eval_X, norm_mul,
  Complex.norm_pow, real_smul, norm_mul, norm_real, ← eval₂_eq_eval_map, ← aeval_def, abs_mul,
  abs_norm, mul_pow, Real.norm_of_nonneg hx.1.le]

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) * ‖(aeval (↑x * s)) f‖ ^ p ≤ |x * ‖s‖ ⊔ 1| ^ p * ‖(aeval (↑x * s)) f‖ ^ p

Proof state:
case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1 ^ p

Tactic:
rw [one_pow]

Result:
case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1

Proof state:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
obtain ⟨c, h⟩ := this.exists_norm_le

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, ‖x‖ ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
refine P_le _ s c (fun p x hx => ?_)

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) * ‖(aeval (↑x * s)) f‖ ^ p ≤ |x * ‖s‖ ⊔ 1| ^ p * ‖(aeval (↑x * s)) f‖ ^ p

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (pow_nonneg (norm_nonneg _) _)

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |x * ‖s‖ ⊔ 1| ^ p

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
⊢ (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p

Tactic:
split_ifs with hx1

Result:
case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1 ^ p

case neg
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : ¬x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p