A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ ∑ k in range n, ↑k ^ p = ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
⊢ ∑ k in range n, ↑k ^ p = ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
have hne : ∀ m : ℕ, (m ! : ℚ) ≠ 0 := fun m => by exact_mod_cast factorial_ne_zero m
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ ∑ x in range (p + 1), bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) / ↑(p + 1)! * ↑p ! =
    ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ ∑ k in range n, ↑k ^ p = ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
rw [hps, sum_mul]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
x : ℕ
x✝ : x ∈ range (p + 1)
⊢ bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) / ↑(p + 1)! * ↑p ! =
    bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) / (↑p + 1)
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ ∑ x in range (p + 1), bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) / ↑(p + 1)! * ↑p ! =
    ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
refine' sum_congr rfl fun x _ => _
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
x : ℕ
x✝ : x ∈ range (p + 1)
⊢ bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) * ↑p ! * (↑p + 1) =
    bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) * ((↑p + 1) * ↑p !)
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
x : ℕ
x✝ : x ∈ range (p + 1)
⊢ bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) / ↑(p + 1)! * ↑p ! =
    bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) / (↑p + 1)
field_simp [mul_right_comm _ ↑p !, ← mul_assoc _ _ ↑p !, cast_add_one_ne_zero, hne]
no goals
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
x : ℕ
x✝ : x ∈ range (p + 1)
⊢ bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) * ↑p ! * (↑p + 1) =
    bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) * ((↑p + 1) * ↑p !)
ring
no goals
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p m : ℕ
⊢ ↑m ! ≠ 0
exact_mod_cast factorial_ne_zero m
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
⊢ ↑(coeff ℚ q) ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    ↑(coeff ℚ q)
      (PowerSeries.mk fun p =>
        ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
ext q : 1
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ ↑(coeff ℚ q) ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    ↑(coeff ℚ q)
      (PowerSeries.mk fun p =>
        ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
⊢ ↑(coeff ℚ q) ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    ↑(coeff ℚ q)
      (PowerSeries.mk fun p =>
        ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
let f a b := bernoulli a / a ! * coeff ℚ (b + 1) (exp ℚ ^ n)
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ ∑ x in range (succ q), bernoulli x / ↑x ! * ↑(coeff ℚ (q - x + 1)) (exp ℚ ^ n) =
    ∑ i in range (q + 1), bernoulli i * ↑(Nat.choose (q + 1) i) * ↑n ^ (q + 1 - i) / ↑(q + 1)!
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ ↑(coeff ℚ q) ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    ↑(coeff ℚ q)
      (PowerSeries.mk fun p =>
        ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
simp only [coeff_mul, coeff_mk, cast_mul, sum_antidiagonal_eq_sum_range_succ f]
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ ∀ (x : ℕ),
    x ∈ range (succ q) →
      bernoulli x / ↑x ! * ↑(coeff ℚ (q - x + 1)) (exp ℚ ^ n) =
        bernoulli x * ↑(Nat.choose (q + 1) x) * ↑n ^ (q + 1 - x) / ↑(q + 1)!
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ ∑ x in range (succ q), bernoulli x / ↑x ! * ↑(coeff ℚ (q - x + 1)) (exp ℚ ^ n) =
    ∑ i in range (q + 1), bernoulli i * ↑(Nat.choose (q + 1) i) * ↑n ^ (q + 1 - i) / ↑(q + 1)!
apply sum_congr rfl
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range (succ q)
⊢ bernoulli m / ↑m ! * ↑(coeff ℚ (q - m + 1)) (exp ℚ ^ n) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ ∀ (x : ℕ),
    x ∈ range (succ q) →
      bernoulli x / ↑x ! * ↑(coeff ℚ (q - x + 1)) (exp ℚ ^ n) =
        bernoulli x * ↑(Nat.choose (q + 1) x) * ↑n ^ (q + 1 - x) / ↑(q + 1)!
intros m h
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range (succ q)
⊢ bernoulli m / ↑m ! * ↑(coeff ℚ (q - m + 1)) (exp ℚ ^ n) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range (succ q)
⊢ bernoulli m / ↑m ! * ↑(coeff ℚ (q - m + 1)) (exp ℚ ^ n) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
simp only [Finset.mem_range]
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range (succ q)
⊢ bernoulli m / ↑m ! *
      ↑(coeff ℚ (q - m + 1))
        (↑{
              toOneHom :=
                { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                  map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : PowerSeries ℚ),
                    OneHom.toFun
                        { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                          map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          g) }
          (exp ℚ)) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range (succ q)
⊢ bernoulli m / ↑m ! * ↑(coeff ℚ (q - m + 1)) (exp ℚ ^ n) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
simp only [exp_pow_eq_rescale_exp, rescale, one_div, coeff_mk, RingHom.coe_mk, coeff_exp,
  RingHom.id_apply, cast_mul, algebraMap_rat_rat]
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m / ↑m ! *
      ↑(coeff ℚ (q - m + 1))
        (↑{
              toOneHom :=
                { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                  map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : PowerSeries ℚ),
                    OneHom.toFun
                        { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                          map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          g) }
          (exp ℚ)) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range (succ q)
⊢ bernoulli m / ↑m ! *
      ↑(coeff ℚ (q - m + 1))
        (↑{
              toOneHom :=
                { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                  map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : PowerSeries ℚ),
                    OneHom.toFun
                        { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                          map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          g) }
          (exp ℚ)) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
simp at h
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑(succ q)! / ↑m ! *
      ↑(coeff ℚ (q - m + 1))
        (↑{
              toOneHom :=
                { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                  map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : PowerSeries ℚ),
                    OneHom.toFun
                        { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                          map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          g) }
          (exp ℚ))
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m / ↑m ! *
      ↑(coeff ℚ (q - m + 1))
        (↑{
              toOneHom :=
                { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                  map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : PowerSeries ℚ),
                    OneHom.toFun
                        { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                          map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          g) }
          (exp ℚ)) =
    bernoulli m * ↑(Nat.choose (q + 1) m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
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]
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑(succ q)! / ↑m ! * (↑n ^ (q - m + 1) * (↑(q - m + 1)!)⁻¹)
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑(succ q)! / ↑m ! *
      ↑(coeff ℚ (q - m + 1))
        (↑{
              toOneHom :=
                { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                  map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (f g : PowerSeries ℚ),
                    OneHom.toFun
                        { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                          map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                        (f * g) =
                      OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          f *
                        OneHom.toFun
                          { toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f,
                            map_one' := (_ : (fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * ↑(coeff ℚ n_1) f) 1 = 1) }
                          g) }
          (exp ℚ))
simp only [add_eq, add_zero, ge_iff_le, IsUnit.mul_iff, Nat.isUnit_iff, succ.injEq, cast_mul,
  cast_succ, MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, Algebra.id.map_eq_id, one_div,
  map_inv₀, map_natCast, coeff_mk, mul_inv_rev]
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m * (↑(q + 1)! / (↑m ! * ↑(q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑(succ q)! / (↑m ! * ↑(q + 1 - m)!) * ↑n ^ (q + 1 - m)

case h.n_dvd
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ m ! * (q + 1 - m)! ∣ (q + 1)!

case h.n_nonzero
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ ↑(m ! * (q + 1 - m)!) ≠ 0
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑(succ q)! / ↑m ! * (↑n ^ (q - m + 1) * (↑(q - m + 1)!)⁻¹)
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]
no goals
case h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ bernoulli m * (↑(q + 1)! / (↑m ! * ↑(q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑(succ q)! / (↑m ! * ↑(q + 1 - m)!) * ↑n ^ (q + 1 - m)
ring
no goals
case h.n_dvd
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ m ! * (q + 1 - m)! ∣ (q + 1)!
exact factorial_mul_factorial_dvd_factorial h.le
no goals
case h.n_nonzero
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * ↑(coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < succ q
⊢ ↑(m ! * (q + 1 - m)!) ≠ 0
simp [hne, factorial_ne_zero]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
suffices
  (mk fun p => ∑ k in range n, (k : ℚ) ^ p * algebraMap ℚ ℚ p !⁻¹) =
    mk fun p =>
      ∑ i in 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
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
have hexp : exp ℚ - 1 ≠ 0 := by
  simp only [exp, PowerSeries.ext_iff, Ne, not_forall]
  use 1
  simp
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
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]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) * (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
rw [← mul_right_inj' hexp, mul_comm]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ x in range n, ↑(x ^ p) * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) * (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p =>
        ∑ x in range (p + 1), bernoulli x * ↑(Nat.choose (p + 1) x) * ↑(n ^ (p + 1 - x)) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) * (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
simp only [← cast_pow]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ((fun x => ℚ) (exp ℚ ^ n))) (bernoulli n_1 / ↑n_1 !)) *
        PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)) *
      (exp ((fun x => ℚ) (exp ℚ ^ n)) - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p =>
        ∑ x in range (p + 1), bernoulli x * ↑(Nat.choose (p + 1) x) * ↑(n ^ (p + 1 - x)) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ x in range n, ↑(x ^ p) * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) * (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p =>
        ∑ x in range (p + 1), bernoulli x * ↑(Nat.choose (p + 1) x) * ↑(n ^ (p + 1 - x)) / ↑(p + 1)!
rw [←exp_pow_sum,  geom_sum_mul, h_r, ← bernoulliPowerSeries_mul_exp_sub_one,
bernoulliPowerSeries, mul_right_comm]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ℚ) (bernoulli n_1 / ↑n_1 !)) *
      PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p =>
      ∑ x in range (p + 1), ↑(n ^ (p + 1 - x)) * (bernoulli x * ↑(Nat.choose (p + 1) x)) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ((fun x => ℚ) (exp ℚ ^ n))) (bernoulli n_1 / ↑n_1 !)) *
        PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)) *
      (exp ((fun x => ℚ) (exp ℚ ^ n)) - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p =>
        ∑ x in range (p + 1), bernoulli x * ↑(Nat.choose (p + 1) x) * ↑(n ^ (p + 1 - x)) / ↑(p + 1)!
simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false]
case refine'_1
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ℚ) (bernoulli n_1 / ↑n_1 !)) =
      PowerSeries.mk fun p => bernoulli p / ↑p !) ∨
    (PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)) = 0

case refine'_2
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) =
    PowerSeries.mk fun p =>
      ∑ x in range (p + 1), ↑(n ^ (p + 1 - x)) * (bernoulli x * ↑(Nat.choose (p + 1) x)) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ℚ) (bernoulli n_1 / ↑n_1 !)) *
      PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p =>
      ∑ x in range (p + 1), ↑(n ^ (p + 1 - x)) * (bernoulli x * ↑(Nat.choose (p + 1) x)) / ↑(p + 1)!
refine' Eq.trans (mul_eq_mul_right_iff.mpr _) (Eq.trans h_cauchy _)
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ x in range n, ↑x ^ p * (↑p !)⁻¹ =
    ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ k in range n, ↑k ^ p =
    (∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this✝ :
  (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  ∀ (n_1 : ℕ),
    ↑(coeff ℚ n_1) (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
      ↑(coeff ℚ n_1)
        (PowerSeries.mk fun p =>
          ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ x in range n, ↑x ^ p * (↑p !)⁻¹ =
    ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ x in range n, ↑x ^ p * (↑p !)⁻¹ =
    ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
rw [PowerSeries.ext_iff] at this
no goals
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this✝ :
  (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  ∀ (n_1 : ℕ),
    ↑(coeff ℚ n_1) (PowerSeries.mk fun p => ∑ k in range n, ↑k ^ p * ↑(algebraMap ℚ ℚ) (↑p !)⁻¹) =
      ↑(coeff ℚ n_1)
        (PowerSeries.mk fun p =>
          ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ x in range n, ↑x ^ p * (↑p !)⁻¹ =
    ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
simpa using this p
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∃ x, ¬↑(coeff ℚ x) ((PowerSeries.mk fun n => ↑(algebraMap ℚ ℚ) (1 / ↑n !)) - 1) = ↑(coeff ℚ x) 0
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ exp ℚ - 1 ≠ 0
simp only [exp, PowerSeries.ext_iff, Ne, not_forall]
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ¬↑(coeff ℚ 1) ((PowerSeries.mk fun n => ↑(algebraMap ℚ ℚ) (1 / ↑n !)) - 1) = ↑(coeff ℚ 1) 0
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∃ x, ¬↑(coeff ℚ x) ((PowerSeries.mk fun n => ↑(algebraMap ℚ ℚ) (1 / ↑n !)) - 1) = ↑(coeff ℚ x) 0
use 1
no goals
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ¬↑(coeff ℚ 1) ((PowerSeries.mk fun n => ↑(algebraMap ℚ ℚ) (1 / ↑n !)) - 1) = ↑(coeff ℚ 1) 0
simp
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_const : ↑(C ℚ) (↑(constantCoeff ℚ) (exp ℚ ^ n)) = 1
⊢ exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
⊢ exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
have h_const : C ℚ (constantCoeff ℚ (exp ℚ ^ n)) = 1 := by simp
no goals
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_const : ↑(C ℚ) (↑(constantCoeff ℚ) (exp ℚ ^ n)) = 1
⊢ exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
rw [← h_const, sub_const_eq_X_mul_shift]
no goals
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
⊢ ↑(C ℚ) (↑(constantCoeff ℚ) (exp ℚ ^ n)) = 1
simp
case refine'_1.h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ℚ) (bernoulli n_1 / ↑n_1 !)) = PowerSeries.mk fun p => bernoulli p / ↑p !
case refine'_1
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ℚ) (bernoulli n_1 / ↑n_1 !)) =
      PowerSeries.mk fun p => bernoulli p / ↑p !) ∨
    (PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)) = 0
left
no goals
case refine'_1.h
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun n_1 => ↑(algebraMap ℚ ℚ) (bernoulli n_1 / ↑n_1 !)) = PowerSeries.mk fun p => bernoulli p / ↑p !
congr
no goals
case refine'_2
A : Type ?u.791691
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => ↑(coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => ↑(coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ (PowerSeries.mk fun p => ∑ i in range (p + 1), bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) =
    PowerSeries.mk fun p =>
      ∑ x in range (p + 1), ↑(n ^ (p + 1 - x)) * (bernoulli x * ↑(Nat.choose (p + 1) x)) / ↑(p + 1)!
simp only [mul_comm, factorial, cast_succ, cast_pow]