Lean4
@[macro BigOperators.bigprod]
public meta def _aux_Mathlib_Algebra_BigOperators_Group_Finset_Defs___macroRules_BigOperators_bigprod_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.prod $s fun $x ↦ if $hx : $p then $v else 1)
| _, some p =>
`(Finset.prod (Finset.filter (fun $x ↦ $p) $s) (fun $x ↦ $v))
| _, none =>
`(Finset.prod $s (fun $x ↦ $v))
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
