[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝³ : CommMonoid β
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → β
a b c : α
⊢ ∏ x in Ico a b, f (x + c) = ∏ x in Ico (a + c) (b + c), f x
[PROOFSTEP]
rw [← map_add_right_Ico, prod_map]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝³ : CommMonoid β
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → β
a b c : α
⊢ ∏ x in Ico a b, f (x + c) = ∏ x in Ico a b, f (↑(addRightEmbedding c) x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝³ : CommMonoid β
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → β
a b c : α
⊢ ∏ x in Ico a b, f (c + x) = ∏ x in Ico (a + c) (b + c), f x
[PROOFSTEP]
convert prod_Ico_add' f a b c using 2
[GOAL]
case h.e'_2.a
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝³ : CommMonoid β
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → β
a b c x✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (c + x✝) = f (x✝ + c)
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a ≤ b
f : ℕ → β
⊢ ∏ k in Ico a (b + 1), f k = (∏ k in Ico a b, f k) * f b
[PROOFSTEP]
rw [Nat.Ico_succ_right_eq_insert_Ico hab, prod_insert right_not_mem_Ico, mul_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a < b
f : ℕ → β
⊢ ∏ k in Ico a b, f k = f a * ∏ k in Ico (a + 1) b, f k
[PROOFSTEP]
have ha : a ∉ Ico (a + 1) b := by simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a < b
f : ℕ → β
⊢ ¬a ∈ Ico (a + 1) b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a < b
f : ℕ → β
ha : ¬a ∈ Ico (a + 1) b
⊢ ∏ k in Ico a b, f k = f a * ∏ k in Ico (a + 1) b, f k
[PROOFSTEP]
rw [← prod_insert ha, Nat.Ico_insert_succ_left hab]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ (∏ i in Ioc m n, f i) * ∏ i in Ioc n k, f i = ∏ i in Ioc m k, f i
[PROOFSTEP]
rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)
[PROOFSTEP]
apply disjoint_left.2 fun x hx h'x => _
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ ∀ (x : ℕ), x ∈ Ioc m n → x ∈ Ioc n k → False
[PROOFSTEP]
intros x hx h'x
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False
[PROOFSTEP]
exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a ≤ b
f : ℕ → β
⊢ ∏ k in Ioc a (b + 1), f k = (∏ k in Ioc a b, f k) * f (b + 1)
[PROOFSTEP]
rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k in Ico m n, f k) * ∏ k in range m, f k = ∏ k in range n, f k
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k in range m, f k) * ∏ k in Ico m n, f k = ∏ k in range n, f k
[PROOFSTEP]
exact prod_range_mul_prod_Ico f h
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ ∏ k in Ico m n, f k = (∏ k in range n, f k) / ∏ k in range m, f k
[PROOFSTEP]
simpa only [div_eq_mul_inv] using prod_Ico_eq_mul_inv f h
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ (∏ k in range m, f k) / ∏ k in range n, f k = ∏ k in filter (fun k => n ≤ k) (range m), f k
[PROOFSTEP]
rw [← prod_Ico_eq_div f hnm]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∏ k in Ico n m, f k = ∏ k in filter (fun k => n ≤ k) (range m), f k
[PROOFSTEP]
congr
[GOAL]
case e_s
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ Ico n m = filter (fun k => n ≤ k) (range m)
[PROOFSTEP]
apply Finset.ext
[GOAL]
case e_s.a
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ filter (fun k => n ≤ k) (range m)
[PROOFSTEP]
simp only [mem_Ico, mem_filter, mem_range, *]
[GOAL]
case e_s.a
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i in Ico a b, ∑ j in Ico i b, f i j = ∑ j in Ico a b, ∑ i in Ico a (j + 1), f i j
[PROOFSTEP]
rw [Finset.sum_sigma', Finset.sum_sigma']
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x in Finset.sigma (Ico a b) fun i => Ico i b, f x.fst x.snd =
    ∑ x in Finset.sigma (Ico a b) fun j => Ico a (j + 1), f x.snd x.fst
[PROOFSTEP]
refine'
  Finset.sum_bij' (fun (x : Σ _ : ℕ, ℕ) _ => (⟨x.2, x.1⟩ : Σ _ : ℕ, ℕ)) _ (fun _ _ => rfl)
    (fun (x : Σ _ : ℕ, ℕ) _ => (⟨x.2, x.1⟩ : Σ _ : ℕ, ℕ)) _ (by (rintro ⟨⟩ _; rfl)) (by (rintro ⟨⟩ _; rfl))
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 : (_ : ℕ) × ℕ) (ha : a_1 ∈ Finset.sigma (Ico a b) fun i => Ico i b),
    (fun x x_1 => { fst := x.snd, snd := x.fst }) ((fun x x_1 => { fst := x.snd, snd := x.fst }) a_1 ha)
        (_ : (fun x x_1 => { fst := x.snd, snd := x.fst }) a_1 ha ∈ ?m.28850) =
      a_1
[PROOFSTEP]
rintro ⟨⟩ _
[GOAL]
case mk
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
fst✝ snd✝ : ℕ
ha✝ : { fst := fst✝, snd := snd✝ } ∈ Finset.sigma (Ico a b) fun i => Ico i b
⊢ (fun x x_1 => { fst := x.snd, snd := x.fst })
      ((fun x x_1 => { fst := x.snd, snd := x.fst }) { fst := fst✝, snd := snd✝ } ha✝)
      (_ : (fun x x_1 => { fst := x.snd, snd := x.fst }) { fst := fst✝, snd := snd✝ } ha✝ ∈ ?m.28850) =
    { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 : (_ : ℕ) × ℕ) (ha : a_1 ∈ Finset.sigma (Ico a b) fun j => Ico a (j + 1)),
    (fun x x_1 => { fst := x.snd, snd := x.fst }) ((fun x x_1 => { fst := x.snd, snd := x.fst }) a_1 ha)
        (_ : (fun x x_1 => { fst := x.snd, snd := x.fst }) a_1 ha ∈ ?m.28849) =
      a_1
[PROOFSTEP]
rintro ⟨⟩ _
[GOAL]
case mk
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
fst✝ snd✝ : ℕ
ha✝ : { fst := fst✝, snd := snd✝ } ∈ Finset.sigma (Ico a b) fun j => Ico a (j + 1)
⊢ (fun x x_1 => { fst := x.snd, snd := x.fst })
      ((fun x x_1 => { fst := x.snd, snd := x.fst }) { fst := fst✝, snd := snd✝ } ha✝)
      (_ : (fun x x_1 => { fst := x.snd, snd := x.fst }) { fst := fst✝, snd := snd✝ } ha✝ ∈ ?m.28849) =
    { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 : (_ : ℕ) × ℕ) (ha : a_1 ∈ Finset.sigma (Ico a b) fun i => Ico i b),
    (fun x x_1 => { fst := x.snd, snd := x.fst }) a_1 ha ∈ Finset.sigma (Ico a b) fun j => Ico a (j + 1)
[PROOFSTEP]
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 : (_ : ℕ) × ℕ) (ha : a_1 ∈ Finset.sigma (Ico a b) fun j => Ico a (j + 1)),
    (fun x x_1 => { fst := x.snd, snd := x.fst }) a_1 ha ∈ Finset.sigma (Ico a b) fun i => Ico i b
[PROOFSTEP]
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1 + 1
[PROOFSTEP]
rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 + 1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 ≤ a_1 ∧ a_1 < b
[PROOFSTEP]
rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩
[GOAL]
case refine'_1.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a ≤ b
h₄ : b < b✝
⊢ (a✝ ≤ b ∧ b < b✝) ∧ a✝ ≤ a ∧ a < b + 1
[PROOFSTEP]
refine' ⟨⟨_, _⟩, ⟨_, _⟩⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a✝ ≤ b
h₄ : b < a + 1
⊢ (a✝ ≤ b ∧ b < b✝) ∧ b ≤ a ∧ a < b✝
[PROOFSTEP]
refine' ⟨⟨_, _⟩, ⟨_, _⟩⟩
[GOAL]
case refine'_1.intro.intro.intro.refine'_1
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a ≤ b
h₄ : b < b✝
⊢ a✝ ≤ b
[PROOFSTEP]
linarith
[GOAL]
case refine'_1.intro.intro.intro.refine'_2
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a ≤ b
h₄ : b < b✝
⊢ b < b✝
[PROOFSTEP]
linarith
[GOAL]
case refine'_1.intro.intro.intro.refine'_3
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a ≤ b
h₄ : b < b✝
⊢ a✝ ≤ a
[PROOFSTEP]
linarith
[GOAL]
case refine'_1.intro.intro.intro.refine'_4
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a ≤ b
h₄ : b < b✝
⊢ a < b + 1
[PROOFSTEP]
linarith
[GOAL]
case refine'_2.intro.intro.intro.refine'_1
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a✝ ≤ b
h₄ : b < a + 1
⊢ a✝ ≤ b
[PROOFSTEP]
linarith
[GOAL]
case refine'_2.intro.intro.intro.refine'_2
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a✝ ≤ b
h₄ : b < a + 1
⊢ b < b✝
[PROOFSTEP]
linarith
[GOAL]
case refine'_2.intro.intro.intro.refine'_3
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a✝ ≤ b
h₄ : b < a + 1
⊢ b ≤ a
[PROOFSTEP]
linarith
[GOAL]
case refine'_2.intro.intro.intro.refine'_4
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : AddCommMonoid M
a✝ b✝ : ℕ
f : ℕ → ℕ → M
a b : ℕ
h₁ : a✝ ≤ a
h₂ : a < b✝
h₃ : a✝ ≤ b
h₄ : b < a + 1
⊢ a < b✝
[PROOFSTEP]
linarith
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n : ℕ
⊢ ∏ k in Ico m n, f k = ∏ k in range (n - m), f (m + k)
[PROOFSTEP]
by_cases h : m ≤ n
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n : ℕ
h : m ≤ n
⊢ ∏ k in Ico m n, f k = ∏ k in range (n - m), f (m + k)
[PROOFSTEP]
rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n : ℕ
h : ¬m ≤ n
⊢ ∏ k in Ico m n, f k = ∏ k in range (n - m), f (m + k)
[PROOFSTEP]
replace h : n ≤ m := le_of_not_ge h
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n : ℕ
h : n ≤ m
⊢ ∏ k in Ico m n, f k = ∏ k in range (n - m), f (m + k)
[PROOFSTEP]
rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
[PROOFSTEP]
have : ∀ i < m, i ≤ n := by
  intro i hi
  exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
⊢ ∀ (i : ℕ), i < m → i ≤ n
[PROOFSTEP]
intro i hi
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
i : ℕ
hi : i < m
⊢ i ≤ n
[PROOFSTEP]
exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
[PROOFSTEP]
cases' lt_or_le k m with hkm hkm
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
[PROOFSTEP]
rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in image (fun x => n - x) (Ico k m), f j
[PROOFSTEP]
refine' (prod_image _).symm
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∀ (x : ℕ), x ∈ Ico k m → ∀ (y : ℕ), y ∈ Ico k m → n - x = n - y → x = y
[PROOFSTEP]
simp only [mem_Ico]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∀ (x : ℕ), k ≤ x ∧ x < m → ∀ (y : ℕ), k ≤ y ∧ y < m → n - x = n - y → x = y
[PROOFSTEP]
rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
[GOAL]
case inl.intro.intro
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ i = j
[PROOFSTEP]
rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
[PROOFSTEP]
have : n + 1 - k ≤ n + 1 - m := by
  rw [tsub_le_tsub_iff_left h]
  exact hkm
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ n + 1 - k ≤ n + 1 - m
[PROOFSTEP]
rw [tsub_le_tsub_iff_left h]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ m ≤ k
[PROOFSTEP]
exact hkm
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this✝ : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
this : n + 1 - k ≤ n + 1 - m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
[PROOFSTEP]
simp only [ge_iff_le, hkm, Ico_eq_empty_of_le, prod_empty, tsub_le_iff_right, Ico_eq_empty_of_le this]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ j in range n, f (n - 1 - j) = ∏ j in range n, f j
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ j in range zero, f (zero - 1 - j) = ∏ j in range zero, f j
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ j in range (succ n✝), f (succ n✝ - 1 - j) = ∏ j in range (succ n✝), f j
[PROOFSTEP]
simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ x in Ico 0 (succ n✝), f (n✝ - x) = ∏ x in Ico 0 (succ n✝), f x
[PROOFSTEP]
rw [prod_Ico_reflect _ _ le_rfl]
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ j in Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x in Ico 0 (succ n✝), f x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ ∏ x in Ico 1 (n + 1 + 1), x = (n + 1)!
[PROOFSTEP]
rw [prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n, Nat.factorial_succ, prod_Ico_id_eq_factorial n,
  Nat.succ_eq_add_one, mul_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ ∏ x in range (n + 1), (x + 1) = (n + 1)!
[PROOFSTEP]
simp [Finset.range_succ, prod_range_add_one_eq_factorial n]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ (∑ i in range n, i) * 2 = ∑ i in range n, i + ∑ i in range n, (n - 1 - i)
[PROOFSTEP]
rw [sum_range_reflect (fun i => i) n, mul_two]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ ∑ i in range n, (n - 1) = n * (n - 1)
[PROOFSTEP]
rw [sum_const, card_range, Nat.nsmul_eq_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ ∑ i in range n, i = n * (n - 1) / 2
[PROOFSTEP]
rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ zero_lt_two]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
rw [sum_eq_sum_Ico_succ_bot hmn]
  -- porting note: the following used to be done with `conv`
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
funext
[GOAL]
case e_f.h
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
rw [← sum_range_succ_sub_sum g]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
rw [h₃]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]
  -- porting note: the following used to be done with `conv`
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
rw [h₄]
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
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
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
intro i
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
rw [sub_smul]
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
M : Type u_2
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
[PROOFSTEP]
simp_rw [this, sum_neg_distrib, sum_range_succ, smul_add]
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
M : Type u_2
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)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
⊢ ∑ i in range n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - ∑ i in range (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hn : n = 0
⊢ ∑ i in range n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - ∑ i in range (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hn : ¬n = 0
⊢ ∑ i in range n, f i • g i =
    f (n - 1) • ∑ i in range n, g i - ∑ i in range (n - 1), (f (i + 1) - f i) • ∑ i in range (i + 1), g i
[PROOFSTEP]
rw [range_eq_Ico, sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero, range_eq_Ico]
