awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
h₁ : HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x
h₂ :
  HasDerivAt ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s)
    (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * HSMul.hSMul (α := ℝ) 1 s) x
h :
  s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s *
          ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s) x +
        cexp (-(x • s)) *
          (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) *
            HSMul.hSMul (α := ℝ) 1 s))
⊢ HasDerivAt (fun (x : ℝ) ↦ -(cexp (-(x • s)) * eval (x • s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)))
    (s * (cexp (-(x • s)) * eval (x • s) p)) x

Tactic:
convert! (h₁.mul h₂).fun_neg using 1

Premises used: HasDerivAt.fun_neg, HasDerivAt.mul
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
h₁ : HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x
h₂ :
  HasDerivAt ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s)
    (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * HSMul.hSMul (α := ℝ) 1 s) x
h :
  s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s *
          ((fun (x : ℂ) ↦
                eval x
                  (HAdd.hAdd (β := ℂ[X]) p
                    ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p) : ℂ[X]))) ∘
              fun (y : ℝ) ↦ y • s)
            x +
        cexp (-(x • s)) *
          (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) *
            HSMul.hSMul (α := ℝ) 1 s))
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s *
          ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s) x +
        cexp (-(x • s)) *
          (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) *
            HSMul.hSMul (α := ℝ) 1 s))

Tactic:
nth_rw 1 [sumIDeriv_eq_self_add p]

Premises used: Polynomial.sumIDeriv_eq_self_add
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
h₁ : HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x
h₂ :
  HasDerivAt ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s)
    (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * HSMul.hSMul (α := ℝ) 1 s) x
h :
  s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -s *
          (eval (x • s) p + eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p))) +
        cexp (-(x • s)) * (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * s))
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s *
          ((fun (x : ℂ) ↦
                eval x
                  (HAdd.hAdd (β := ℂ[X]) p
                    ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p) : ℂ[X]))) ∘
              fun (y : ℝ) ↦ y • s)
            x +
        cexp (-(x • s)) *
          (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) *
            HSMul.hSMul (α := ℝ) 1 s))

Tactic:
simp only [one_smul, eval_add, Function.comp_apply]

Premises used: one_smul, Polynomial.eval_add, Function.comp_apply
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
h₁ : HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x
h₂ :
  HasDerivAt ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s)
    (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * HSMul.hSMul (α := ℝ) 1 s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -s *
          (eval (x • s) p + eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p))) +
        cexp (-(x • s)) * (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * s))

Tactic:
ring
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ s * (cexp (-(x • s)) * eval (x • s) p)) (Set.uIcc 0 1)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
rw :
  -(cexp (-HSMul.hSMul (α := ℝ) 1 s) * eval (HSMul.hSMul (α := ℝ) 1 s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) -
      -(cexp (-HSMul.hSMul (α := ℝ) 0 s) * eval (HSMul.hSMul (α := ℝ) 0 s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) =
    -(cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) + eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)
⊢ s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) p =
    -(cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) + eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)

Tactic:
rw [← intervalIntegral.integral_const_mul,
    intervalIntegral.integral_eq_sub_of_hasDerivAt
      (fun x hx => hasDerivAt_cexp_mul_sumIDeriv p s x)
      (ContinuousOn.intervalIntegrable (by fun_prop))]

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt, ContinuousOn.intervalIntegrable, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, intervalIntegral.integral_const_mul
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
⊢ -(cexp (-HSMul.hSMul (α := ℝ) 1 s) * eval (HSMul.hSMul (α := ℝ) 1 s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) -
      -(cexp (-HSMul.hSMul (α := ℝ) 0 s) * eval (HSMul.hSMul (α := ℝ) 0 s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) =
    -(cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) + eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℂ[X]
s : ℂ
rw :
  P f s =
    cexp s * (-(cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)) + eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f))
rw₁ :
  P f s =
    cexp s * -(cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)) +
      cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)
rw₂ :
  P f s =
    -(cexp s * (cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f))) +
      cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)
rw₃ :
  P f s =
    -(cexp s * ((cexp s)⁻¹ * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f))) +
      cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)
rw₄ : P f s = -eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f) + cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)
rw₅ : P f s = cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f) - eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)
rw₆ rw₇ :
  cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f) - eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f) =
    cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f) - eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)

Tactic:
rw [integral_exp_mul_eval, mul_add, mul_neg, exp_neg, mul_inv_cancel_left₀ (exp_ne_zero s),
    neg_add_eq_sub, P]

Premises used: mul_inv_cancel_left₀, Complex.exp_ne_zero, neg_add_eq_sub, Complex.exp_neg, LindemannWeierstrass.integral_exp_mul_eval, mul_add, _private.0.LindemannWeierstrass.P, mul_neg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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 (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)

Tactic:
⟨|c|, abs_nonneg _, fun p => ?_⟩

Premises used: abs, And.intro, Exists.intro, abs_nonneg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
refine : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)

Tactic:
refine ⟨|c|, abs_nonneg _, fun p => ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
rw :
  Real.exp s.re * (norm (E := ℂ) (∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)) * ‖s‖) ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)
⊢ ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
rw [P_eq_integral_exp_mul_eval (f p) s, mul_comm s, norm_mul, norm_mul, norm_exp]

Premises used: _private.0.LindemannWeierstrass.P_eq_integral_exp_mul_eval, norm_mul, Complex.norm_exp, mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
hbc : norm (E := ℂ) (∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)) ≤ Real.exp ‖s‖ * |c| ^ p
⊢ Real.exp s.re * (norm (E := ℂ) (∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)) * ‖s‖) ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
hbc :
  norm (E := ℂ)
      (@MeasureTheory.integral _ _ _ _ Real.measurableSpace
        (MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Ioc 0 1)) fun (x : ℝ) ↦
        cexp (-(x • s)) * eval (x • s) (f p)) ≤
    Real.exp ‖s‖ * |c| ^ p * 1
⊢ norm (E := ℂ) (∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)) ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
rw [intervalIntegral.integral_of_le zero_le_one, ← mul_one (_ * _)]

Premises used: HMul.hMul, zero_le_one, intervalIntegral.integral_of_le, mul_one
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ norm (E := ℂ)
      (@MeasureTheory.integral _ _ _ _ Real.measurableSpace
        (MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Ioc 0 1)) fun (x : ℝ) ↦
        cexp (-(x • s)) * eval (x • s) (f p)) ≤
    Real.exp ‖s‖ * |c| ^ p *
      MeasureTheory.Measure.real (α := ℝ) (m := Real.measurableSpace) MeasureTheory.volume (Set.Ioc 0 1)

Tactic:
MeasureTheory.norm_setIntegral_le_of_norm_le_const _ _

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
h : 1 = MeasureTheory.Measure.real (α := ℝ) (m := Real.measurableSpace) MeasureTheory.volume (Set.Ioc 0 1)
hbc : LT.lt (α := ENNReal) ((MeasureTheory.volume : (a : Set ℝ) → ENNReal) (Set.Ioc 0 1) : ENNReal) (⊤ : ENNReal)
hbc₁ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
⊢ norm (E := ℂ)
      (@MeasureTheory.integral _ _ _ _ Real.measurableSpace
        (MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Ioc 0 1)) fun (x : ℝ) ↦
        cexp (-(x • s)) * eval (x • s) (f p)) ≤
    Real.exp ‖s‖ * |c| ^ p * 1

Tactic:
convert! MeasureTheory.norm_setIntegral_le_of_norm_le_const _ _

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
h : 1 = HSub.hSub (α := ℝ) 1 0
h₁ h₂ : Eq (α := ℝ) 1 1
⊢ 1 = MeasureTheory.Measure.real (α := ℝ) (m := Real.measurableSpace) MeasureTheory.volume (Set.Ioc 0 1)

Tactic:
rw [Real.volume_real_Ioc_of_le zero_le_one, sub_zero]

Premises used: sub_zero, Real.volume_real_Ioc_of_le, zero_le_one
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
hbc : ENNReal.ofReal 1 < ⊤
⊢ LT.lt (α := ENNReal) ((MeasureTheory.volume : (a : Set ℝ) → ENNReal) (Set.Ioc 0 1) : ENNReal) (⊤ : ENNReal)

Tactic:
rw [Real.volume_Ioc, sub_zero]

Premises used: sub_zero, Real.volume_Ioc
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ENNReal.ofReal 1 < ⊤

Tactic:
ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ENNReal.ofReal 1 < ⊤

Tactic:
exact ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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 : Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
⊢ ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
rw [norm_mul, norm_exp]

Premises used: norm_mul, Complex.norm_exp
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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‖
hbc₁ : ‖eval (x • s) (f p)‖ ≤ |c| ^ p
⊢ Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
⊢ 0 < x ∧ x ≤ 1

Tactic:
simp only [Set.mem_Ioc] at hx

Premises used: Set.mem_Ioc
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
hbc : ‖-(x • s)‖ ≤ ‖s‖
⊢ (-(x • s)).re ≤ ‖s‖

Tactic:
apply (re_le_norm _).trans

Premises used: Complex.re_le_norm, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
hbc : x * ‖s‖ ≤ ‖s‖
⊢ ‖-(x • s)‖ ≤ ‖s‖

Tactic:
rw [norm_neg, norm_smul, Real.norm_of_nonneg hx.1.le]

Premises used: norm_smul, LT.lt.le, And.left, norm_neg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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‖

Tactic:
mul_le_of_le_one_left (norm_nonneg _) hx.2

Premises used: mul_le_of_le_one_left, And.right, norm_nonneg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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‖

Tactic:
exact mul_le_of_le_one_left (norm_nonneg _) hx.2

Premises used: mul_le_of_le_one_left, And.right, norm_nonneg
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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 : ‖eval (x • s) (f p)‖ ≤ |c ^ p|
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p

Tactic:
rw [← abs_pow]

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

Tactic:
(hc p x hx).trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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|

Tactic:
exact (hc p x hx).trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ) (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖eval (x • s) (f p)‖ ≤ c ^ p
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
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p

Tactic:
obtain ⟨c', hc', h'⟩ := P_le_aux f s c hc

Premises used: _private.0.LindemannWeierstrass.P_le_aux
-- 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
⊢ c₁ * (c₂ * c' * c₃) ≥ 0

Tactic:
positivity
-- 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
right : ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p

Tactic:
use c₁ * (c₂ * c' * c₃), by positivity

Premises used: HMul.hMul
-- 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
⊢ ‖P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
(h' p).trans ?_

Premises used: LE.le.trans
-- 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
right : Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p
⊢ ‖P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
refine (h' p).trans ?_

Premises used: LE.le.trans
-- 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
right : Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
simp_rw [mul_pow]

Premises used: mul_pow
-- 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
x : ℝ
h : max x 1 = 1 ∧ x < 1
rw : x ≤ 1
⊢ x ≤ max x 1 ^ p

Tactic:
rw [h.1, one_pow]

Premises used: one_pow, And.left
-- 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
x : ℝ
h : max x 1 = 1 ∧ x < 1
⊢ x ≤ 1

Tactic:
h.2.le

Premises used: LT.lt.le, And.right
-- 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
x : ℝ
h : max x 1 = 1 ∧ x < 1
⊢ x ≤ 1

Tactic:
exact h.2.le

Premises used: LT.lt.le, And.right
-- 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
⊢ ∀ {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
-- 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
right : Real.exp s.re ≤ c₁ ^ p
right₁ : Real.exp ‖s‖ ≤ c₂ ^ p
right₂ : ‖s‖ ≤ c₃ ^ p
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)

Tactic:
gcongr
-- 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
⊢ Real.exp s.re ≤ c₁ ^ p

Tactic:
le_max_one_pow
-- 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
⊢ Real.exp s.re ≤ c₁ ^ p

Tactic:
exact le_max_one_pow
-- 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
⊢ Real.exp ‖s‖ ≤ c₂ ^ p

Tactic:
le_max_one_pow
-- 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
⊢ Real.exp ‖s‖ ≤ c₂ ^ p

Tactic:
exact le_max_one_pow
-- 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:
le_max_one_pow