-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- First step in Bojanić's proof of Mahler's theorem (equation (10) of [bojanic74]): rewrite
`Δ^[n + R] f 0` in a shape that makes it easy to bound `p`-adically. -/
private lemma bojanic_mahler_step1 [AddCommMonoidWithOne M] [AddCommGroup G] (f : M → G)
    (n : ℕ) {R : ℕ} (hR : 1 ≤ R) :
    Δ_[1]^[n + R] f 0 = -∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 +
      ∑ k ∈ range (n + 1), ((-1 : ℤ) ^ (n - k) * n.choose k) • (f (k + R) - f k)

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
⊢ Δ_[1]^[n + R] f 0 =
    -∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 +
      ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Tactic:
have aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0 := by
  rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]

Result:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 =
    -∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 +
      ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 - Δ_[1]^[n] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Tactic:
have : ∑ k ∈ Finset.range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f R := by
  simpa only [← Function.iterate_add_apply, add_comm, nsmul_one, add_zero] using
    (shift_eq_sum_fwdDiff_iter 1 (Δ_[1]^[n] f) R 0).symm

Result:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
this : ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f ↑R
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 - Δ_[1]^[n] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ n + R = n + (R - 1 + 1)

Tactic:
omega

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f ↑R

Tactic:
simpa only [← Function.iterate_add_apply, add_comm, nsmul_one, add_zero] using
  (shift_eq_sum_fwdDiff_iter 1 (Δ_[1]^[n] f) R 0).symm

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
⊢ Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0

Tactic:
rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 =
    -∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 +
      ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Tactic:
rw [neg_add_eq_sub, eq_sub_iff_add_eq, add_comm, aux, (by omega : n + R = (n + ((R - 1) + 1))),
  ← sum_range_succ, Nat.sub_add_cancel hR,
  ← sub_eq_iff_eq_add.mpr (sum_range_succ' (fun x ↦ R.choose x • Δ_[1]^[n + x] f 0) R), add_zero,
  Nat.choose_zero_right, one_smul]

Result:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 - Δ_[1]^[n] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
this : ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f ↑R
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 - Δ_[1]^[n] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Tactic:
simp only [this, fwdDiff_iter_eq_sum_shift (1 : M) f n, mul_comm, nsmul_one, mul_smul, add_comm,
  add_zero, smul_sub, sum_sub_distrib]

Result:
no goals