-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
The coefficients of a Mahler series can be recovered from the sum by taking forward differences at
`0`.
-/
lemma fwdDiff_mahlerSeries (ha : Tendsto a atTop (𝓝 0)) (n) :
    Δ_[1]^[n] (mahlerSeries a) (0 : ℤ_[p]) = a n :=
  calc Δ_[1]^[n] (mahlerSeries a) 0
  -- throw away terms after the n'th
  _ = Δ_[1]^[n] (fun k ↦ ∑ j ∈ range (n + 1), k.choose j • (a j)) 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k => ↑(k.choose j)) 0 • a j = a n

Tactic:
simp only [fwdDiff_iter_choose_zero, ite_smul, one_smul, zero_smul, sum_ite_eq,
  Finset.mem_range, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ∑ x_1 ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • (0 + x • 1).choose x_1 • a x_1 =
    ∑ x ∈ range (n + 1), ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (0 + k • 1).choose x • a x

Tactic:
rw [sum_comm]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k => k.choose j • a j) 0 =
    ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k => ↑(k.choose j)) 0 • a j

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, zero_add, sum_smul, smul_assoc, Nat.cast_id,
  natCast_zsmul]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Δ_[1]^[n] (fun k => ∑ j ∈ range (n + 1), k.choose j • a j) 0 =
    ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k => k.choose j • a j) 0

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, smul_sum]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ∑ x_1 ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • (0 + x • 1).choose x_1 • a x_1 =
    ∑ x ∈ range (n + 1), ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (0 + k • 1).choose x • a x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n j : ℕ
hj : j ∈ range (n + 1)
⊢ ((-1) ^ (n - j) * ↑(n.choose j)) • (mahlerSeries a) (j • 1) =
    ((-1) ^ (n - j) * ↑(n.choose j)) • ∑ x ∈ range (n + 1), (j • 1).choose x • a x

Tactic:
rw [nsmul_one, nsmul_one,
  mahlerSeries_apply_nat ha (Nat.lt_succ.mp <| Finset.mem_range.mp hj), Nat.cast_id]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Δ_[1]^[n] (⇑(mahlerSeries a)) 0 = Δ_[1]^[n] (fun k => ∑ j ∈ range (n + 1), k.choose j • a j) 0

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, zero_add]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • (mahlerSeries a) (x • 1) =
    ∑ x ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • ∑ x_1 ∈ range (n + 1), (x • 1).choose x_1 • a x_1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • (mahlerSeries a) (x • 1) =
    ∑ x ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • ∑ x_1 ∈ range (n + 1), (x • 1).choose x_1 • a x_1

Tactic:
refine Finset.sum_congr rfl fun j hj ↦ ?_

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n j : ℕ
hj : j ∈ range (n + 1)
⊢ ((-1) ^ (n - j) * ↑(n.choose j)) • (mahlerSeries a) (j • 1) =
    ((-1) ^ (n - j) * ↑(n.choose j)) • ∑ x ∈ range (n + 1), (j • 1).choose x • a x