awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
h :
  ∀ x ∈ Icc (↑a : ℕ) (↑b : ℕ),
    (if h : x < n then f (⟨x, h⟩ : Fin n).succ / f (⟨x, h⟩ : Fin n).castSucc else 1) =
      HDiv.hDiv (α := M) (if hi : x + 1 < n + 1 then f (⟨x + 1, hi⟩ : Fin (n + 1)) else 1)
        (if hi : x < n + 1 then f (⟨x, hi⟩ : Fin (n + 1)) else 1)
⊢ (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1) =
    f b.succ / f a.castSucc
have h₁ : f b.succ = if hi : (↑b : ℕ) + 1 < n + 1 then f ⟨(↑b : ℕ) + 1, hi⟩ else 1
Tactic: convert! Finset.prod_Icc_div (Fin.le_def.1 hab) (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
h :
  ∀ x ∈ Icc (↑a : ℕ) (↑b : ℕ),
    (if h : x < n then f (⟨x, h⟩ : Fin n).succ / f (⟨x, h⟩ : Fin n).castSucc else 1) =
      HDiv.hDiv (α := M) (if hi : x + 1 < n + 1 then f (⟨x + 1, hi⟩ : Fin (n + 1)) else 1)
        (if hi : x < n + 1 then f (⟨x, hi⟩ : Fin (n + 1)) else 1)
h₁ : f b.succ = if hi : (↑b : ℕ) + 1 < n + 1 then f ⟨(↑b : ℕ) + 1, hi⟩ else 1
⊢ (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1) =
    f b.succ / f a.castSucc
have h₂ : f a.castSucc = if hi : (↑a : ℕ) < n + 1 then f ⟨(↑a : ℕ), hi⟩ else 1
Tactic: convert! Finset.prod_Icc_div (Fin.le_def.1 hab) (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
x : ℕ
h : x ∈ Icc (↑a : ℕ) (↑b : ℕ)
⊢ (if h : x < n then f (⟨x, h⟩ : Fin n).succ / f (⟨x, h⟩ : Fin n).castSucc else 1) =
    HDiv.hDiv (α := M) (if hi : x + 1 < n + 1 then f (⟨x + 1, hi⟩ : Fin (n + 1)) else 1)
      (if hi : x < n + 1 then f (⟨x, hi⟩ : Fin (n + 1)) else 1)
have h : (↑a : ℕ) ≤ x ∧ x ≤ (↑b : ℕ) →
  (if h : x < n then f (⟨x + 1, sorry⟩ : Fin (n + 1)) / f (⟨x, sorry⟩ : Fin (n + 1)) else 1) =
    HDiv.hDiv (α := M) (if h : x < n then f (⟨x + 1, sorry⟩ : Fin (n + 1)) else 1)
      (if h : x ≤ n then f (⟨x, sorry⟩ : Fin (n + 1)) else 1)
Tactic: simp_all
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = if hi : (↑a : ℕ) < n + 1 then f ⟨(↑a : ℕ), hi⟩ else 1
have h : f a.castSucc = f ⟨(↑a : ℕ), sorry⟩
Tactic: simp only [Order.lt_add_one_iff, is_le', ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [MOD n]
have nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]),
  (List.map f []).prod ≡ (List.map g []).prod [MOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]),
    (List.map f []).prod ≡ (List.map g []).prod [MOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [MOD n]
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : ∀ x ∈ tail, f x ≡ g x [MOD n]), (List.map f tail).prod ≡ (List.map g tail).prod [MOD n]) →
    ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [MOD n]),
      (List.map f (head :: tail)).prod ≡ (List.map g (head :: tail)).prod [MOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [MOD n]
have nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]),
  (List.map f []).sum ≡ (List.map g []).sum [MOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]),
    (List.map f []).sum ≡ (List.map g []).sum [MOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [MOD n]
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : ∀ x ∈ tail, f x ≡ g x [MOD n]), (List.map f tail).sum ≡ (List.map g tail).sum [MOD n]) →
    ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [MOD n]),
      (List.map f (head :: tail)).sum ≡ (List.map g (head :: tail)).sum [MOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [MOD n]
have mk : ∀ (l : List α)
  (h :
    ∀ (x : α),
      Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x → f x ≡ g x [MOD n]),
  (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod [MOD n]
Tactic: rcases s with ⟨l⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]
have mk : ∀ (l : List α)
  (h :
    ∀ (x : α),
      Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x → f x ≡ g x [MOD n]),
  (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum [MOD n]
Tactic: rcases s with ⟨l⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]
have simp : ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1),
  Eq (α := ZMod n) (∏ i ∈ s, (↑(f i) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 1)
Tactic: simp only [← ZMod.natCast_eq_natCast_iff, cast_one, cast_prod, apply_ite Nat.cast] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 1 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ f a [MOD n]
have simp : ∀ (ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 1) (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1),
  Eq (α := ZMod n) (∏ i ∈ s, (↑(f i) : ZMod n)) (↑(f a) : ZMod n)
Tactic: simp only [← ZMod.natCast_eq_natCast_iff, cast_one, cast_prod] at *
Cleared hypotheses: ha, hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [MOD n]
have simp : ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0),
  Eq (α := ZMod n) (∑ x ∈ s, (↑(f x) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 0)
Tactic: simp only [← ZMod.natCast_eq_natCast_iff, cast_zero, cast_sum, apply_ite Nat.cast] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ f a [MOD n]
have simp : ∀ (ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 0) (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0),
  Eq (α := ZMod n) (∑ x ∈ s, (↑(f x) : ZMod n)) (↑(f a) : ZMod n)
Tactic: simp only [← ZMod.natCast_eq_natCast_iff, cast_zero, cast_sum] at *
Cleared hypotheses: ha, hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [ZMOD n]
have nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]),
  (List.map f []).prod ≡ (List.map g []).prod [ZMOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]),
    (List.map f []).prod ≡ (List.map g []).prod [ZMOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [ZMOD n]
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : ∀ x ∈ tail, f x ≡ g x [ZMOD n]), (List.map f tail).prod ≡ (List.map g tail).prod [ZMOD n]) →
    ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [ZMOD n]),
      (List.map f (head :: tail)).prod ≡ (List.map g (head :: tail)).prod [ZMOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]
have nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]),
  (List.map f []).sum ≡ (List.map g []).sum [ZMOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]),
    (List.map f []).sum ≡ (List.map g []).sum [ZMOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : ∀ x ∈ tail, f x ≡ g x [ZMOD n]), (List.map f tail).sum ≡ (List.map g tail).sum [ZMOD n]) →
    ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [ZMOD n]),
      (List.map f (head :: tail)).sum ≡ (List.map g (head :: tail)).sum [ZMOD n]
Tactic: induction l
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [ZMOD n]
have mk : ∀ (l : List α)
  (h :
    ∀ (x : α),
      Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x →
        f x ≡ g x [ZMOD n]),
  (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod [ZMOD n]
Tactic: rcases s with ⟨l⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [ZMOD n]
have mk : ∀ (l : List α)
  (h :
    ∀ (x : α),
      Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x →
        f x ≡ g x [ZMOD n]),
  (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum [ZMOD n]
Tactic: rcases s with ⟨l⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [ZMOD n]
have simp : ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1),
  Eq (α := ZMod n.natAbs) (∏ i ∈ s, (↑(f i) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 1)
Tactic: simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_one, cast_prod,
    apply_ite Int.cast] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 1 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ f a [ZMOD n]
have simp : ∀ (ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 1)
  (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1),
  Eq (α := ZMod n.natAbs) (∏ i ∈ s, (↑(f i) : ZMod n.natAbs)) (↑(f a) : ZMod n.natAbs)
Tactic: simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_one, cast_prod] at *
Cleared hypotheses: ha, hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [ZMOD n]
have simp : ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0),
  Eq (α := ZMod n.natAbs) (∑ x ∈ s, (↑(f x) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 0)
Tactic: simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_zero, cast_sum,
    apply_ite Int.cast] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.ModEq (goal)
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ f a [ZMOD n]
have simp : ∀ (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),
  Eq (α := ZMod n.natAbs) (∑ x ∈ s, (↑(f x) : ZMod n.natAbs)) (↑(f a) : ZMod n.natAbs)
Tactic: simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_zero, cast_sum] at *
Cleared hypotheses: ha, hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Module (goal)
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))
have 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))
Tactic: rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Module (hypothesis)
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
⊢ ∑ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Module (goal)
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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Module (goal)
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)
⊢ ∑ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Module (goal)
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)
⊢ ∑ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Module (goal)
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)
⊢ ∑ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Module (hypothesis)
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 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)
have 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)
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]