awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
⊢ ‖s‖ ≤ c₃ ^ p

Tactic:
exact le_max_one_pow
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
s : ℂ
⊢ 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
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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)

Tactic:
(IsCompact.image isCompact_Icc ?_).isBounded.subset h

Premises used: IsCompact.isBounded, CompactIccSpace.isCompact_Icc, Bornology.IsBounded.subset, IsCompact.image
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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)
refine :
  Continuous (Y := ℝ) fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)
⊢ Bornology.IsBounded (α := ℝ)
    ((fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)) '' Set.Ioc 0 1)

Tactic:
refine (IsCompact.image isCompact_Icc ?_).isBounded.subset h

Premises used: IsCompact.isBounded, CompactIccSpace.isCompact_Icc, Bornology.IsBounded.subset, IsCompact.image
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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)
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ max (x * ‖s‖) 1 * norm (E := ℂ) ((aeval ((↑x : ℂ) * s) : (a : ℤ[X]) → ℂ) f : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
s : ℂ
⊢ 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
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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)
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
⊢ ∃ 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

Premises used: Bornology.IsBounded.exists_norm_le
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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

Tactic:
P_le _ s c (fun p x hx => ?_)

Premises used: _private.0.LindemannWeierstrass.P_le
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
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
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
refine P_le _ s c (fun p x hx => ?_)

Premises used: _private.0.LindemannWeierstrass.P_le
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
⊢ |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)

Premises used: Norm.norm, HMul.hMul, Complex.ofReal, Max.max, Set.mem_image_of_mem, Polynomial.aeval, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
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
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p))‖ ≤ c ^ p

Tactic:
grw [← h]
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
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
⊢ ‖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:
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]

Premises used: Complex.real_smul, Polynomial.map_mul, Complex.norm_pow, Polynomial.eval_X, Polynomial.eval_pow, abs_mul, Polynomial.map_pow, LT.lt.le, Polynomial.map_X, Polynomial.eval_mul, norm_mul, Complex.norm_real, Polynomial.aeval_def, And.left, abs_norm, mul_pow, Polynomial.eval₂_eq_eval_map, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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

Tactic:
mul_le_mul_of_nonneg_right ?_ (pow_nonneg (norm_nonneg _) _)

Premises used: pow_nonneg, mul_le_mul_of_nonneg_right, norm_nonneg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
refine : x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p
⊢ 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:
refine mul_le_mul_of_nonneg_right ?_ (pow_nonneg (norm_nonneg _) _)

Premises used: pow_nonneg, mul_le_mul_of_nonneg_right, norm_nonneg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
⊢ 0 ≤ max (x * ‖s‖) 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
rw : (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p

Tactic:
rw [← mul_pow, abs_of_nonneg (by positivity), max_def]

Premises used: abs_of_nonneg, mul_pow, max_def
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
neg : ∀ (hx1 : ¬x * ‖s‖ ≤ 1), (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p
⊢ (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p

Tactic:
split_ifs with hx1
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
pos : (x * ‖s‖) ^ (p - 1) ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ HPow.hPow (α := ℝ) 1 p

Tactic:
rw [one_pow]

Premises used: one_pow
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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) ≤ 1

Tactic:
pow_le_one₀ (mul_nonneg hx.1.le (norm_nonneg _)) hx1

Premises used: mul_nonneg, LT.lt.le, And.left, norm_nonneg, pow_le_one₀
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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) ≤ 1

Tactic:
exact pow_le_one₀ (mul_nonneg hx.1.le (norm_nonneg _)) hx1

Premises used: mul_nonneg, LT.lt.le, And.left, norm_nonneg, pow_le_one₀
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
⊢ 1 < x * ‖s‖

Tactic:
push Not at hx1

Premises used: Not
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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 : 1 < x * ‖s‖
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p

Tactic:
pow_le_pow_right₀ hx1.le (Nat.sub_le _ _)

Premises used: Nat.sub_le, LT.lt.le, pow_le_pow_right₀
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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 : 1 < x * ‖s‖
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p

Tactic:
exact pow_le_pow_right₀ hx1.le (Nat.sub_le _ _)

Premises used: Nat.sub_le, LT.lt.le, pow_le_pow_right₀
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
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)! : ℝ)
⊢ ∃ (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)! : ℝ)

Tactic:
simp_rw [nsmul_eq_mul, zsmul_eq_mul]

Premises used: zsmul_eq_mul, nsmul_eq_mul
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
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)! : ℝ)
⊢ ∃ (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

Premises used: _private.0.LindemannWeierstrass.exp_polynomial_approx_aux
-- 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
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)! : ℝ)
⊢ ∃ (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:
use
    if h : ((f.aroots ℂ).map c').toFinset.Nonempty then ((f.aroots ℂ).map c').toFinset.max' h else 0

Premises used: Multiset.toFinset, Multiset.map, Polynomial.aroots, Finset.Nonempty, Complex
-- 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
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)! : ℝ)
⊢ ∃ (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

Premises used: HMul.hMul, HSub.hSub, Nat.Prime.pos, HPow.hPow, Polynomial.eval_sumIDeriv_of_pos, 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' :
  ∀ (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
rw₁ rw₂ : HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p = HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p
⊢ HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p = HSub.hSub (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 0) ^ (p - 1) * f ^ p

Tactic:
rw [C_0, sub_zero]

Premises used: sub_zero, Polynomial.C_0
-- 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' :
  ∀ (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'
⊢ 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])

Premises used: OfNat.ofNat