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

Proof state:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
⊢ ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
intro p hp

Result:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
⊢ ‖LindemannWeierstrass.P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Proof state:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p

Tactic:
let c₃ := max ‖s‖ 1

Result:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p

Proof state:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)

Tactic:
have le_max_one_pow {x : ℝ} : x ≤ max x 1 ^ p :=
  (max_cases x 1).elim (fun h ↦ h.1.symm ▸ le_self_pow₀ h.2 hp)
    fun h ↦ by rw [h.1, one_pow]; exact h.2.le

Result:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ (x ⊔ 1) ^ p
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)

Proof state:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p

Tactic:
let c₁ := max (Real.exp s.re) 1

Result:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p

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

Tactic:
obtain ⟨c', hc', h'⟩ := P_le_aux f s c hc

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

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

Tactic:
clear c hc

Result:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p

Proof state:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
⊢ ‖LindemannWeierstrass.P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
refine (h' p).trans ?_

Result:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Proof state:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
simp_rw [mul_pow]

Result:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)

Proof state:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
x : ℝ
h : x ⊔ 1 = 1 ∧ x < 1
⊢ x ≤ 1

Tactic:
exact h.2.le

Result:
no goals

Proof state:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
⊢ c₁ * (c₂ * c' * c₃) ≥ 0

Tactic:
positivity

Result:
no goals

Proof state:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ (x ⊔ 1) ^ p
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)

Tactic:
gcongr <;> exact le_max_one_pow

Result:
no goals

Proof state:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p

Tactic:
use c₁ * (c₂ * c' * c₃), by positivity

Result:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
⊢ ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Proof state:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
x : ℝ
h : x ⊔ 1 = 1 ∧ x < 1
⊢ x ≤ (x ⊔ 1) ^ p

Tactic:
rw [h.1, one_pow]

Result:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
c₃ : ℝ := ‖s‖ ⊔ 1
p : ℕ
hp : p ≠ 0
x : ℝ
h : x ⊔ 1 = 1 ∧ x < 1
⊢ x ≤ 1