feat(Algebra/Group/Indicator): add Pi. mulIndicator_singleton (leanprover-community#34083)

Add `Pi.mulIndicator_singleton ` and `Pi.indicator_singleton ` (via `@[to_additive]`), showing that on non-dependent functions:

```lean
Set.mulIndicator {i} f = Pi.mulSingle i (f i)
Set.indicator {i} f = Pi.single i (f i)
```

This is the direct `Pi` analog of [`Finsupp.single_eq_set_indicator`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finsupp/Single.html#Finsupp.single_eq_set_indicator), without involving Finsupp.

Also add confluence lemmas about `NNReal.toReal` to fix compile.

Co-authored-by: IlPreteRosso <will1541286313@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: IlPreteRosso

Mathlib/Algebra/Group/Indicator.lean

@@ -196,6 +196,19 @@ theorem apply_mulIndicator_symmDiff {g : G → β} (hg : ∀ x, g x⁻¹ = g x)
 
 end Group
 
+/-! ### Relationship with `Pi.mulSingle`/`Pi.single` -/
+
+variable {ι : Type*} [DecidableEq ι] {M : Type*} [One M]
+
+/-- On non-dependent functions, `Set.mulIndicator` on a singleton set equals `Pi.mulSingle`. -/
+@[to_additive (attr := simp)
+  /-- On non-dependent functions, `Set.indicator` on a singleton set equals `Pi.single`. -/]
+theorem mulIndicator_singleton (i : ι) (f : ι → M) :
+    Set.mulIndicator {i} f = Pi.mulSingle i (f i) := by
+  ext j
+  simp only [Set.mulIndicator_apply, Pi.mulSingle_apply, Set.mem_singleton_iff]
+  split_ifs with h <;> simp [h]
+
 end Set
 
 @[to_additive]

Mathlib/Data/NNReal/Basic.lean

@@ -35,11 +35,26 @@ namespace NNReal
 
 noncomputable instance : FloorSemiring ℝ≥0 := Nonneg.floorSemiring
 
+@[simp, norm_cast]
+theorem coe_mulIndicator {α} (s : Set α) (f : α → ℝ≥0) (a : α) :
+    ((s.mulIndicator f a : ℝ≥0) : ℝ) = s.mulIndicator (fun x => ↑(f x)) a :=
+  map_mulIndicator toRealHom _ _ _
+
 @[simp, norm_cast]
 theorem coe_indicator {α} (s : Set α) (f : α → ℝ≥0) (a : α) :
     ((s.indicator f a : ℝ≥0) : ℝ) = s.indicator (fun x => ↑(f x)) a :=
   map_indicator toRealHom _ _ _
 
+@[simp, norm_cast]
+theorem coe_mulSingle {α} [DecidableEq α] (a : α) (b : ℝ≥0) (c : α) :
+    ((Pi.mulSingle a b : α → ℝ≥0) c : ℝ) = (Pi.mulSingle a b : α → ℝ) c := by
+  simpa using coe_mulIndicator {a} (fun _ ↦ b) c
+
+@[simp, norm_cast]
+theorem coe_single {α} [DecidableEq α] (a : α) (b : ℝ≥0) (c : α) :
+    ((Pi.single a b : α → ℝ≥0) c : ℝ) = (Pi.single a b : α → ℝ) c := by
+  simpa using coe_indicator {a} (fun _ ↦ b) c
+
 @[norm_cast]
 theorem coe_list_sum (l : List ℝ≥0) : ((l.sum : ℝ≥0) : ℝ) = (l.map (↑)).sum :=
   map_list_sum toRealHom l