R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
⊢ ∑ i in Ico m n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i in Ico m n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
have h₁ : (∑ i in Ico (m + 1) n, f i • G i) = ∑ i in Ico m (n - 1), f (i + 1) • G (i + 1) := by
  rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
  simp only [ge_iff_le, tsub_le_iff_right, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
    tsub_eq_zero_iff_le, add_tsub_cancel_right]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
⊢ ∑ i in Ico m n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
⊢ ∑ i in Ico m n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
have h₂ :
  (∑ i in Ico (m + 1) n, f i • G (i + 1)) =
    (∑ i in Ico m (n - 1), f i • G (i + 1)) + f (n - 1) • G n - f m • G (m + 1) := by
  rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_pred_of_lt hmn),
    Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
⊢ f m • g m + ∑ k in Ico (m + 1) n, f k • g k =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
⊢ ∑ i in Ico m n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
rw [sum_eq_sum_Ico_succ_bot hmn]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
⊢ f m • g m + ∑ k in Ico (m + 1) n, f k • g k =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
⊢ f m • g m + ∑ k in Ico (m + 1) n, f k • g k =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
have h₃: (Finset.sum (Ico (m + 1) n) fun i => f i • g i) =
           (Finset.sum (Ico (m + 1) n) fun i =>
              f i • ((Finset.sum (Finset.range (i + 1)) g) -
                      (Finset.sum (Finset.range i) g))) := by
  congr; funext; rw [← sum_range_succ_sub_sum g]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
⊢ f m • g m + ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
⊢ f m • g m + ∑ k in Ico (m + 1) n, f k • g k =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
rw [h₃]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
⊢ f m • g m +
      (∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
          f m • ∑ i in range (m + 1), g i -
        ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
⊢ f m • g m + ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
⊢ f m • g m +
      (∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
          f m • ∑ i in range (m + 1), g i -
        ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
⊢ f m • g m +
      (∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
          f m • ∑ i in range (m + 1), g i -
        ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
have h₄ : ((((Finset.sum (Ico m (n - 1)) fun i => f i • Finset.sum (range (i + 1)) fun i => g i) +
    f (n - 1) • Finset.sum (range n) fun i => g i) -
    f m • Finset.sum (range (m + 1)) fun i => g i) -
    Finset.sum (Ico m (n - 1)) fun i => f (i + 1) • Finset.sum (range (i + 1)) fun i => g i) =
    f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g +
    Finset.sum (Ico m (n - 1)) (fun i => f i • (range (i + 1)).sum g -
    f (i + 1) • (range (i + 1)).sum g) := by
  rw [← add_sub, add_comm, ←add_sub, ← sum_sub_distrib]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
⊢ f m • g m +
      (f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
        ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
⊢ f m • g m +
      (∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
          f m • ∑ i in range (m + 1), g i -
        ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
rw [h₄]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
this :
  ∀ (i : ℕ),
    f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i in range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
        ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
⊢ f m • g m +
      (f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
        ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
have : ∀ i, f i • G (i + 1) - f (i + 1) • G (i + 1) = -((f (i + 1) - f i) • G (i + 1)) := by
  intro i
  rw [sub_smul]
  abel
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
this :
  ∀ (i : ℕ),
    f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i in range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • Finset.sum (range n) g - (f m • ∑ x in range m, g x + f m • g m) +
        -∑ x in Ico m (n - 1), ((f (x + 1) - f x) • ∑ x in range x, g x + (f (x + 1) - f x) • g x)) =
    f (n - 1) • ∑ x in range n, g x - f m • ∑ x in range m, g x -
      ∑ x in Ico m (n - 1), ((f (x + 1) - f x) • ∑ x in range x, g x + (f (x + 1) - f x) • g x)
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
this :
  ∀ (i : ℕ),
    f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i in range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
        ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)) =
    f (n - 1) • ∑ i in range n, g i - f m • ∑ i in range m, g i -
      ∑ i in Ico m (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
simp_rw [this, sum_neg_distrib, sum_range_succ, smul_add]
no goals
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
this :
  ∀ (i : ℕ),
    f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i in range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • Finset.sum (range n) g - (f m • ∑ x in range m, g x + f m • g m) +
        -∑ x in Ico m (n - 1), ((f (x + 1) - f x) • ∑ x in range x, g x + (f (x + 1) - f x) • g x)) =
    f (n - 1) • ∑ x in range n, g x - f m • ∑ x in range m, g x -
      ∑ x in Ico m (n - 1), ((f (x + 1) - f x) • ∑ x in range x, g x + (f (x + 1) - f x) • g x)
abel
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ x in Ico m (n - 1), f (x + 1) • ∑ i in range (x + 1), g i =
    ∑ i in Ico m (n - 1 + 1 - 1), f (i + 1) • ∑ i in range (i + 1), g i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
no goals
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ x in Ico m (n - 1), f (x + 1) • ∑ i in range (x + 1), g i =
    ∑ i in Ico m (n - 1 + 1 - 1), f (i + 1) • ∑ i in range (i + 1), g i
simp only [ge_iff_le, tsub_le_iff_right, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
  tsub_eq_zero_iff_le, add_tsub_cancel_right]
no goals
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
⊢ ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_pred_of_lt hmn),
  Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]
case e_f
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
⊢ (fun i => f i • g i) = fun i => f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
⊢ ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
congr
case e_f.h
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
x✝ : ℕ
⊢ f x✝ • g x✝ = f x✝ • (Finset.sum (range (x✝ + 1)) g - Finset.sum (range x✝) g)
case e_f
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
⊢ (fun i => f i • g i) = fun i => f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
funext
no goals
case e_f.h
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
x✝ : ℕ
⊢ f x✝ • g x✝ = f x✝ • (Finset.sum (range (x✝ + 1)) g - Finset.sum (range x✝) g)
rw [← sum_range_succ_sub_sum g]
no goals
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
⊢ ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
rw [← add_sub, add_comm, ←add_sub, ← sum_sub_distrib]
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
i : ℕ
⊢ f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
    -((f (i + 1) - f i) • ∑ i in range (i + 1), g i)
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
⊢ ∀ (i : ℕ),
    f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i in range (i + 1), g i)
intro i
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
i : ℕ
⊢ f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
    -(f (i + 1) • ∑ i in range (i + 1), g i - f i • ∑ i in range (i + 1), g i)
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
i : ℕ
⊢ f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
    -((f (i + 1) - f i) • ∑ i in range (i + 1), g i)
rw [sub_smul]
no goals
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i in Ico (m + 1) n, f i • ∑ i in range i, g i = ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i
h₂ :
  ∑ i in Ico (m + 1) n, f i • ∑ i in range (i + 1), g i =
    ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
      f m • ∑ i in range (m + 1), g i
h₃ :
  ∑ i in Ico (m + 1) n, f i • g i = ∑ i in Ico (m + 1) n, f i • (Finset.sum (range (i + 1)) g - Finset.sum (range i) g)
h₄ :
  ∑ i in Ico m (n - 1), f i • ∑ i in range (i + 1), g i + f (n - 1) • ∑ i in range n, g i -
        f m • ∑ i in range (m + 1), g i -
      ∑ i in Ico m (n - 1), f (i + 1) • ∑ i in range (i + 1), g i =
    f (n - 1) • Finset.sum (range n) g - f m • Finset.sum (range (m + 1)) g +
      ∑ i in Ico m (n - 1), (f i • Finset.sum (range (i + 1)) g - f (i + 1) • Finset.sum (range (i + 1)) g)
i : ℕ
⊢ f i • ∑ i in range (i + 1), g i - f (i + 1) • ∑ i in range (i + 1), g i =
    -(f (i + 1) • ∑ i in range (i + 1), g i - f i • ∑ i in range (i + 1), g i)
abel