Theorem: test_fun_inference (Ray/Tactic/BoundTests.lean)

State before:
α : Type
s : Finset α
f g : α → ℂ
⊢ ‖s.sum fun x => f x + g x‖ ≤ s.sum fun x => ‖f x + g x‖
Tactic:
bound
State after:
no goals