-- 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
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))
⊢ c' r ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0

Tactic:
have aux : c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset := by
  simpa only [Multiset.mem_toFinset] using Multiset.mem_map_of_mem _ 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
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
⊢ c' r ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0

Proof state:
case h
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 > (eval 0 f).natAbs,
    Nat.Prime p →
      ∃ n,
        ¬↑p ∣ n ∧
          ∃ gp,
            gp.natDegree ≤ p * f.natDegree - 1 ∧
              ∀ {r : ℂ},
                r ∈ f.aroots ℂ →
                  ‖↑n * 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 p p_gt prime_p

Result:
case h
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
⊢ ∃ n,
    ¬↑p ∣ n ∧
      ∃ gp,
        gp.natDegree ≤ p * f.natDegree - 1 ∧
          ∀ {r : ℂ},
            r ∈ f.aroots ℂ →
              ‖↑n * 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.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
⊢ ‖↑(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:
rw [nsmul_eq_mul] at h

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
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‖ ≤
    (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.right.intro.intro.refine_1
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
⊢ gp.natDegree ≤ p * f.natDegree - 1

Tactic:
refine gp'_le.trans ((tsub_le_tsub_right natDegree_mul_le p).trans ?_)

Result:
case h.right.intro.intro.refine_1
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
⊢ (X ^ (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1