awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
push_cast :
  ((HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p + HMul.hMul (α := ℂ) (↑p : ℂ) (↑(eval 0 gp') : ℂ)) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HMul.hMul (α := ℂ) (↑p : ℂ) (↑(p - 1)! : ℂ) *
        HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
⊢ ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
⊢ ((HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p + HMul.hMul (α := ℂ) (↑p : ℂ) (↑(eval 0 gp') : ℂ)) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HMul.hMul (α := ℂ) (↑p : ℂ) (↑(p - 1)! : ℂ) *
        HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
⊢ ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)

Tactic:
have :
      (↑(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)) := by
    push_cast; ring
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
h₁ :
  ‖HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
        HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
          ((aeval r : (a : ℤ[X]) → ℂ)
              ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
            ℂ)‖ ≤
    HPow.hPow (α := ℝ)
      (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0)
      p
⊢ ‖(↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)‖ ≤
    HPow.hPow (α := ℝ)
        (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 [le_div_iff₀ (Nat.cast_pos.mpr (Nat.factorial_pos _) : (0 : ℝ) < _), ← norm_natCast,
    ← norm_mul, this, Nat.mul_factorial_pred prime_p.ne_zero, mul_sub, ← h]

Premises used: Iff.mpr, Nat.cast_pos, mul_sub, Complex.norm_natCast, norm_mul, Nat.Prime.ne_zero, le_div_iff₀, Nat.factorial_pos, Nat.mul_factorial_pred
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
simp :
  HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ)
      (((↑(p - 1)! : ℂ) * HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p + HMul.hMul (α := ℂ) (↑p ! : ℂ) (↑(eval 0 gp') : ℂ)) *
        cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)
⊢ HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
⊢ HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ)
      (((↑(p - 1)! : ℂ) * HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p + HMul.hMul (α := ℂ) (↑p ! : ℂ) (↑(eval 0 gp') : ℂ)) *
        cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
⊢ HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)

Tactic:
have :
      ↑(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)) := by
    simp; ring
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this_1 :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)
h₁ :
  ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) r‖ ≤
    HPow.hPow (α := ℝ)
      (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0)
      p
⊢ ‖HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
        HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
          ((aeval r : (a : ℤ[X]) → ℂ)
              ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
            ℂ)‖ ≤
    HPow.hPow (α := ℝ)
      (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0)
      p

Tactic:
rw [this, ← h', mul_comm, ← eq_intCast (algebraMap ℤ ℂ),
    ← aeval_algebraMap_apply_eq_algebraMap_eval, map_zero,
    aeval_sumIDeriv_eq_eval, aeval_sumIDeriv_eq_eval, ← P]

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, Algebra.algebraMap, map_zero, Int, eq_intCast, Polynomial.aeval_sumIDeriv_eq_eval, mul_comm, Complex, _private.0.LindemannWeierstrass.P
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this_1 :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)
⊢ ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) r‖ ≤
    HPow.hPow (α := ℝ)
      (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0)
      p

Tactic:
(Pp'_le r p prime_p.ne_zero).trans (pow_le_pow_left₀ (c'0 r) ?_ _)

Premises used: pow_le_pow_left₀, Nat.Prime.ne_zero, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this_1 :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)
h₁ :
  c' r ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0
⊢ ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) r‖ ≤
    HPow.hPow (α := ℝ)
      (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0)
      p

Tactic:
refine (Pp'_le r p prime_p.ne_zero).trans (pow_le_pow_left₀ (c'0 r) ?_ _)

Premises used: pow_le_pow_left₀, Nat.Prime.ne_zero, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this_1 :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)
⊢ c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset

Tactic:
simpa only [Multiset.mem_toFinset] using Multiset.mem_map_of_mem _ hr

Premises used: Multiset.mem_map_of_mem, Multiset.mem_toFinset
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) 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 : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this_1 :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)
⊢ c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset

Tactic:
have aux : c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset := by
    simpa only [Multiset.mem_toFinset] using Multiset.mem_map_of_mem _ hr