awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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 ∈ 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 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)
Tactic: rw [sum_eq_sum_Ico_succ_bot hmn]
-- 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))
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 : ℕ
| f k • g k
have rw : f k • HSub.hSub (α := M) (∑ i ∈ range (k + 1), g i) (∑ i ∈ range k, g i)
Tactic: rw [← sum_range_succ_sub_sum g]
-- 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))
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 + ∑ 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)
have 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)
Tactic: conv in (occs := 3) (f _ • g _) => rw [← sum_range_succ_sub_sum g]
-- 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))
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 + ∑ 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)
have 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)
Tactic: simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]
-- 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))
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 +
    (∑ 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))
have a : f m • g m
Tactic: congr
-- 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))
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
| 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))
have 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)
Tactic: congr
-- 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))
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)
| ∑ 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)
have 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))
Tactic: rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]
-- 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))
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 +
    (∑ 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))
have 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))
Tactic: congr; rfl; rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]
-- 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))
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 +
      (∑ 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)
have 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)
Tactic: conv_lhs => congr; rfl; rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]
-- 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))
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)
have 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))
Tactic: rw [sub_smul]
-- 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))
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 +
      (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)
have 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)
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
-- 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))
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 + 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)
have 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)
Tactic: simp_rw [this, sum_neg_distrib, sum_range_succ, smul_add]
-- 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
n : ℕ
⊢ ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
have pos : ∀ (hn : n = 0),
  ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
Tactic: by_cases hn : n = 0
-- 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
n : ℕ
pos :
  ∀ (hn : n = 0),
    ∑ i ∈ range n, f i • g i =
      HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
        ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
⊢ ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
have neg : ∀ (hn : ¬n = 0),
  ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
Tactic: by_cases hn : n = 0
-- 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
n : ℕ
hn : ¬n = 0
⊢ ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
have neg : ∑ x ∈ Ico 0 n, f x • g x =
  HSMul.hSMul (β := M) (f (n - 1)) (∑ x ∈ Ico 0 n, g x) -
    ∑ x ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ x ∈ Ico 0 (x + 1), g x)
Tactic: simp only [range_eq_Ico]
-- 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
n : ℕ
hn : ¬n = 0
⊢ ∑ x ∈ Ico 0 n, f x • g x =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ x ∈ Ico 0 n, g x) -
      ∑ x ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ x ∈ Ico 0 (x + 1), g x)
have neg : HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
    ∑ i ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i) =
  HSMul.hSMul (β := M) (f (n - 1)) (∑ x ∈ Ico 0 n, g x) -
    ∑ x ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ x ∈ Ico 0 (x + 1), g x)
Tactic: rw [sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.NatAntidiagonal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ (n + 1), f p =
    f (0, n + 1) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1 + 1, p.2)
have rw : f (0, n + 1) *
    ∏ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f
        (({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Function.Embedding.refl ℕ) :
            (a : ℕ × ℕ) → ℕ × ℕ)
          x) =
  f (0, n + 1) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1 + 1, p.2)
Tactic: rw [antidiagonal_succ, prod_cons, prod_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.NatAntidiagonal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
| ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p.swap
have rw : ∏ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
  f (Prod.swap (({ toFun := Prod.swap, inj' := sorry } : (a : ℕ × ℕ) → ℕ × ℕ) x))
Tactic: rw [← map_swap_antidiagonal, Finset.prod_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.NatAntidiagonal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ Eq.{u_1 + 1} (α := M) (∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p.swap)
    (∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p)
have conv_lhs : Eq.{u_1 + 1} (α := M)
  (∏ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    f (Prod.swap (({ toFun := Prod.swap, inj' := sorry } : (a : ℕ × ℕ) → ℕ × ℕ) x)))
  (∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p)
Tactic: conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.NatAntidiagonal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ (n + 1), f p =
    f (n + 1, 0) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1, p.2 + 1)
have rw : f (Prod.swap (0, n + 1)) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.swap.1 + 1, p.swap.2).swap =
  f (n + 1, 0) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1, p.2 + 1)
Tactic: rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.NatAntidiagonal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ f p n = f p (p.1 + p.2)
have rw : f p n = f p n
Tactic: rw [mem_antidiagonal.mp hp]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ Eq.{u_2 + 1} (α := M)
    (∏ x ∈ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s), Option.elim' 1 f x)
    (∏ x ∈ s.erase none, Option.elim' 1 f x)
have rw : Eq.{u_2 + 1} (α := M) (∏ x ∈ s.erase none, Option.elim' 1 f x) (∏ x ∈ s.erase none, Option.elim' 1 f x)
Tactic: rw [map_some_eraseNone]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ Eq.{u_2 + 1} (α := M) (∏ x ∈ (eraseNone : (a : Finset (Option α)) → Finset α) s, f x) (∏ x ∈ s, Option.elim' 1 f x)
have x : Eq.{u_2 + 1} (α := M)
  (∏ x ∈ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s), Option.elim' 1 f x)
  (∏ x ∈ s.erase none, Option.elim' 1 f x)
Tactic: calc
      ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
        (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
      _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
      _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ Eq.{u_2 + 1} (α := M) (∏ x ∈ (eraseNone : (a : Finset (Option α)) → Finset α) s, f x) (∏ x ∈ s, Option.elim' 1 f x)
have classical : Eq.{u_2 + 1} (α := M)
  (∏ x ∈ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s), Option.elim' 1 f x)
  (∏ x ∈ s.erase none, Option.elim' 1 f x)
Tactic: classical calc
      ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
        (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
      _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
      _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
inst_2 : NonAssocSemiring R
x : ι → R
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0
have h : ∀ (x_1 : ι), x x_1 = (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0) x_1
Tactic: ext