rw [← Finset.sum_add_distrib]
α : Type u_1
β : Type u_2
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : ExistsAddOfLE β
inst✝³ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub β
inst✝ : OrderedSub β
s : Finset α
f g : α → β
hfg : ∀ x ∈ s, g x ≤ f x
⊢ ∑ x in s, (f x - g x) + ∑ x in s, g x = ∑ x in s, f x
α : Type u_1
β : Type u_2
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : ExistsAddOfLE β
inst✝³ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub β
inst✝ : OrderedSub β
s : Finset α
f g : α → β
hfg : ∀ x ∈ s, g x ≤ f x
⊢ ∑ x in s, (f x - g x + g x) = ∑ x in s, f x