Theorem: sum_tsub (ExponentialRamsey/Prereq/Mathlib/Algebra/BigOperators/Ring.lean)

State before:
α : 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
Tactic:
rw [← Finset.sum_add_distrib]
State after:
α : 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

State before:
α : 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
Tactic:
exact Finset.sum_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx
State after:
no goals