awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h_1 : m ∈ range q.succ
h : m < q + 1
h₁ :
  bernoulli m * (↑((q + 1)! / (m ! * (q + 1 - m)!)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) =
    HMul.hMul (β := ℚ) (bernoulli m * (↑q.succ ! : ℚ) / (↑m ! : ℚ))
      ((coeff (q - m + 1) : (a : ℚ⟦X⟧) → ℚ)
          (({
                  toFun := fun (f : ℚ⟦X⟧) ↦
                    PowerSeries.mk fun (n_1 : ℕ) ↦
                      HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑n : ℚ) n_1) ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ) f : ℚ),
                  map_one' := ⋯, map_mul' := ⋯ } :
                (a : ℚ⟦X⟧) → ℚ⟦X⟧)
              (exp ℚ) :
            ℚ⟦X⟧) :
        ℚ)
⊢ HMul.hMul (β := ℚ) (bernoulli m / (↑m ! : ℚ))
      ((coeff (q - m + 1) : (a : ℚ⟦X⟧) → ℚ)
          (({
                  toFun := fun (f : ℚ⟦X⟧) ↦
                    PowerSeries.mk fun (n_1 : ℕ) ↦
                      HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑n : ℚ) n_1) ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ) f : ℚ),
                  map_one' := ⋯, map_mul' := ⋯ : ℚ⟦X⟧ →* ℚ⟦X⟧ } :
                (a : ℚ⟦X⟧) → ℚ⟦X⟧)
              (exp ℚ) :
            ℚ⟦X⟧) :
        ℚ) =
    bernoulli m * (↑((q + 1).choose m) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) / (↑(q + 1)! : ℚ)

Tactic:
rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one,
      mul_assoc _ _ (q.succ ! : ℚ), mul_comm _ (q.succ ! : ℚ), ← mul_assoc, div_mul_eq_mul_div]

Premises used: Nat.succ_eq_add_one, mul_assoc, LT.lt.le, div_mul_eq_mul_div, eq_comm, Nat.cast, div_eq_iff, Nat.factorial, mul_comm, Nat.succ, Nat.choose_eq_factorial_div_factorial
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h_1 : m ∈ range q.succ
h : m < q + 1
h₁ :
  bernoulli m * (↑((q + 1)! / (m ! * (q + 1 - m)!)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) =
    bernoulli m * (↑q.succ ! : ℚ) / (↑m ! : ℚ) * (HPow.hPow (α := ℚ) (↑n : ℚ) (q - m + 1) * (↑(q - m + 1)! : ℚ)⁻¹)
⊢ bernoulli m * (↑((q + 1)! / (m ! * (q + 1 - m)!)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) =
    HMul.hMul (β := ℚ) (bernoulli m * (↑q.succ ! : ℚ) / (↑m ! : ℚ))
      ((coeff (q - m + 1) : (a : ℚ⟦X⟧) → ℚ)
          (({
                  toFun := fun (f : ℚ⟦X⟧) ↦
                    PowerSeries.mk fun (n_1 : ℕ) ↦
                      HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑n : ℚ) n_1) ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ) f : ℚ),
                  map_one' := ⋯, map_mul' := ⋯ } :
                (a : ℚ⟦X⟧) → ℚ⟦X⟧)
              (exp ℚ) :
            ℚ⟦X⟧) :
        ℚ)

Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, Algebra.algebraMap_self, one_div,
      map_inv₀, map_natCast, coeff_mk]

Premises used: Algebra.algebraMap_self, OneHom.coe_mk, map_inv₀, PowerSeries.coeff_mk, PowerSeries.coeff_exp, MonoidHom.coe_mk, map_natCast, one_div
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h_1 : m ∈ range q.succ
h : m < q + 1
h₁ :
  bernoulli m * ((↑(q + 1)! : ℚ) / HMul.hMul (α := ℚ) (↑m ! : ℚ) (↑(q + 1 - m)! : ℚ)) *
      HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) =
    bernoulli m * (↑q.succ ! : ℚ) / HMul.hMul (α := ℚ) (↑m ! : ℚ) (↑(q + 1 - m)! : ℚ) *
      HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m)
h₂ : m ! * (q + 1 - m)! ∣ (q + 1)!
h₃ : Ne (α := ℚ) (↑(m ! * (q + 1 - m)!) : ℚ) 0
⊢ bernoulli m * (↑((q + 1)! / (m ! * (q + 1 - m)!)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) =
    bernoulli m * (↑q.succ ! : ℚ) / (↑m ! : ℚ) * (HPow.hPow (α := ℚ) (↑n : ℚ) (q - m + 1) * (↑(q - m + 1)! : ℚ)⁻¹)

Tactic:
rw [mul_comm ((n : ℚ) ^ (q - m + 1)), ← mul_assoc _ _ ((n : ℚ) ^ (q - m + 1)), ← one_div,
      mul_one_div, div_div, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_div, cast_mul]

Premises used: mul_assoc, HSub.hSub, Nat.cast, Nat.cast_div, tsub_add_eq_add_tsub, Nat.cast_mul, HPow.hPow, mul_one_div, HAdd.hAdd, Nat.le_of_lt_succ, one_div, mul_comm, div_div, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h_1 : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ((↑(q + 1)! : ℚ) / HMul.hMul (α := ℚ) (↑m ! : ℚ) (↑(q + 1 - m)! : ℚ)) *
      HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) =
    bernoulli m * (↑q.succ ! : ℚ) / HMul.hMul (α := ℚ) (↑m ! : ℚ) (↑(q + 1 - m)! : ℚ) *
      HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h_1 : m ∈ range q.succ
h : m < q + 1
⊢ m ! * (q + 1 - m)! ∣ (q + 1)!

Tactic:
factorial_mul_factorial_dvd_factorial h.le

Premises used: LT.lt.le, Nat.factorial_mul_factorial_dvd_factorial
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h_1 : m ∈ range q.succ
h : m < q + 1
⊢ m ! * (q + 1 - m)! ∣ (q + 1)!

Tactic:
exact factorial_mul_factorial_dvd_factorial h.le

Premises used: LT.lt.le, Nat.factorial_mul_factorial_dvd_factorial
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h_1 : m ∈ range q.succ
h : m < q + 1
⊢ Ne (α := ℚ) (↑(m ! * (q + 1 - m)!) : ℚ) 0

Tactic:
simp [factorial_ne_zero]

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
⊢ 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)! : ℚ)

Tactic:
have h_cauchy :
    ((mk fun p => bernoulli p / p !) * mk fun q => coeff (q + 1) (exp ℚ ^ n)) =
      mk fun p => ∑ i ∈ range (p + 1),
          bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)! := by
    ext q : 1
    let f a b := bernoulli a / a ! * coeff (b + 1) (exp ℚ ^ n)
    -- key step: use `PowerSeries.coeff_mul` and then rewrite sums
    simp only [f, coeff_mul, coeff_mk, sum_antidiagonal_eq_sum_range_succ f]
    apply sum_congr rfl
    intro m h
    simp only [exp_pow_eq_rescale_exp, rescale, RingHom.coe_mk]
    -- manipulate factorials and binomial coefficients
    have h : m < q + 1 := by simpa using h
    rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one,
      mul_assoc _ _ (q.succ ! : ℚ), mul_comm _ (q.succ ! : ℚ), ← mul_assoc, div_mul_eq_mul_div]
    simp only [MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, Algebra.algebraMap_self, one_div,
      map_inv₀, map_natCast, coeff_mk]
    rw [mul_comm ((n : ℚ) ^ (q - m + 1)), ← mul_assoc _ _ ((n : ℚ) ^ (q - m + 1)), ← one_div,
      mul_one_div, div_div, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_div, cast_mul]
    · ring
    · exact factorial_mul_factorial_dvd_factorial h.le
    · simp [factorial_ne_zero]
-- Module: Mathlib.NumberTheory.Bernoulli
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)! : ℚ)
this :
  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)! : ℚ))
rw :
  Eq (α := ℚ) (∑ i ∈ range n, HPow.hPow (α := ℚ) (↑i : ℚ) p * (↑p ! : ℚ)⁻¹)
    (∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))
⊢ ∑ 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:
rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]

Premises used: div_eq_mul_inv, div_eq_iff, Finset.sum_mul
-- Module: Mathlib.NumberTheory.Bernoulli
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)! : ℚ)
this :
  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)! : ℚ))
⊢ ∀ (n_1 : ℕ),
    Eq (α := ℚ)
      ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ)
          (PowerSeries.mk fun (p : ℕ) ↦
            ∑ k ∈ range n,
              HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑k : ℚ) p) ((algebraMap ℚ ℚ : (a : ℚ) → ℚ) (↑p ! : ℚ)⁻¹ : ℚ)) :
        ℚ)
      ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ)
          (PowerSeries.mk fun (p : ℕ) ↦
            ∑ i ∈ range (p + 1),
              bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)) :
        ℚ)

Tactic:
rw [PowerSeries.ext_iff] at this

Premises used: PowerSeries.ext_iff
-- Module: Mathlib.NumberTheory.Bernoulli
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)! : ℚ)
this :
  ∀ (n_1 : ℕ),
    Eq (α := ℚ)
      ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ)
          (PowerSeries.mk fun (p : ℕ) ↦
            ∑ k ∈ range n,
              HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑k : ℚ) p) ((algebraMap ℚ ℚ : (a : ℚ) → ℚ) (↑p ! : ℚ)⁻¹ : ℚ)) :
        ℚ)
      ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ)
          (PowerSeries.mk fun (p : ℕ) ↦
            ∑ i ∈ range (p + 1),
              bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)) :
        ℚ)
⊢ Eq (α := ℚ) (∑ i ∈ range n, HPow.hPow (α := ℚ) (↑i : ℚ) p * (↑p ! : ℚ)⁻¹)
    (∑ i ∈ range (p + 1),
      bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ))

Tactic:
simpa using this p
-- Module: Mathlib.NumberTheory.Bernoulli
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)! : ℚ)
fun :
  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)! : ℚ))
⊢ ∑ 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:
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
-- Module: Mathlib.NumberTheory.Bernoulli
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)! : ℚ)
simp :
  ∃ (x : ℕ),
    ¬Eq (α := ℚ)
        ((coeff x : (a : ℚ⟦X⟧) → ℚ)
            (HSub.hSub (α := ℚ⟦X⟧)
              (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ))) 1) :
          ℚ)
        ((coeff x : (a : ℚ⟦X⟧) → ℚ) 0 : ℚ)
⊢ exp ℚ - 1 ≠ 0

Tactic:
simp only [exp, PowerSeries.ext_iff, Ne, not_forall]

Premises used: Ne, PowerSeries.ext_iff, PowerSeries.exp, Classical.not_forall
-- Module: Mathlib.NumberTheory.Bernoulli
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)! : ℚ)
h :
  ¬Eq (α := ℚ)
      ((coeff 1 : (a : ℚ⟦X⟧) → ℚ)
          (HSub.hSub (α := ℚ⟦X⟧)
            (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ))) 1) :
        ℚ)
      ((coeff 1 : (a : ℚ⟦X⟧) → ℚ) 0 : ℚ)
⊢ ∃ (x : ℕ),
    ¬Eq (α := ℚ)
        ((coeff x : (a : ℚ⟦X⟧) → ℚ)
            (HSub.hSub (α := ℚ⟦X⟧)
              (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ))) 1) :
          ℚ)
        ((coeff x : (a : ℚ⟦X⟧) → ℚ) 0 : ℚ)

Tactic:
use 1
-- Module: Mathlib.NumberTheory.Bernoulli
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 (α := ℚ)
      ((coeff 1 : (a : ℚ⟦X⟧) → ℚ)
          (HSub.hSub (α := ℚ⟦X⟧)
            (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ ℚ : (a : ℚ) → ℚ) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ))) 1) :
        ℚ)
      ((coeff 1 : (a : ℚ⟦X⟧) → ℚ) 0 : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
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)! : ℚ)
⊢ exp ℚ - 1 ≠ 0

Tactic:
have hexp : exp ℚ - 1 ≠ 0 := by
      simp only [exp, PowerSeries.ext_iff, Ne, not_forall]
      use 1
      simp
-- Module: Mathlib.NumberTheory.Bernoulli
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⟧) ((C : (a : ℚ) → ℚ⟦X⟧) ((constantCoeff : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ) : ℚ⟦X⟧) (1 : ℚ⟦X⟧)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
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⟧) ((C : (a : ℚ) → ℚ⟦X⟧) ((constantCoeff : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ) : ℚ⟦X⟧) (1 : ℚ⟦X⟧)

Tactic:
have h_const : C (constantCoeff (exp ℚ ^ n)) = 1 := by simp
-- Module: Mathlib.NumberTheory.Bernoulli
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))
rw₁ 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))
⊢ exp ℚ ^ n - 1 = 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]

Premises used: PowerSeries.sub_const_eq_X_mul_shift
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ 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]
-- Module: Mathlib.NumberTheory.Bernoulli
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))
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)! : ℚ)
⊢ 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)! : ℚ))

Tactic:
rw [← mul_right_inj' hexp, mul_comm]

Premises used: mul_comm, mul_right_inj'
-- Module: Mathlib.NumberTheory.Bernoulli
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))
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)! : ℚ)
⊢ (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 [← exp_pow_sum, geom_sum_mul, h_r, ← bernoulliPowerSeries_mul_exp_sub_one,
      bernoulliPowerSeries, mul_right_comm]

Premises used: bernoulliPowerSeries_mul_exp_sub_one, PowerSeries.exp_pow_sum, geom_sum_mul, mul_right_comm, bernoulliPowerSeries
-- Module: Mathlib.NumberTheory.Bernoulli
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))
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)! : ℚ)
⊢ 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:
simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false]

Premises used: mul_eq_mul_left_iff, mul_comm, or_false