fix(Algebra/BigOperators/Group/Finset): Add missing binder annotation with pp.analyze in Finset.sum (leanprover-community#33070)

Author: MrQubo

Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

@@ -265,7 +265,7 @@ to show the domain type when the product is over `Finset.univ`. -/
   whenPPOption getPPNotation <| withOverApp 5 do
   let #[_, _, _, _, f] := (← getExpr).getAppArgs | failure
   guard f.isLambda
-  let ppDomain ← getPPOption getPPFunBinderTypes
+  let ppDomain ← withAppArg <| getPPOption getPPFunBinderTypes
   let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
     return (⟨i⟩, ← delab)
   let res ← withNaryArg 3 <| delabFinsetArg i
@@ -296,7 +296,7 @@ to show the domain type when the sum is over `Finset.univ`. -/
   whenPPOption getPPNotation <| withOverApp 5 do
   let #[_, _, _, _, f] := (← getExpr).getAppArgs | failure
   guard f.isLambda
-  let ppDomain ← getPPOption getPPFunBinderTypes
+  let ppDomain ← withAppArg <| getPPOption getPPFunBinderTypes
   let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
     return ((⟨i⟩ : Ident), ← delab)
   let res ← withNaryArg 3 <| delabFinsetArg i

MathlibTest/BigOps.lean

@@ -1,4 +1,5 @@
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import Mathlib.Data.Fintype.Basic
 
 section
 variable {ι M : Type*} [CommMonoid M] [AddCommMonoid M] [Fintype ι] {s : Finset ι} {p : ι → Prop}
@@ -62,4 +63,64 @@ set_option pp.funBinderTypes false
 #guard_msgs in
 #check Finset.prod {j | p j} fun i ↦ f i
 
+/-! ### Big operators over a finset with `pp.analyze` on -/
+
+/-- info: ∑ i, i.toNat : ℕ -/
+#guard_msgs in
+#check ∑ i : Fin 3, i.toNat
+
+/-- info: ∏ i, i.toNat : ℕ -/
+#guard_msgs in
+#check ∏ i : Fin 3, i.toNat
+
+/-- info: ∑ i : Fin 3, i.toNat : ℕ -/
+#guard_msgs in
+set_option pp.analyze true in
+#check ∑ i : Fin 3, i.toNat
+
+/-- info: ∏ i : Fin 3, i.toNat : ℕ -/
+#guard_msgs in
+set_option pp.analyze true in
+#check ∏ i : Fin 3, i.toNat
+
+/-- info: ∑ i ∈ s, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.sum s fun i ↦ f i
+
+/-- info: ∏ i ∈ s, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.prod s fun i ↦ f i
+
+/-- info: ∑ i ∈ s with p i, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.sum {j ∈ s | p j} fun i ↦ f i
+
+/-- info: ∏ i ∈ s with p i, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.prod {j ∈ s | p j} fun i ↦ f i
+
+/-- info: ∑ i : ι, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.sum Finset.univ fun i ↦ f i
+
+/-- info: ∏ i : ι, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.prod Finset.univ fun i ↦ f i
+
+/-- info: ∑ i : ι with p i, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.sum {j | p j} fun i ↦ f i
+
+/-- info: ∏ i : ι with p i, f i : M -/
+#guard_msgs in
+set_option pp.analyze true in
+#check Finset.prod {j | p j} fun i ↦ f i
+
 end