α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ x in s, (f x + -g x) =
    ∏ i in s, f i +
      -∑ x in s, (g x * ∏ x in filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i in filter (fun j => x < j) s, f i
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i in s, (f i - g i) =
    ∏ i in s, f i -
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j - g j)) * ∏ j in filter (fun j => i < j) s, f j
simp only [sub_eq_add_neg]
case h.e'_3.h.e'_6
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ -∑ x in s, (g x * ∏ x in filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i in filter (fun j => x < j) s, f i =
    ∑ i in s, (-g i * ∏ j in filter (fun x => x < i) s, (f j + -g j)) * ∏ j in filter (fun j => i < j) s, f j
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ x in s, (f x + -g x) =
    ∏ i in s, f i +
      -∑ x in s, (g x * ∏ x in filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i in filter (fun j => x < j) s, f i
convert prod_add_ordered s f fun i => -g i
no goals
case h.e'_3.h.e'_6
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ -∑ x in s, (g x * ∏ x in filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i in filter (fun j => x < j) s, f i =
    ∑ i in s, (-g i * ∏ j in filter (fun x => x < i) s, (f j + -g j)) * ∏ j in filter (fun j => i < j) s, f j
simp