-- Mathlib/Algebra/Group/ForwardDiff.lean
theorem fwdDiff_iter_eq_sum_shift (f : M → G) (n : ℕ) (y : M) :
    Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), ((-1 : ℤ) ^ (n - k) * n.choose k) • f (y + k • h)

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ fwdDiffₗ M G h = shiftₗ M G h - 1

Tactic:
simp only [shiftₗ, add_sub_cancel_right]

Result:
no goals

Proof state:
case h.e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    (∑ m ∈ range (n + 1), shiftₗ M G h ^ m * (-1) ^ (n - m) * ↑(n.choose m)) f y

Tactic:
rw [LinearMap.sum_apply, sum_apply]

Result:
case h.e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    ∑ c ∈ range (n + 1), (shiftₗ M G h ^ c * (-1) ^ (n - c) * ↑(n.choose c)) f y

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
have : Commute (shiftₗ M G h) (-1) := (Commute.one_right _).neg_right

Result:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Proof state:
case h.e'_2.h.e'_2.h.e'_5
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ shiftₗ M G h - 1 = shiftₗ M G h + -1

Tactic:
simp only [sub_eq_add_neg]

Result:
no goals

Proof state:
case h.e'_3.e_f.h
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * (-1) ^ (n - k) * ↑(n.choose k)) f y

Tactic:
rw [mul_assoc, LinearMap.mul_apply, this, Module.End.intCast_apply, LinearMap.map_smul,
  Pi.smul_apply, shiftₗ_pow_apply]

Result:
no goals

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

Tactic:
have : fwdDiffₗ M G h = shiftₗ M G h - 1 := by simp only [shiftₗ, add_sub_cancel_right]

Result:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Proof state:
case h.e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    ∑ c ∈ range (n + 1), (shiftₗ M G h ^ c * (-1) ^ (n - c) * ↑(n.choose c)) f y

Tactic:
congr 1 with k

Result:
case h.e'_3.e_f.h
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
k : ℕ
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * (-1) ^ (n - k) * ↑(n.choose k)) f y

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
convert congr_fun (LinearMap.congr_fun (this.add_pow n) f) y using 3

Result:
case h.e'_2.h.e'_2.h.e'_5
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ shiftₗ M G h - 1 = shiftₗ M G h + -1

case h.e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    (∑ m ∈ range (n + 1), shiftₗ M G h ^ m * (-1) ^ (n - m) * ↑(n.choose m)) f y

Proof state:
case h.e'_3.e_f.h
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
k : ℕ
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * (-1) ^ (n - k) * ↑(n.choose k)) f y

Tactic:
have : ((-1) ^ (n - k) * n.choose k : Module.End ℤ (M → G))
          = ↑((-1) ^ (n - k) * n.choose k : ℤ) := by norm_cast

Result:
case h.e'_3.e_f.h
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * (-1) ^ (n - k) * ↑(n.choose k)) f y

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
k : ℕ
⊢ (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))

Tactic:
norm_cast

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
rw [← coe_fwdDiffₗ, this, ← LinearMap.pow_apply]

Result:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)