awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 0
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0
h₀ : ∀ b ∈ s, b ≠ a → Eq (α := ZMod n.natAbs) (↑(f b) : ZMod n.natAbs) 0
h₁ : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 0
⊢ Eq (α := ZMod n.natAbs) (∑ x ∈ s, (↑(f x) : ZMod n.natAbs)) (↑(f a) : ZMod n.natAbs)

Tactic:
apply Finset.sum_eq_single

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 0
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0
⊢ ∀ b ∈ s, b ≠ a → Eq (α := ZMod n.natAbs) (↑(f b) : ZMod n.natAbs) 0

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 0
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0
⊢ a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 0

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
rw :
  Eq.{u_2 + 1} (α := M) (∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (x + 1)) (∑ i ∈ range (x + 1), g i))
    (∑ i ∈ Ico m (n - 1 + 1 - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))

Tactic:
rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']

Premises used: Nat.one_le_of_lt, Finset.sum_Ico_add', Nat.sub_add_cancel
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ Eq.{u_2 + 1} (α := M) (∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (x + 1)) (∑ i ∈ range (x + 1), g i))
    (∑ i ∈ Ico m (n - 1 + 1 - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))

Tactic:
simp only [add_tsub_cancel_right]

Premises used: add_tsub_cancel_right
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))

Tactic:
have h₁ : (∑ i ∈ Ico (m + 1) n, f i • G i) = ∑ i ∈ 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 [add_tsub_cancel_right]
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
rw :
  ∑ i ∈ Ico m n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
rw₁ :
  ∑ i ∈ Ico m n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) =
    ∑ i ∈ Ico m (n - 1 + 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
          HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range (n - 1 + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
rw₂ :
  ∑ i ∈ Ico m n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) =
    ∑ i ∈ Ico m n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
          HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
rw₃ rw₄ :
  ∑ i ∈ Ico m n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) =
    ∑ i ∈ Ico m n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
⊢ ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)

Tactic:
rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_sub_one_of_lt hmn),
      Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]

Premises used: Finset.sum_Ico_sub_bot, pos_of_gt, Nat.le_sub_one_of_lt, Nat.sub_add_cancel, Finset.sum_Ico_succ_sub_top, sub_add_cancel
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
⊢ ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)

Tactic:
have h₂ :
    (∑ i ∈ Ico (m + 1) n, f i • G (i + 1)) =
      (∑ i ∈ 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_sub_one_of_lt hmn),
      Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
rw :
  f m • g m + ∑ k ∈ Ico (m + 1) n, f k • g k =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
⊢ ∑ i ∈ Ico m n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
rw [sum_eq_sum_Ico_succ_bot hmn]

Premises used: Finset.sum_eq_sum_Ico_succ_bot
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
k : ℕ
rw : f k • HSub.hSub (α := M) (∑ i ∈ range (k + 1), g i) (∑ i ∈ range k, g i)
| f k • g k

Tactic:
rw [← sum_range_succ_sub_sum g]

Premises used: Finset.sum_range_succ_sub_sum
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
conv :
  f m • g m + ∑ k ∈ Ico (m + 1) n, f k • HSub.hSub (α := M) (∑ i ∈ range (k + 1), g i) (∑ i ∈ range k, g i) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
⊢ f m • g m + ∑ k ∈ Ico (m + 1) n, f k • g k =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
conv in (occs := 3) (f _ • g _) => rw [← sum_range_succ_sub_sum g]

Premises used: HSMul.hSMul, Finset.sum_range_succ_sub_sum
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
simp_rw :
  f m • g m +
      (∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) +
            HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
          HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) -
        ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i)) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
⊢ f m • g m + ∑ k ∈ Ico (m + 1) n, f k • HSub.hSub (α := M) (∑ i ∈ range (k + 1), g i) (∑ i ∈ range k, g i) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]

Premises used: smul_sub, Finset.sum_sub_distrib
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
a : f m • g m
a₁ :
  ∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) -
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i)
| f m • g m +
    (∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) +
          HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
        HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
| f m • g m

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
a :
  HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) +
    ∑ x ∈ Ico m (n - 1),
      (HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) -
        HSMul.hSMul (β := M) (f (x + 1)) (∑ i ∈ range (x + 1), g i))
| ∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) -
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i)

Tactic:
rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]

Premises used: add_sub, add_comm, Finset.sum_sub_distrib
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
a :
  HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) +
    ∑ x ∈ Ico m (n - 1),
      (HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) -
        HSMul.hSMul (β := M) (f (x + 1)) (∑ i ∈ range (x + 1), g i))
| f m • g m +
    (∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) +
          HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
        HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))

Tactic:
congr; rfl; rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]

Premises used: add_sub, add_comm, Finset.sum_sub_distrib
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
conv_lhs :
  f m • g m +
      (HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) +
        ∑ x ∈ Ico m (n - 1),
          (HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) -
            HSMul.hSMul (β := M) (f (x + 1)) (∑ i ∈ range (x + 1), g i))) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (∑ x ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) +
            HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
          HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) -
        ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i)) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
conv_lhs => congr; rfl; rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]

Premises used: add_sub, add_comm, Finset.sum_sub_distrib
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
i : ℕ
rw :
  HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) - HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) =
    -(HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) -
        HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i))
⊢ HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) - HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) =
    -HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
rw [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
i : ℕ
⊢ HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) - HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) =
    -(HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) -
        HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i))

Tactic:
abel
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
⊢ ∀ (i : ℕ),
    HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
        HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) =
      -HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
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
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
this :
  ∀ (i : ℕ),
    HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
        HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) =
      -HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
simp_rw :
  f m • g m +
      (HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
          (HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) + f m • g m) +
        -∑ x ∈ Ico m (n - 1), (HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ i ∈ range x, g i) + (f (x + 1) - f x) • g x)) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ x ∈ Ico m (n - 1), (HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ i ∈ range x, g i) + (f (x + 1) - f x) • g x)
⊢ f m • g m +
      (HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i) +
        ∑ x ∈ Ico m (n - 1),
          (HSMul.hSMul (β := M) (f x) (∑ i ∈ range (x + 1), g i) -
            HSMul.hSMul (β := M) (f (x + 1)) (∑ i ∈ range (x + 1), g i))) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
simp_rw [this, sum_neg_distrib, sum_range_succ, smul_add]

Premises used: Finset.sum_neg_distrib, Finset.sum_range_succ, smul_add
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range i, g i))
    (∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i))
h₂ :
  ∑ i ∈ Ico (m + 1) n, HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) =
    ∑ i ∈ Ico m (n - 1), HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) +
        HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      HSMul.hSMul (β := M) (f m) (∑ i ∈ range (m + 1), g i)
this :
  ∀ (i : ℕ),
    HSMul.hSMul (β := M) (f i) (∑ i ∈ range (i + 1), g i) -
        HSMul.hSMul (β := M) (f (i + 1)) (∑ i ∈ range (i + 1), g i) =
      -HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
          (HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) + f m • g m) +
        -∑ x ∈ Ico m (n - 1), (HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ i ∈ range x, g i) + (f (x + 1) - f x) • g x)) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) - HSMul.hSMul (β := M) (f m) (∑ i ∈ range m, g i) -
      ∑ x ∈ Ico m (n - 1), (HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ i ∈ range x, g i) + (f (x + 1) - f x) • g x)

Tactic:
abel