Lean4
@[macro BigOperators.bigsum]
public meta def _aux_Mathlib_Algebra_BigOperators_Group_Finset_Defs___macroRules_BigOperators_bigsum_1 : Macro✝ := fun
| `(∑ $bs:bigOpBinders$[ with $[$hx??:binderIdent : ]?$p?:term]?, $v) => do
let processed ← processBigOpBinders bs
let x ← bigOpBindersPattern processed
let s ← bigOpBindersProd processed
match hx??, p? with
| some (some hx), some p =>
`(Finset.sum $s fun $x ↦ if $hx : $p then $v else 0)
| _, some p =>
`(Finset.sum (Finset.filter (fun $x ↦ $p) $s) (fun $x ↦ $v))
| _, none =>
`(Finset.sum $s (fun $x ↦ $v))
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
