awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have mpr : ∀ (x' y' : ℕ) (h : b = HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2),
  ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
x' y' : ℕ
h : b = HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2
⊢ n = HPow.hPow (β := ℕ) (a * x') 2 + HPow.hPow (β := ℕ) (a * y') 2
have rw : HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2) =
  HPow.hPow (β := ℕ) (a * x') 2 + HPow.hPow (β := ℕ) (a * y') 2
Tactic: rw [h₁, h]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
have inl : (∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
  ∀ q ∈ primeFactors 0, q % 4 = 3 → Even (padicValNat q 0)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn₀)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
inl :
  (∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ primeFactors 0, q % 4 = 3 → Even (padicValNat q 0)
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
have inr : ∀ (hn₀ : n > 0),
  (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn₀)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn₀ : n > 0
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
have inr : (∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)) →
  ∀ (q : ℕ) (hq : q ∈ n.primeFactors) (h : q % 4 = 3) (a b : ℕ) (h₁ : n = HPow.hPow (β := ℕ) a 2 * b)
    (h₂ : IsSquare (α := ZMod b) (-1)), Even (padicValNat q n)
Tactic: refine eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn₀ : n > 0
inr :
  (∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)) →
    ∀ (q : ℕ) (hq : q ∈ n.primeFactors) (h : q % 4 = 3) (a b : ℕ) (h₁ : n = HPow.hPow (β := ℕ) a 2 * b)
      (h₂ : IsSquare (α := ZMod b) (-1)), Even (padicValNat q n)
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
have inr₁ : ∀ (H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)),
  ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
Tactic: refine eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn₀ : n > 0
h_1 : ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
⊢ Even (padicValNat q n)
have this : Fact (Prime q)
Tactic: have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn₀ : n > 0
h_1 : ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
this : Fact (Prime q)
⊢ Even (padicValNat q n)
have this₁ : q ∣ b → q ∈ b.primeFactors
Tactic: have : q ∣ b → q ∈ b.primeFactors := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have inr : ∀ (b a : ℕ) (hb₀ : 0 < b) (ha₀ : 0 < a) (hab : HPow.hPow (β := ℕ) a 2 * b = n) (hb : Squarefree b),
  ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
Tactic: obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := sq_mul_squarefree_of_pos hn₀
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have inr : ∀ (q : ℕ) (hq : q ∈ b.primeFactors) (hq4 : q % 4 = 3), False
Tactic: refine ⟨a, b, hab.symm, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hb
      |>.mpr fun q hq hq4 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
⊢ False
have this : Fact (Prime q)
Tactic: have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
this : Fact (Prime q)
⊢ False
have this₁ : ∀ (hn : n ≠ 0), b.primeFactors ⊆ n.primeFactors
Tactic: have := Nat.primeFactors_mono <| Dvd.intro_left _ hab
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
this_1 : Fact (Prime q)
this : ∀ (hn : n ≠ 0), b.primeFactors ⊆ n.primeFactors
⊢ False
have this₁ : Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) (1 : ℕ)
Tactic: have : b.factorization q = 1 := by grind [Squarefree.natFactorization_le_one,
      Prime.dvd_iff_one_le_factorization, prime_of_mem_primeFactors, dvd_of_mem_primeFactors]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ -(cexp (-(x • s)) * eval (x • s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)))
    (s * (cexp (-(x • s)) * eval (x • s) p)) x
have h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
Tactic: have h₀ := (hasDerivAt_id' x).smul_const s
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
⊢ HasDerivAt (fun (x : ℝ) ↦ -(cexp (-(x • s)) * eval (x • s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)))
    (s * (cexp (-(x • s)) * eval (x • s) p)) x
have h₁ : HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x
Tactic: have h₁ := h₀.fun_neg.cexp
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
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
⊢ HasDerivAt (fun (x : ℝ) ↦ -(cexp (-(x • s)) * eval (x • s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)))
    (s * (cexp (-(x • s)) * eval (x • s) p)) x
have 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
Tactic: have h₂ := ((sumIDeriv p).hasDerivAt (x • s)).comp x h₀
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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
⊢ HasDerivAt (fun (x : ℝ) ↦ -(cexp (-(x • s)) * eval (x • s) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)))
    (s * (cexp (-(x • s)) * eval (x • s) p)) x
have 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))
Tactic: convert! (h₁.mul h₂).fun_neg using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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)) * -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))
have 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))
Tactic: nth_rw 1 [sumIDeriv_eq_self_add p]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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)) * -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))
have 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))
Tactic: simp only [one_smul, eval_add, Function.comp_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
p : ℂ[X]
s : ℂ
⊢ 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)
have 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)
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
Goal:
f : ℂ[X]
s : ℂ
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)
have rw : P f s =
  cexp s * (-(cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)) + eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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))
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)
have rw₁ : P f s =
  cexp s * -(cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f)) +
    cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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)
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)
have rw₂ : P f s =
  -(cexp s * (cexp (-s) * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f))) +
    cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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)
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)
have rw₃ : P f s =
  -(cexp s * ((cexp s)⁻¹ * eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f))) +
    cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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)
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)
have rw₄ : P f s = -eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f) + cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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)
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)
have rw₅ : P f s = cexp s * eval 0 ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) f) - eval s ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (goal)
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)
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)
have 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)
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]
-- 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 (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
have refine : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)
Tactic: refine ⟨|c|, abs_nonneg _, fun p => ?_⟩
-- 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 : ℕ
⊢ ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)
have 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‖)
Tactic: rw [P_eq_integral_exp_mul_eval (f p) s, mul_comm s, norm_mul, 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 : ℕ
⊢ 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‖)
have hbc : norm (E := ℂ) (∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)) ≤ Real.exp ‖s‖ * |c| ^ p
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 : ℕ
⊢ norm (E := ℂ) (∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)) ≤ Real.exp ‖s‖ * |c| ^ p
have 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
Tactic: rw [intervalIntegral.integral_of_le zero_le_one, ← mul_one (_ * _)]
-- 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 : ℕ
⊢ 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
have h : 1 = MeasureTheory.Measure.real (α := ℝ) (m := Real.measurableSpace) MeasureTheory.volume (Set.Ioc 0 1)
Tactic: convert! MeasureTheory.norm_setIntegral_le_of_norm_le_const _ _
-- 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 : ℕ
h : 1 = MeasureTheory.Measure.real (α := ℝ) (m := Real.measurableSpace) MeasureTheory.volume (Set.Ioc 0 1)
⊢ 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
have hbc : LT.lt (α := ENNReal) ((MeasureTheory.volume : (a : Set ℝ) → ENNReal) (Set.Ioc 0 1) : ENNReal) (⊤ : ENNReal)
Tactic: convert! MeasureTheory.norm_setIntegral_le_of_norm_le_const _ _
-- 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 : ℕ
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)
⊢ 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
have hbc₁ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) x → ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
Tactic: convert! MeasureTheory.norm_setIntegral_le_of_norm_le_const _ _
-- 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 : ℕ
⊢ 1 = MeasureTheory.Measure.real (α := ℝ) (m := Real.measurableSpace) MeasureTheory.volume (Set.Ioc 0 1)
have h : 1 = HSub.hSub (α := ℝ) 1 0
Tactic: rw [Real.volume_real_Ioc_of_le zero_le_one, 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 : ℕ
h : 1 = HSub.hSub (α := ℝ) 1 0
⊢ 1 = MeasureTheory.Measure.real (α := ℝ) (m := Real.measurableSpace) MeasureTheory.volume (Set.Ioc 0 1)
have h₁ : Eq (α := ℝ) 1 1
Tactic: rw [Real.volume_real_Ioc_of_le zero_le_one, sub_zero]