awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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
h :
  ∀ (r : ℂ),
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
        map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) →
      (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
        HSMul.hSMul (β := ℂ) p ! ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
r : ℂ
hr : r ∈ f.aroots ℂ
h₁ :
  HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
    map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ 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)! : ℝ)
have h₂ : ∀
  (h :
    (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
      HSMul.hSMul (β := ℂ) p ! ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)),
  ‖(↑(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: specialize h r _
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
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
h :
  ∀ (r : ℂ),
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
        map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) →
      (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
        HSMul.hSMul (β := ℂ) p ! ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
r : ℂ
hr : r ∈ f.aroots ℂ
⊢ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
    map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)
have hr₁ : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
Tactic: rw [mem_roots'] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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
h :
  ∀ (r : ℂ),
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
        map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) →
      (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
        HSMul.hSMul (β := ℂ) p ! ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
r : ℂ
hr : map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r
⊢ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
    map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)
have h₁ : HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
  map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1)) * map (algebraMap ℤ ℂ) f ^ p
Tactic: rw [Polynomial.map_mul, f.map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
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]) =
    HSMul.hSMul (β := ℂ) p ! ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
⊢ ‖(↑(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)! : ℝ)
have 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 : ℂ)
Tactic: rw [nsmul_eq_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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 : ℂ)
have 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 : ℂ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
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 : ℂ)‖ ≤
    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)! : ℝ)
have 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 : ℂ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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 : ℂ)
⊢ ‖(↑(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)! : ℝ)
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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]) :
        ℂ)
have 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]) : ℂ)
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
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]) :
            ℂ)‖ ≤
    HPow.hPow (α := ℝ)
      (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0)
      p
have 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]) : ℂ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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]) :
        ℂ)
⊢ ‖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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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
have h₁ : c' r ≤
  if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0
Tactic: refine (Pp'_le r p prime_p.ne_zero).trans (pow_le_pow_left₀ (c'0 r) ?_ _)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
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 ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0
have aux : 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