feat: add congruence lemmas for Function.update and Pi.single (leanprover-community#35423)

Adds `simp` congruence lemmas to `Function.update` and `Pi.single` that are specialized for the non-dependent case. See also [#mathlib4 > Simp fails to apply with &leanprover-community#96;Function.update&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Simp.20fails.20to.20apply.20with.20.60Function.2Eupdate.60/with/573889929).

Co-authored-by: Rob23oba <robin.arnez@web.de>

Author: Rob23oba

Mathlib/Algebra/Notation/Pi/Basic.lean

@@ -88,6 +88,21 @@ lemma mulSingle_inj (i : ι) {x y : M i} : mulSingle i x = mulSingle i y ↔ x =
 
 variable {M : Type*} [One M]
 
+/--
+A congruence lemma for `Pi.mulSingle`, specialized for the non-dependent case. Without this,
+`simp` can't rewrite in the first and third argument (`i` and `j`) because of dependence.
+See also https://github.com/leanprover/lean4/issues/12478.
+-/
+@[to_additive (attr := congr) /--
+A congruence lemma for `Pi.single`, specialized for the non-dependent case. Without this,
+`simp` can't rewrite in the first and third argument (`i` and `j`) because of dependence.
+See also https://github.com/leanprover/lean4/issues/12478.
+-/]
+lemma mulSingle_congr {i₁ i₂ : ι} (hi : i₁ = i₂)
+    {x₁ x₂ : M} (hx : x₁ = x₂) {j₁ j₂ : ι} (hj : j₁ = j₂) :
+    (mulSingle i₁ x₁ : ι → M) j₁ = (mulSingle i₂ x₂ : ι → M) j₂ :=
+  update_congr rfl hi hx hj
+
 /-- On non-dependent functions, `Pi.mulSingle` can be expressed as an `ite` -/
 @[to_additive (attr := grind =)
   /-- On non-dependent functions, `Pi.single` can be expressed as an `ite` -/]

Mathlib/Logic/Function/Basic.lean

@@ -642,6 +642,18 @@ theorem update_self (a : α) (v : β a) (f : ∀ a, β a) : update f a v a = v :
 theorem update_of_ne {a a' : α} (h : a ≠ a') (v : β a') (f : ∀ a, β a) : update f a' v a = f a :=
   dif_neg h
 
+/--
+A congruence lemma for `Function.update`, specialized for the non-dependent case. Without this,
+`simp` can't rewrite in the fourth argument `a` because the result type depends on `a`.
+See also https://github.com/leanprover/lean4/issues/12478.
+-/
+@[congr]
+lemma update_congr {β : Sort*}
+    {f₁ f₂ : α → β} (hf : f₁ = f₂) {a'₁ a'₂ : α} (ha' : a'₁ = a'₂)
+    {v₁ v₂ : β} (hv : v₁ = v₂) {a₁ a₂ : α} (ha : a₁ = a₂) :
+    Function.update f₁ a'₁ v₁ a₁ = Function.update f₂ a'₂ v₂ a₂ := by
+  subst hf; subst ha'; subst hv; subst ha; rfl
+
 /-- On non-dependent functions, `Function.update` can be expressed as an `ite` -/
 theorem update_apply {β : Sort*} (f : α → β) (a' : α) (b : β) (a : α) :
     update f a' b a = if a = a' then b else f a := by

Mathlib/NumberTheory/ModularForms/QExpansion.lean

@@ -251,10 +251,6 @@ private lemma hasFPowerSeriesOnBall_update {f : ℍ → ℂ} (hh : 0 < h) {c : 
           (mod_cast hr')).summable.norm
   · simp
   · intro y hy
-    rw [zero_add]
-    -- note the `simp`s below do not automatically apply this lemma to the argument of
-    -- `Function.update`, because of limitations in `simp`'s support for dependent function types,
-    -- see lean4 issue #12478.
     rw [← ENNReal.coe_one, Metric.eball_coe, NNReal.coe_one, mem_ball_zero_iff] at hy
     rcases eq_or_ne y 0 with rfl | hy'
     · simpa +contextual [zero_pow_eq] using hasSum_ite_eq 0 (c 0)

Mathlib/RepresentationTheory/Tannaka.lean

@@ -211,7 +211,7 @@ lemma toRightFDRepComp_in_rightRegular [IsDomain k] (η : Aut (forget k G)) :
       congrFun congr(($nat.symm).hom (single u 1)) 1
     _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
       congr($hs (leftRegular t⁻¹ (single u 1)))
-    _ = _ := by by_cases u = t * s <;> simp_all [single_apply]
+    _ = _ := by by_cases u = t * s <;> simp_all
 
 lemma equivHom_surjective [IsDomain k] : Function.Surjective (equivHom k G) := by
   intro η

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

@@ -719,7 +719,7 @@ protected theorem Multipliable.tprod_eq_mul_tprod_ite' [DecidableEq β] [L.LeAtT
     ∏'[L] x, f x = f b * ∏'[L] x, ite (x = b) 1 (f x) :=
   calc
     ∏'[L] x, f x = ∏'[L] x, (ite (x = b) (f x) 1 * update f b 1 x) :=
-      tprod_congr fun n ↦ by split_ifs with h <;> simp [update_apply, h]
+      tprod_congr fun n ↦ by split_ifs with h <;> simp [h]
     _ = (∏'[L] x, ite (x = b) (f x) 1) * ∏'[L] x, update f b 1 x :=
       Multipliable.tprod_mul ⟨ite (b = b) (f b) 1, hasProd_single b (fun _ hb ↦ if_neg hb) L⟩ hf
     _ = ite (b = b) (f b) 1 * ∏'[L] x, update f b 1 x := by