-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem exp_polynomial_approx (f : ℤ[X]) (hf : f.eval 0 ≠ 0) :
    ∃ c,
      ∀ p > (eval 0 f).natAbs, p.Prime →
        ∃ n : ℤ, ¬ ↑p ∣ n ∧ ∃ gp : ℤ[X], gp.natDegree ≤ p * f.natDegree - 1 ∧
          ∀ {r : ℂ}, r ∈ f.aroots ℂ →
            ‖n • exp r - p • aeval r gp‖ ≤ c ^ p / (p - 1)!

Proof state:
case h.right.intro.intro.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1)) * map (algebraMap ℤ ℂ) f ^ p

Tactic:
exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd (dvd_iff_isRoot.mpr hr.2) _) _

Result:
no goals

Proof state:
case h.left
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
⊢ ¬↑p ∣ eval 0 f ^ p + ↑p * eval 0 gp'

Tactic:
rw [dvd_add_left (dvd_mul_right _ _)]

Result:
case h.left
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
⊢ ¬↑p ∣ eval 0 f ^ p

Proof state:
case h.right.intro.intro.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
⊢ ∀ {r : ℂ},
    r ∈ f.aroots ℂ →
      ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
        (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
            else 0) ^
            p /
          ↑(p - 1)!

Tactic:
intro r hr

Result:
case h.right.intro.intro.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : r ∈ f.aroots ℂ
⊢ ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
        else 0) ^
        p /
      ↑(p - 1)!

Proof state:
case h.left
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
h : ↑p ∣ eval 0 f ^ p
⊢ p ≤ (eval 0 f).natAbs

Tactic:
exact Nat.le_of_dvd (Int.natAbs_pos.mpr hf) (Int.natCast_dvd.mp (Int.Prime.dvd_pow' prime_p h))

Result:
no goals

Proof state:
case h.right.intro.intro.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h✝ : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
aux : c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset
h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty
⊢ c' r ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0

Tactic:
simpa only [h, ↓reduceDIte] using Finset.le_max' _ _ aux

Result:
no goals

Proof state:
case h.right.intro.intro.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)

Tactic:
rw [Polynomial.map_mul, f.map_pow]

Result:
case h.right.intro.intro.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1)) * map (algebraMap ℤ ℂ) f ^ p

Proof state:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
⊢ ((↑(eval 0 f) ^ p + ↑p * ↑(eval 0 gp')) * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑p * ↑(p - 1)! * (↑(eval 0 gp') * cexp r - (aeval r) gp)

Tactic:
ring

Result:
no goals