[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]


[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
l : List R
⊢ trop (sum l) = prod (map trop l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
⊢ trop (sum []) = prod (map trop [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop (sum tl) = prod (map trop tl)
⊢ trop (sum (hd :: tl)) = prod (map trop (hd :: tl))
[PROOFSTEP]
simp [← IH]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop (sum (Quotient.mk (List.isSetoid R) a)) = prod (map trop (Quotient.mk (List.isSetoid R) a))
[PROOFSTEP]
simpa using List.trop_sum
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ trop (∑ i in s, f i) = ∏ i in s, trop (f i)
[PROOFSTEP]
convert Multiset.trop_sum (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i in s, trop (f i) = Multiset.prod (Multiset.map trop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i in s, trop (f i) = Multiset.prod (Multiset.map (fun i => trop (f i)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
l : List (Tropical R)
⊢ untrop (prod l) = sum (map untrop l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
⊢ untrop (prod []) = sum (map untrop [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop (prod tl) = sum (map untrop tl)
⊢ untrop (prod (hd :: tl)) = sum (map untrop (hd :: tl))
[PROOFSTEP]
simp [← IH]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Multiset (Tropical R)
⊢ ∀ (a : List (Tropical R)),
    untrop (prod (Quotient.mk (List.isSetoid (Tropical R)) a)) =
      sum (map untrop (Quotient.mk (List.isSetoid (Tropical R)) a))
[PROOFSTEP]
simpa using List.untrop_prod
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ untrop (∏ i in s, f i) = ∑ i in s, untrop (f i)
[PROOFSTEP]
convert Multiset.untrop_prod (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i in s, untrop (f i) = Multiset.sum (Multiset.map untrop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i in s, untrop (f i) = Multiset.sum (Multiset.map (fun i => untrop (f i)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : LinearOrder R
l : List R
⊢ trop (minimum l) = sum (map (trop ∘ WithTop.some) l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u_1
S : Type u_2
inst✝ : LinearOrder R
⊢ trop (minimum []) = sum (map (trop ∘ WithTop.some) [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
inst✝ : LinearOrder R
hd : R
tl : List R
IH : trop (minimum tl) = sum (map (trop ∘ WithTop.some) tl)
⊢ trop (minimum (hd :: tl)) = sum (map (trop ∘ WithTop.some) (hd :: tl))
[PROOFSTEP]
simp [List.minimum_cons, ← IH]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset R
⊢ trop (inf s) = sum (map trop s)
[PROOFSTEP]
induction' s using Multiset.induction with s x IH
[GOAL]
case empty
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = sum (map trop 0)
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : R
x : Multiset R
IH : trop (inf x) = sum (map trop x)
⊢ trop (inf (s ::ₘ x)) = sum (map trop (s ::ₘ x))
[PROOFSTEP]
simp [← IH]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ trop (inf s f) = ∑ i in s, trop (f i)
[PROOFSTEP]
convert Multiset.trop_inf (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map trop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map (fun i => trop (f i)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
⊢ trop (sInf (f '' ↑s)) = ∑ i in s, trop (f i)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | h)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' ↑∅)) = ∑ i in ∅, trop (f i)
[PROOFSTEP]
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : Finset.Nonempty s
⊢ trop (sInf (f '' ↑s)) = ∑ i in s, trop (f i)
[PROOFSTEP]
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → WithTop R
⊢ trop (⨅ (i : S), f i) = ∑ i : S, trop (f i)
[PROOFSTEP]
rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset (Tropical R)
⊢ untrop (sum s) = inf (map untrop s)
[PROOFSTEP]
induction' s using Multiset.induction with s x IH
[GOAL]
case empty
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ untrop (sum 0) = inf (map untrop 0)
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop (sum x) = inf (map untrop x)
⊢ untrop (sum (s ::ₘ x)) = inf (map untrop (s ::ₘ x))
[PROOFSTEP]
simp only [sum_cons, ge_iff_le, untrop_add, untrop_le_iff, map_cons, inf_cons, ← IH]
[GOAL]
case cons
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop (sum x) = inf (map untrop x)
⊢ min (untrop s) (untrop (sum x)) = untrop s ⊓ untrop (sum x)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ untrop (∑ i in s, f i) = inf s (untrop ∘ f)
[PROOFSTEP]
convert Multiset.untrop_sum (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map untrop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map (fun x => untrop (f x)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in s, f i) = sInf (untrop ∘ f '' ↑s)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | h)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in ∅, f i) = sInf (untrop ∘ f '' ↑∅)
[PROOFSTEP]
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : Finset.Nonempty s
⊢ untrop (∑ i in s, f i) = sInf (untrop ∘ f '' ↑s)
[PROOFSTEP]
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i : S, f i) = ⨅ (i : S), untrop (f i)
[PROOFSTEP]
rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ sInf ((untrop ∘ fun i => f i) '' ↑univ) = sInf ((fun i => untrop (f i)) '' ↑univ)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in s, f i) = ⨅ (i : { x // x ∈ s }), untrop (f ↑i)
[PROOFSTEP]
simpa [← _root_.untrop_sum] using sum_attach.symm


[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ untrop (min a b) = untrop (if a ≤ b then a else b)
[PROOFSTEP]
simp [min_def]
[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : a ≤ b
⊢ untrop a = untrop a
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop b = untrop b
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ untrop (max a b) = untrop (if a ≤ b then b else a)
[PROOFSTEP]
simp [max_def]
[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : a ≤ b
⊢ untrop b = untrop b
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop a = untrop a
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ untrop (x + y) = untrop x
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ untrop (x + y) = untrop y
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = x ↔ x ≤ y
[PROOFSTEP]
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = y ↔ y ≤ x
[PROOFSTEP]
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
[PROOFSTEP]
rw [trop_add_def, trop_eq_iff_eq_untrop]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ min (untrop x) (untrop y) = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
[PROOFSTEP]
simp [min_eq_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0
[PROOFSTEP]
rw [add_eq_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0
[PROOFSTEP]
rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
[GOAL]
case mp.inl.intro
R : Type u
inst✝ : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ 0 = 0 ∧ b = 0
[PROOFSTEP]
exact ⟨rfl, le_antisymm (le_zero _) h⟩
[GOAL]
case mp.inr.intro
R : Type u
inst✝ : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ 0 = 0
[PROOFSTEP]
exact ⟨le_antisymm (le_zero _) h, rfl⟩
[GOAL]
case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case mpr.intro
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
src✝¹ : One (Tropical R) := instOneTropical
src✝ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
n : ℕ
⊢ untrop (NatCast.natCast (n + 1)) = untrop (NatCast.natCast n + 1)
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
src✝¹ : One (Tropical R) := instOneTropical
src✝ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
⊢ untrop (NatCast.natCast (Nat.zero + 1)) = untrop (NatCast.natCast Nat.zero + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
case succ
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
src✝¹ : One (Tropical R) := instOneTropical
src✝ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
n✝ : ℕ
⊢ untrop (NatCast.natCast (Nat.succ n✝ + 1)) = untrop (NatCast.natCast (Nat.succ n✝) + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
R : Type u
inst✝ : AddMonoid R
src✝¹ : MulOneClass (Tropical R) := instMulOneClassTropical
src✝ : Semigroup (Tropical R) := instSemigroupTropical
x✝ : Tropical R
⊢ untrop ((fun n x => x ^ n) 0 x✝) = untrop 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : AddGroup R
src✝ : Monoid (Tropical R) := instMonoidTropical
x✝¹ x✝ : Tropical R
⊢ untrop (x✝¹ / x✝) = untrop (x✝¹ * x✝⁻¹)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
⊢ x + y ≤ x + z
[PROOFSTEP]
cases' le_total x y with hx hy
[GOAL]
case inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hx : x ≤ y
⊢ x + y ≤ x + z
[PROOFSTEP]
rw [add_eq_left hx, add_eq_left (hx.trans h)]
[GOAL]
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z
[PROOFSTEP]
rw [add_eq_right hy]
[GOAL]
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ y ≤ x + z
[PROOFSTEP]
cases' le_total x z with hx hx
[GOAL]
case inr.inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : x ≤ z
⊢ y ≤ x + z
[PROOFSTEP]
rwa [add_eq_left hx]
[GOAL]
case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ x + z
[PROOFSTEP]
rwa [add_eq_right hx]
[GOAL]
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : Tropical R
n : ℕ
⊢ (x + y) ^ n = x ^ n + y ^ n
[PROOFSTEP]
cases' le_total x y with h h
[GOAL]
case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ (x + y) ^ n = x ^ n + y ^ n
[PROOFSTEP]
rw [add_eq_left h, add_eq_left (pow_le_pow_of_le_left' h _)]
[GOAL]
case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ (x + y) ^ n = x ^ n + y ^ n
[PROOFSTEP]
rw [add_eq_right h, add_eq_right (pow_le_pow_of_le_left' h _)]
[GOAL]
R : Type u
inst✝ : LinearOrderedAddCommMonoidWithTop R
src✝³ : AddMonoidWithOne (Tropical R) := instAddMonoidWithOneTropical
src✝² : Distrib (Tropical R) := instDistribTropical
src✝¹ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
src✝ : CommMonoid (Tropical R) := instCommMonoidTropical
x✝ : Tropical R
⊢ untrop (0 * x✝) = untrop 0
[PROOFSTEP]
simp [top_add]
[GOAL]
R : Type u
inst✝ : LinearOrderedAddCommMonoidWithTop R
src✝³ : AddMonoidWithOne (Tropical R) := instAddMonoidWithOneTropical
src✝² : Distrib (Tropical R) := instDistribTropical
src✝¹ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
src✝ : CommMonoid (Tropical R) := instCommMonoidTropical
x✝ : Tropical R
⊢ untrop (x✝ * 0) = untrop 0
[PROOFSTEP]
simp [add_top]
[GOAL]
R✝ : Type u
inst✝² : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
⊢ (n + 1) • x = x
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
R✝ : Type u
inst✝² : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
⊢ (Nat.zero + 1) • x = x
[PROOFSTEP]
simp
[GOAL]
case succ
R✝ : Type u
inst✝² : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ (Nat.succ n + 1) • x = x
[PROOFSTEP]
rw [add_nsmul, IH, one_nsmul, add_self]
[GOAL]
R✝ : Type u
inst✝¹ : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝ : LinearOrderedAddCommMonoid R
a b : Tropical (WithTop R)
⊢ a * b = 0 ↔ a = 0 ∨ b = 0
[PROOFSTEP]
simp [← untrop_inj_iff, WithTop.add_eq_top]