awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
h_const : Eq (α := ℚ⟦X⟧) ((C : (a : ℚ) → ℚ⟦X⟧) ((constantCoeff : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ) : ℚ⟦X⟧) (1 : ℚ⟦X⟧)
rw :
  HSub.hSub (β := ℚ⟦X⟧) (exp ℚ ^ n) ((C : (a : ℚ) → ℚ⟦X⟧) ((constantCoeff : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ) : ℚ⟦X⟧) =
    HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
⊢ exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
have rw₁ : HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
  HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
Tactic: rw [← h_const, sub_const_eq_X_mul_shift]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
⊢ Eq (α := ℚ⟦X⟧)
    (PowerSeries.mk fun (p : ℕ) ↦
      ∑ k ∈ range n,
        HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑k : ℚ) p) ((algebraMap ℚ ℚ : (a : ℚ) → ℚ) (↑p ! : ℚ)⁻¹ : ℚ))
    (PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))
have h_r : exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
Tactic: have h_r : exp ℚ ^ n - 1 = X * mk fun p => coeff (p + 1) (exp ℚ ^ n) := by
      have h_const : C (constantCoeff (exp ℚ ^ n)) = 1 := by simp
      rw [← h_const, sub_const_eq_X_mul_shift]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
h_r :
  exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
⊢ Eq (α := ℚ⟦X⟧)
    (PowerSeries.mk fun (p : ℕ) ↦
      ∑ k ∈ range n,
        HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑k : ℚ) p) ((algebraMap ℚ ℚ : (a : ℚ) → ℚ) (↑p ! : ℚ)⁻¹ : ℚ))
    (PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))
have rw : (PowerSeries.mk fun (p : ℕ) ↦
      ∑ k ∈ range n,
        HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑k : ℚ) p) ((algebraMap ℚ ℚ : (a : ℚ) → ℚ) (↑p ! : ℚ)⁻¹ : ℚ)) *
    (exp ℚ - 1) =
  (exp ℚ - 1) *
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
Tactic: rw [← mul_right_inj' hexp, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
h_r :
  exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
⊢ (PowerSeries.mk fun (p : ℕ) ↦
        ∑ k ∈ range n,
          HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑k : ℚ) p) ((algebraMap ℚ ℚ : (a : ℚ) → ℚ) (↑p ! : ℚ)⁻¹ : ℚ)) *
      (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun (p : ℕ) ↦
        ∑ i ∈ range (p + 1),
          bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
have rw : HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
      (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) *
    (exp ℚ - 1) =
  (exp ℚ - 1) *
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
Tactic: rw [← exp_pow_sum, geom_sum_mul, h_r, ← bernoulliPowerSeries_mul_exp_sub_one,
      bernoulliPowerSeries, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
h_r :
  exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
⊢ HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
        (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) *
      (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun (p : ℕ) ↦
        ∑ i ∈ range (p + 1),
          bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
have simp : HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
    (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
  PowerSeries.mk fun (p : ℕ) ↦
    ∑ x ∈ range (p + 1),
      HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) * (bernoulli x * (↑((p + 1).choose x) : ℚ)) / (↑(p + 1)! : ℚ)
Tactic: simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
h_r :
  exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
⊢ HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
      (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ x ∈ range (p + 1),
        HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) * (bernoulli x * (↑((p + 1).choose x) : ℚ)) / (↑(p + 1)! : ℚ)
have refine_1 : Eq (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
    (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ)) ∨
  Eq (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) 0
Tactic: refine Eq.trans (mul_eq_mul_right_iff.mpr ?_) (Eq.trans h_cauchy ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
h_r :
  exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
refine_1 :
  Eq (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
      (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ)) ∨
    Eq (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) 0
⊢ HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
      (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ x ∈ range (p + 1),
        HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) * (bernoulli x * (↑((p + 1).choose x) : ℚ)) / (↑(p + 1)! : ℚ)
have refine_2 : Eq (α := ℚ⟦X⟧)
  (PowerSeries.mk fun (p : ℕ) ↦
    ∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))
  (PowerSeries.mk fun (p : ℕ) ↦
    ∑ x ∈ range (p + 1),
      HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) * (bernoulli x * (↑((p + 1).choose x) : ℚ)) / (↑(p + 1)! : ℚ))
Tactic: refine Eq.trans (mul_eq_mul_right_iff.mpr ?_) (Eq.trans h_cauchy ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hexp : exp ℚ - 1 ≠ 0
h_r :
  exp ℚ ^ n - 1 = HMul.hMul (α := ℚ⟦X⟧) X (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))
⊢ Eq (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
      (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ)) ∨
    Eq (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) 0
have refine_1 : Eq (α := ℚ⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (bernoulli n / (↑n ! : ℚ)))
  (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
⊢ Eq (α := ℚ) (∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p)
    (∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / HAdd.hAdd (α := ℚ) (↑p : ℚ) 1)
have hps : ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p =
  HMul.hMul (α := ℚ)
    (∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))
    (↑p ! : ℚ)
Tactic: have hps :
    (∑ k ∈ range n, (k : ℚ) ^ p) =
      (∑ i ∈ range (p + 1),
          bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)!) * p ! := by
    suffices
      (mk fun p => ∑ k ∈ range n, (k : ℚ) ^ p * algebraMap ℚ ℚ p !⁻¹) =
        mk fun p =>
          ∑ i ∈ range (p + 1), bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)! by
      rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]
      rw [PowerSeries.ext_iff] at this
      simpa using this p
    -- the power series `exp ℚ - 1` is non-zero, a fact we need in order to use `mul_right_inj'`
    have hexp : exp ℚ - 1 ≠ 0 := by
      simp only [exp, PowerSeries.ext_iff, Ne, not_forall]
      use 1
      simp
    have h_r : exp ℚ ^ n - 1 = X * mk fun p => coeff (p + 1) (exp ℚ ^ n) := by
      have h_const : C (constantCoeff (exp ℚ ^ n)) = 1 := by simp
      rw [← h_const, sub_const_eq_X_mul_shift]
    -- key step: a chain of equalities of power series
    rw [← mul_right_inj' hexp, mul_comm]
    rw [← exp_pow_sum, geom_sum_mul, h_r, ← bernoulliPowerSeries_mul_exp_sub_one,
      bernoulliPowerSeries, mul_right_comm]
    simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false]
    refine Eq.trans (mul_eq_mul_right_iff.mpr ?_) (Eq.trans h_cauchy ?_)
    · left
      congr
    · simp only [mul_comm, factorial]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hps :
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p =
    HMul.hMul (α := ℚ)
      (∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))
      (↑p ! : ℚ)
⊢ Eq (α := ℚ) (∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p)
    (∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / HAdd.hAdd (α := ℚ) (↑p : ℚ) 1)
have rw : Eq (α := ℚ)
  (∑ i ∈ range (p + 1),
    bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ) * (↑p ! : ℚ))
  (∑ i ∈ range (p + 1),
    bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / HAdd.hAdd (α := ℚ) (↑p : ℚ) 1)
Tactic: rw [hps, sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h_cauchy :
  HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)
hps :
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p =
    HMul.hMul (α := ℚ)
      (∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))
      (↑p ! : ℚ)
⊢ Eq (α := ℚ)
    (∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ) * (↑p ! : ℚ))
    (∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / HAdd.hAdd (α := ℚ) (↑p : ℚ) 1)
have refine : ∀ x ∈ range (p + 1),
  bernoulli x * (↑((p + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) / (↑(p + 1)! : ℚ) * (↑p ! : ℚ) =
    bernoulli x * (↑((p + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) / HAdd.hAdd (α := ℚ) (↑p : ℚ) 1
Tactic: refine sum_congr rfl fun x _ => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑k : ℚ) p)
    (∑ i ∈ range (p + 1),
      bernoulli' i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) /
        HAdd.hAdd (α := ℚ) (↑p : ℚ) 1)
have rw : Eq (α := ℚ) (∑ k ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑k : ℚ) p)
  (∑ i ∈ range (p + 1),
    bernoulli' i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑p.succ : ℚ))
Tactic: rw [← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have hle : 1 ≤ n + 1
Tactic: have hle := Nat.le_add_left 1 n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
⊢ HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
Tactic: have hne : (p + 1 + 1 : ℚ) ≠ 0 := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
r : ℚ
⊢ r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
    r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
have rw : r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
  r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
r : ℚ
rw :
  r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
    r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
have rw₁ : r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have h1 : ∀ (r : ℚ),
  r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
    r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: have h1 : ∀ r : ℚ, r * (p + 1 + 1) * (n : ℚ) ^ p.succ / (p + 1 + 1 : ℚ) = r * (n : ℚ) ^ p.succ :=
      fun r => by rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
have simp_rw : -1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
  1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: have h2 : f 1 + (n : ℚ) ^ p.succ = 1 / 2 * (n : ℚ) ^ p.succ := by
    simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1]
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
i : ℕ
h : i ∈ range p
⊢ bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ) =
    bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ)
have rw : bernoulli' i.succ.succ * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ) =
  bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ)
Tactic: rw [bernoulli_eq_bernoulli'_of_ne_one (succ_succ_ne_one i)]