-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem P_le_aux (f : ℕ → ℂ[X]) (s : ℂ) (c : ℝ)
    (hc : ∀ p : ℕ, ∀ x ∈ Set.Ioc (0 : ℝ) 1, ‖(f p).eval (x • s)‖ ≤ c ^ p) :
    ∃ c' ≥ 0, ∀ p : ℕ,
      ‖P (f p) s‖ ≤
        Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)

Proof state:
case h.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in 0 ..1, cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
rw [intervalIntegral.integral_of_le zero_le_one, ← mul_one (_ * _)]

Result:
case h.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in Set.Ioc 0 1, cexp (-(x • s)) * eval (x • s) (f p) ∂MeasureTheory.volume‖ ≤ Real.exp ‖s‖ * |c| ^ p * 1

Proof state:
case h.h.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ MeasureTheory.volume (Set.Ioc 0 1) < ⊤

Tactic:
rw [Real.volume_Ioc, sub_zero]

Result:
case h.h.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ENNReal.ofReal 1 < ⊤

Proof state:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ (-(x • s)).re ≤ ‖s‖

Tactic:
simp only [Set.mem_Ioc] at hx

Result:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ (-(x • s)).re ≤ ‖s‖

Proof state:
case h.h.convert_11
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ MeasurableSet (Set.Ioc 0 1)

Tactic:
exact measurableSet_Ioc

Result:
no goals

Proof state:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ (-(x • s)).re ≤ ‖s‖

Tactic:
apply (re_le_norm _).trans

Result:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ ‖-(x • s)‖ ≤ ‖s‖

Proof state:
case h.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in Set.Ioc 0 1, cexp (-(x • s)) * eval (x • s) (f p) ∂MeasureTheory.volume‖ ≤ Real.exp ‖s‖ * |c| ^ p * 1

Tactic:
convert MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ _ _

Result:
case h.e'_4.h.e'_6
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ 1 = (MeasureTheory.volume (Set.Ioc 0 1)).toReal

case h.h.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ MeasureTheory.volume (Set.Ioc 0 1) < ⊤

case h.h.convert_11
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ MeasurableSet (Set.Ioc 0 1)

case h.h.convert_12
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ∀ x ∈ Set.Ioc 0 1, ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Proof state:
case h.h.convert_12.h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p

Tactic:
rw [← abs_pow]

Result:
case h.h.convert_12.h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c ^ p|

Proof state:
case h.h.convert_12
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ∀ x ∈ Set.Ioc 0 1, ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
intro x hx

Result:
case h.h.convert_12
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Proof state:
case h.e'_4.h.e'_6
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ 1 = (MeasureTheory.volume (Set.Ioc 0 1)).toReal

Tactic:
rw [Real.volume_Ioc, sub_zero, ENNReal.toReal_ofReal zero_le_one]

Result:
no goals

Proof state:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)

Tactic:
refine ⟨|c|, abs_nonneg _, fun p => ?_⟩

Result:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Proof state:
case h.h.convert_12
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
gcongr

Result:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ (-(x • s)).re ≤ ‖s‖

case h.h.convert_12.h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p

Proof state:
case h.h.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ENNReal.ofReal 1 < ⊤

Tactic:
exact ENNReal.ofReal_lt_top

Result:
no goals

Proof state:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
rw [P_eq_integral_exp_mul_eval (f p) s, mul_comm s, norm_mul, norm_mul, norm_exp]

Result:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ Real.exp s.re * (‖∫ (x : ℝ) in 0 ..1, cexp (-(x • s)) * eval (x • s) (f p)‖ * ‖s‖) ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Proof state:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ x * ‖s‖ ≤ ‖s‖

Tactic:
exact mul_le_of_le_one_left (norm_nonneg _) hx.2

Result:
no goals

Proof state:
case h.h.convert_12.h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c ^ p|

Tactic:
exact (hc p x hx).trans (le_abs_self _)

Result:
no goals

Proof state:
case h.h.convert_12
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
rw [norm_mul, norm_exp]

Result:
case h.h.convert_12
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Proof state:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ Real.exp s.re * (‖∫ (x : ℝ) in 0 ..1, cexp (-(x • s)) * eval (x • s) (f p)‖ * ‖s‖) ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
gcongr

Result:
case h.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in 0 ..1, cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Proof state:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ ‖-(x • s)‖ ≤ ‖s‖

Tactic:
rw [norm_neg, norm_smul, Real.norm_of_nonneg hx.1.le]

Result:
case h.h.convert_12.h₁.h
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ x * ‖s‖ ≤ ‖s‖