awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ LT.lt (α := ENNReal) ((MeasureTheory.volume : (a : Set ℝ) → ENNReal) (Set.Ioc 0 1) : ENNReal) (⊤ : ENNReal)
have hbc : ENNReal.ofReal 1 < ⊤
Tactic: rw [Real.volume_Ioc, sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
⊢ ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
have hbc : Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
Tactic: rw [norm_mul, norm_exp]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
⊢ Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
have hbc : (-(x • s)).re ≤ ‖s‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
hbc : (-(x • s)).re ≤ ‖s‖
⊢ Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
have hbc₁ : ‖eval (x • s) (f p)‖ ≤ |c| ^ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
⊢ (-(x • s)).re ≤ ‖s‖
have hx₁ : 0 < x ∧ x ≤ 1
Tactic: simp only [Set.mem_Ioc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ (-(x • s)).re ≤ ‖s‖
have hbc : ‖-(x • s)‖ ≤ ‖s‖
Tactic: apply (re_le_norm _).trans
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : 0 < x ∧ x ≤ 1
⊢ ‖-(x • s)‖ ≤ ‖s‖
have hbc : x * ‖s‖ ≤ ‖s‖
Tactic: rw [norm_neg, norm_smul, Real.norm_of_nonneg hx.1.le]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p
have hbc : ‖eval (x • s) (f p)‖ ≤ |c ^ p|
Tactic: rw [← abs_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p
have obtain : ∀ (c' : ℝ) (hc' : c' ≥ 0) (h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)),
  ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p
Tactic: obtain ⟨c', hc', h'⟩ := P_le_aux f s c hc
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p
have right : ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p
Tactic: use c₁ * (c₂ * c' * c₃), by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
⊢ ‖P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p
have right : Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p
Tactic: refine (h' p).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p
have right : Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)
Tactic: simp_rw [mul_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
x : ℝ
h : max x 1 = 1 ∧ x < 1
⊢ x ≤ max x 1 ^ p
have rw : x ≤ 1
Tactic: rw [h.1, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)
have le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
Tactic: have le_max_one_pow {x : ℝ} : x ≤ max x 1 ^ p :=
    (max_cases x 1).elim (fun h ↦ h.1.symm ▸ le_self_pow₀ h.2 hp)
      fun h ↦ by rw [h.1, one_pow]; exact h.2.le
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)
have right : Real.exp s.re ≤ c₁ ^ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
right : Real.exp s.re ≤ c₁ ^ p
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)
have right₁ : Real.exp ‖s‖ ≤ c₂ ^ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
right : Real.exp s.re ≤ c₁ ^ p
right₁ : Real.exp ‖s‖ ≤ c₂ ^ p
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)
have right₂ : ‖s‖ ≤ c₃ ^ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
f : ℤ[X]
s : ℂ
⊢ Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
have h : Subset (α := Set ℝ)
  ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
  ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Icc 0 1)
Tactic: have h :
      (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1 ⊆
        (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Icc 0 1 :=
      Set.image_mono Set.Ioc_subset_Icc_self
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
h :
  Subset (α := Set ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Icc 0 1)
⊢ Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
have refine : Continuous (Y := ℝ) fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)
Tactic: refine (IsCompact.image isCompact_Icc ?_).isBounded.subset h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
f : ℤ[X]
s : ℂ
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) s‖ ≤ c ^ p
have this : Bornology.IsBounded (α := ℝ)
  ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
Tactic: have : Bornology.IsBounded
      ((fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1) := by
    have h :
      (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1 ⊆
        (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Icc 0 1 :=
      Set.image_mono Set.Ioc_subset_Icc_self
    refine (IsCompact.image isCompact_Icc ?_).isBounded.subset h
    fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) s‖ ≤ c ^ p
have obtain : ∀ (c : ℝ)
  (h :
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ)
          ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) ''
            Set.Ioc 0 1)
          x →
        ‖x‖ ≤ c),
  ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) s‖ ≤ c ^ p
Tactic: obtain ⟨c, h⟩ := this.exists_norm_le
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
h :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ)
        ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
        x →
      |x| ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) s‖ ≤ c ^ p
have refine : ∀ (p : ℕ) (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x),
  ‖eval (x • s) (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p))‖ ≤ c ^ p
Tactic: refine P_le _ s c (fun p x hx => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
h :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ)
        ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
        x →
      |x| ≤ c
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p))‖ ≤ c ^ p
have h₁ : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
Tactic: specialize h (max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) (Set.mem_image_of_mem _ hx)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p))‖ ≤ c ^ p
have grw : ‖eval (x • s) (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p))‖ ≤
  |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ^ p
Tactic: grw [← h]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p))‖ ≤
    |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ^ p
have simp_rw : x ^ (p - 1) * ‖s‖ ^ (p - 1) * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ) ^ p ≤
  |max (x * ‖s‖) 1| ^ p * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ) ^ p
Tactic: simp_rw [Polynomial.map_mul, Polynomial.map_pow, map_X, eval_mul, eval_pow, eval_X, norm_mul,
    Complex.norm_pow, real_smul, norm_mul, norm_real, ← eval₂_eq_eval_map, ← aeval_def, abs_mul,
    abs_norm, mul_pow, Real.norm_of_nonneg hx.1.le]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ) ^ p ≤
    |max (x * ‖s‖) 1| ^ p * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ) ^ p
have refine : x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p
Tactic: refine mul_le_mul_of_nonneg_right ?_ (pow_nonneg (norm_nonneg _) _)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p
have rw : (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p
Tactic: rw [← mul_pow, abs_of_nonneg (by positivity), max_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
⊢ (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p
have pos : ∀ (hx1 : x * ‖s‖ ≤ 1), (x * ‖s‖) ^ (p - 1) ≤ HPow.hPow (α := ℝ) 1 p
Tactic: split_ifs with hx1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
pos : ∀ (hx1 : x * ‖s‖ ≤ 1), (x * ‖s‖) ^ (p - 1) ≤ HPow.hPow (α := ℝ) 1 p
⊢ (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p
have neg : ∀ (hx1 : ¬x * ‖s‖ ≤ 1), (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p
Tactic: split_ifs with hx1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ HPow.hPow (α := ℝ) 1 p
have pos : (x * ‖s‖) ^ (p - 1) ≤ 1
Tactic: rw [one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
f : ℤ[X]
s : ℂ
this :
  Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x
h : |max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)| ≤ c
hx1 : ¬x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p
have hx1₁ : 1 < x * ‖s‖
Tactic: push Not at hx1
Cleared hypotheses: hx1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
⊢ ∃ (c : ℝ),
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ (n : ℤ),
          ¬(↑p : ℤ) ∣ n ∧
            ∃ (gp : ℤ[X]),
              gp.natDegree ≤ p * f.natDegree - 1 ∧
                ∀ {r : ℂ},
                  r ∈ f.aroots ℂ →
                    ‖n • cexp r - HSMul.hSMul (β := ℂ) p ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)‖ ≤ c ^ p / (↑(p - 1)! : ℝ)
have simp_rw : ∃ (c : ℝ),
  ∀ p > (eval 0 f).natAbs,
    Nat.Prime p →
      ∃ (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 : ℂ)‖ ≤
                    c ^ p / (↑(p - 1)! : ℝ)
Tactic: simp_rw [nsmul_eq_mul, zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
⊢ ∃ (c : ℝ),
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ (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 : ℂ)‖ ≤
                      c ^ p / (↑(p - 1)! : ℝ)
have choose : ∀ (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),
  ∃ (c : ℝ),
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ (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 : ℂ)‖ ≤
                      c ^ p / (↑(p - 1)! : ℝ)
Tactic: choose c' c'0 Pp'_le using exp_polynomial_approx_aux f
-- 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
⊢ ∃ (c : ℝ),
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ (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 : ℂ)‖ ≤
                      c ^ p / (↑(p - 1)! : ℝ)
have h : ∀ p > (eval 0 f).natAbs,
  Nat.Prime p →
    ∃ (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
    if h : ((f.aroots ℂ).map c').toFinset.Nonempty then ((f.aroots ℂ).map c').toFinset.max' h else 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
⊢ ∃ (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 : ∀ (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)! : ℝ)
Tactic: obtain ⟨gp', -, h'⟩ := eval_sumIDeriv_of_pos (X ^ (p - 1) * f ^ p) prime_p.pos
-- 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'
⊢ 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 = HSub.hSub (α := ℤ[X]) X 0 ^ (p - 1) * f ^ p
Tactic: rw [C_0, sub_zero]