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'
h :
  ¬(↑p : ℤ) ∣ eval 0 f ^ p + (↑p : ℤ) * eval 0 gp' ∧
    ∃ (gp : ℤ[X]),
      gp.natDegree ≤ p * f.natDegree - 1 ∧
        ∀ {r : ℂ},
          r ∈ f.aroots ℂ →
            ‖(↑(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)! : ℝ)
⊢ ∃ (n : ℤ),
    ¬(↑p : ℤ) ∣ n ∧
      ∃ (gp : ℤ[X]),
        gp.natDegree ≤ p * f.natDegree - 1 ∧
          ∀ {r : ℂ},
            r ∈ f.aroots ℂ →
              ‖(↑n : ℂ) * 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:
use f.eval 0 ^ p + p * gp'.eval 0

Premises used: Polynomial.eval, OfNat.ofNat
-- 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'
h : ¬(↑p : ℤ) ∣ eval 0 f ^ p + (↑p : ℤ) * eval 0 gp'
h₁ :
  ∃ (gp : ℤ[X]),
    gp.natDegree ≤ p * f.natDegree - 1 ∧
      ∀ {r : ℂ},
        r ∈ f.aroots ℂ →
          ‖(↑(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)! : ℝ)
⊢ ¬(↑p : ℤ) ∣ eval 0 f ^ p + (↑p : ℤ) * eval 0 gp' ∧
    ∃ (gp : ℤ[X]),
      gp.natDegree ≤ p * f.natDegree - 1 ∧
        ∀ {r : ℂ},
          r ∈ f.aroots ℂ →
            ‖(↑(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:
constructor
-- 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'
h : ¬(↑p : ℤ) ∣ eval 0 f ^ p
⊢ ¬(↑p : ℤ) ∣ eval 0 f ^ p + (↑p : ℤ) * eval 0 gp'

Tactic:
rw [dvd_add_left (dvd_mul_right _ _)]

Premises used: dvd_add_left, dvd_mul_right
-- 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'
h : ∀ (h : (↑p : ℤ) ∣ eval 0 f ^ p), p ≤ (eval 0 f).natAbs
⊢ ¬(↑p : ℤ) ∣ eval 0 f ^ p

Tactic:
contrapose! p_gt with h
-- 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 : ℕ
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'
h : (↑p : ℤ) ∣ eval 0 f ^ p
⊢ p ≤ (eval 0 f).natAbs

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

Premises used: Iff.mpr, Int.natAbs_pos, Iff.mp, Int.natCast_dvd, Nat.le_of_dvd, Int.Prime.dvd_pow'
-- 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 : ℕ
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'
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))

Premises used: Iff.mpr, Int.natAbs_pos, Iff.mp, Int.natCast_dvd, Nat.le_of_dvd, Int.Prime.dvd_pow'
-- 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'
h :
  ∀ (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 : ℂ)),
    ∃ (gp : ℤ[X]),
      gp.natDegree ≤ p * f.natDegree - 1 ∧
        ∀ {r : ℂ},
          r ∈ f.aroots ℂ →
            ‖(↑(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)! : ℝ)
⊢ ∃ (gp : ℤ[X]),
    gp.natDegree ≤ p * f.natDegree - 1 ∧
      ∀ {r : ℂ},
        r ∈ f.aroots ℂ →
          ‖(↑(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:
obtain ⟨gp, gp'_le, h⟩ := aeval_sumIDeriv ℂ (X ^ (p - 1) * f ^ p) p

Premises used: HMul.hMul, Polynomial.aeval_sumIDeriv, HSub.hSub, HPow.hPow, Complex, OfNat.ofNat, Polynomial.X
-- 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
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 : ℂ)
⊢ ∃ (gp : ℤ[X]),
    gp.natDegree ≤ p * f.natDegree - 1 ∧
      ∀ {r : ℂ},
        r ∈ f.aroots ℂ →
          ‖(↑(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:
⟨gp, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
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 : ℂ)
h₁ : gp.natDegree ≤ p * f.natDegree - 1
h₂ :
  ∀ {r : ℂ},
    r ∈ f.aroots ℂ →
      ‖(↑(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)! : ℝ)
⊢ ∃ (gp : ℤ[X]),
    gp.natDegree ≤ p * f.natDegree - 1 ∧
      ∀ {r : ℂ},
        r ∈ f.aroots ℂ →
          ‖(↑(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:
refine ⟨gp, ?_, ?_⟩
-- 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
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 : ℂ)
⊢ gp.natDegree ≤ p * f.natDegree - 1

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

Premises used: tsub_le_tsub_right, Polynomial.natDegree_mul_le, 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
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 : ℂ)
h₁ : (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
⊢ gp.natDegree ≤ p * f.natDegree - 1

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

Premises used: tsub_le_tsub_right, Polynomial.natDegree_mul_le, 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
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 : ℂ)
h₁ : p - 1 + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
h₂ : p - 1 + p * f.natDegree - p ≤ p * f.natDegree - 1
h₃ : p + p * f.natDegree - 1 - p ≤ p * f.natDegree - 1
h₄ : p + p * f.natDegree - p - 1 ≤ p * f.natDegree - 1
h₅ h₆ : p * f.natDegree - 1 ≤ p * f.natDegree - 1
⊢ (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1

Tactic:
rw [natDegree_X_pow, natDegree_pow, tsub_add_eq_add_tsub prime_p.one_le, tsub_right_comm,
      add_tsub_cancel_left]

Premises used: tsub_right_comm, add_tsub_cancel_left, Nat.Prime.one_le, tsub_add_eq_add_tsub, Polynomial.natDegree_pow, Polynomial.natDegree_X_pow
-- 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
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)
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)! : ℝ)
⊢ ‖(↑(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 _
-- 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
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 ℂ
⊢ map (algebraMap ℤ ℂ) f ≠ 0 ∧ (map (algebraMap ℤ ℂ) f).IsRoot r

Tactic:
rw [mem_roots'] at hr

Premises used: Polynomial.mem_roots'
-- 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
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
h₁ :
  HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
    map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1)) * map (algebraMap ℤ ℂ) f ^ p
⊢ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
    map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)

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

Premises used: Polynomial.map_mul, Polynomial.map_pow
-- 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
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)) * map (algebraMap ℤ ℂ) f ^ p

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

Premises used: Iff.mpr, dvd_mul_of_dvd_right, pow_dvd_pow_of_dvd, And.right, Polynomial.dvd_iff_isRoot
-- 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
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)) * map (algebraMap ℤ ℂ) f ^ p

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

Premises used: Iff.mpr, dvd_mul_of_dvd_right, pow_dvd_pow_of_dvd, And.right, Polynomial.dvd_iff_isRoot
-- 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]) =
    HSMul.hSMul (β := ℂ) p ! ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
⊢ (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

Premises used: nsmul_eq_mul