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' :
  ∀ (r : ℤ) {p' : ℤ[X]},
    HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p =
        HSub.hSub (α := ℤ[X]) (β := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) r : ℤ[X]) ^ (p - 1) * p' →
      eval r ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
        (p - 1)! • eval r p' + p ! • eval r gp'
rw : HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p = HSub.hSub (α := ℤ[X]) X 0 ^ (p - 1) * f ^ p
⊢ HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p = HSub.hSub (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 0) ^ (p - 1) * f ^ p
have rw₁ : HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p = HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p
Tactic: rw [C_0, sub_zero]
-- 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' :
  ∀ (r : ℤ) {p' : ℤ[X]},
    HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p =
        HSub.hSub (α := ℤ[X]) (β := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) r : ℤ[X]) ^ (p - 1) * p' →
      eval r ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
        (p - 1)! • eval r p' + p ! • eval r gp'
⊢ ∃ (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)! : ℝ)
have 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'
Tactic: specialize h' 0 (by rw [C_0, sub_zero])
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'
⊢ ∃ (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)! : ℝ)
have 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)! : ℝ)
Tactic: use f.eval 0 ^ p + p * gp'.eval 0
-- 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'
⊢ ¬(↑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)! : ℝ)
have h : ¬(↑p : ℤ) ∣ eval 0 f ^ p + (↑p : ℤ) * eval 0 gp'
Tactic: constructor
-- 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'
h : ¬(↑p : ℤ) ∣ eval 0 f ^ p + (↑p : ℤ) * eval 0 gp'
⊢ ¬(↑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)! : ℝ)
have 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)! : ℝ)
Tactic: constructor
-- 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'
⊢ ¬(↑p : ℤ) ∣ eval 0 f ^ p + (↑p : ℤ) * eval 0 gp'
have h : ¬(↑p : ℤ) ∣ eval 0 f ^ p
Tactic: rw [dvd_add_left (dvd_mul_right _ _)]
-- 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'
⊢ ¬(↑p : ℤ) ∣ eval 0 f ^ p
have h : ∀ (h : (↑p : ℤ) ∣ eval 0 f ^ p), p ≤ (eval 0 f).natAbs
Tactic: contrapose! p_gt with h
Cleared hypotheses: p_gt
-- 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.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)! : ℝ)
have 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)! : ℝ)
Tactic: obtain ⟨gp, gp'_le, h⟩ := aeval_sumIDeriv ℂ (X ^ (p - 1) * f ^ p) 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
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)! : ℝ)
have h₁ : gp.natDegree ≤ p * f.natDegree - 1
Tactic: refine ⟨gp, ?_, ?_⟩
-- 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 : ℂ)
h₁ : gp.natDegree ≤ p * f.natDegree - 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)! : ℝ)
have 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)! : ℝ)
Tactic: refine ⟨gp, ?_, ?_⟩
-- 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 : ℂ)
⊢ gp.natDegree ≤ p * f.natDegree - 1
have h₁ : (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
Tactic: refine gp'_le.trans ((tsub_le_tsub_right natDegree_mul_le p).trans ?_)
-- 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 : ℂ)
⊢ (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
have h₁ : p - 1 + (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]
-- 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 : ℂ)
h₁ : p - 1 + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
⊢ (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
have h₂ : p - 1 + p * f.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]
-- 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 : ℂ)
h₁ : p - 1 + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
h₂ : p - 1 + p * f.natDegree - p ≤ p * f.natDegree - 1
⊢ (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
have h₃ : p + p * f.natDegree - 1 - 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]
-- 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 : ℂ)
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
⊢ (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
have h₄ : p + p * f.natDegree - p - 1 ≤ 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]
-- 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 : ℂ)
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
⊢ (HPow.hPow (α := ℤ[X]) X (p - 1)).natDegree + (f ^ p).natDegree - p ≤ p * f.natDegree - 1
have h₅ : p * f.natDegree - 1 ≤ 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]
-- 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 ℂ
⊢ ‖(↑(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₁ : HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) ^ p ∣
  map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)
Tactic: specialize h r _