chore: bump to v4.24.0 (#172)

* The definition of `ModularForm` was generalized:
leanprover-community/mathlib4#26651
* `Summable` has a `SummationFilter` parameter now:
leanprover-community/mathlib4#29914
* `f` parameter of `tprod_pnat_eq_tprod_succ` is now implicit:
leanprover-community/mathlib4#27841
* various lemmas were deprecated
* A lemma named `Filter.map_add_atTop_eq` was added to mathlib:
leanprover-community/mathlib4#29532
* other changes too...

---------

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>

Author: dwrensha

SpherePacking/Basic/E8.lean

@@ -469,18 +469,6 @@ lemma dotProduct_is_integer {R : Type*} [Field R] [CharZero R] (i j : Fin 8) :
     ∃ z : ℤ, z = (E8Matrix R).row i ⬝ᵥ (E8Matrix R).row j :=
   ⟨_, (dotProduct_eq_inn _ _).symm⟩
 
-lemma sum_dotProduct {α β γ : Type*} [Fintype β] [CommSemiring γ]
-    {s : Finset α} {v : α → β → γ} {w : β → γ} :
-    (∑ i ∈ s, v i) ⬝ᵥ w = ∑ i ∈ s, v i ⬝ᵥ w := by
-  simp_rw [dotProduct, Finset.sum_apply, Finset.sum_mul]
-  exact Finset.sum_comm
-
-lemma dotProduct_sum {α β γ : Type*} [Fintype β] [CommSemiring γ]
-    {s : Finset α} {v : β → γ} {w : α → β → γ} :
-    v ⬝ᵥ (∑ i ∈ s, w i) = ∑ i ∈ s, v ⬝ᵥ w i := by
-  simp_rw [dotProduct, Finset.sum_apply, Finset.mul_sum]
-  exact Finset.sum_comm
-
 theorem E8_integral {R : Type*} [Field R] [CharZero R] (v w : Fin 8 → R)
     (hv : v ∈ Submodule.E8 R) (hw : w ∈ Submodule.E8 R) :
     ∃ z : ℤ, z = v ⬝ᵥ w := by

SpherePacking/Basic/PeriodicPacking.lean

@@ -78,7 +78,8 @@ theorem aux3 {ι τ : Type*} {s : Set ι} {f : ι → Set (EuclideanSpace ℝ τ
     have h_volume' := volume.mono hL
     rw [OuterMeasure.measureOf_eq_coe, Measure.coe_toOuterMeasure, Set.biUnion_eq_iUnion,
       measure_iUnion] at h_volume'
-    · have h_le := Summable.tsum_mono (f := fun _ ↦ c) (g := fun (x : s) ↦ volume (f x)) ?_ ?_ ?_
+    · have h_le : ∑' (n : ↑s), c ≤ ∑' (n : ↑s), volume (f ↑n) :=
+          Summable.tsum_mono (f := fun _ ↦ c) (g := fun (x : s) ↦ volume (f x)) ?_ ?_ ?_
       · have h₁ := (ENNReal.tsum_set_const _ _ ▸ h_le).trans h_volume'
         rw [← Set.encard_lt_top_iff, ← ENat.toENNReal_lt, ENat.toENNReal_top]
         refine lt_of_le_of_lt ((ENNReal.le_div_iff_mul_le ?_ ?_).mpr h₁) <|
@@ -871,7 +872,7 @@ theorem volume_ball_ratio_tendsto_nhds_one'
   · convert ENNReal.Tendsto.div (volume_ball_ratio_tendsto_nhds_one hd hC') ?_
       (volume_ball_ratio_tendsto_nhds_one hd hC) ?_ <;> simp
 
-theorem Filter.map_add_atTop_eq {β : Type*} {f : ℝ → β} (C : ℝ) (α : Filter β) :
+theorem Filter.map_add_atTop_eq' {β : Type*} {f : ℝ → β} (C : ℝ) (α : Filter β) :
     Tendsto f atTop α ↔ Tendsto (fun x ↦ f (x + C)) atTop α := by
   constructor <;> intro hf
   · apply tendsto_map'_iff.mp
@@ -889,7 +890,7 @@ theorem Filter.map_add_atTop_eq {β : Type*} {f : ℝ → β} (C : ℝ) (α : Fi
 theorem volume_ball_ratio_tendsto_nhds_one'' {d : ℕ} {C C' : ℝ} (hd : 0 < d) :
     Tendsto (fun R ↦ volume (ball (0 : EuclideanSpace ℝ (Fin d)) (R + C))
       / volume (ball (0 : EuclideanSpace ℝ (Fin d)) (R + C'))) atTop (𝓝 1) := by
-  apply (Filter.map_add_atTop_eq (max (-C) (-C')) _).mpr
+  apply (Filter.map_add_atTop_eq' (max (-C) (-C')) _).mpr
   simp_rw [add_assoc]
   convert volume_ball_ratio_tendsto_nhds_one' hd ?_ ?_
   · trans (-C) + C

SpherePacking/Basic/SpherePacking.lean

@@ -63,7 +63,7 @@ instance PeriodicSpherePacking.instIsZLattice (S : PeriodicSpherePacking d) :
 
 instance SpherePacking.instCentersDiscrete (S : SpherePacking d) :
     DiscreteTopology S.centers := by
-  simp_rw [← singletons_open_iff_discrete, Metric.isOpen_iff]
+  simp_rw [discreteTopology_iff_isOpen_singleton, Metric.isOpen_iff]
   intro ⟨u, hu⟩ ⟨v, hv⟩ huv
   simp_rw [Set.subset_singleton_iff, mem_ball, Subtype.forall, Subtype.mk.injEq]
   rw [Set.mem_singleton_iff, Subtype.mk.injEq] at huv
@@ -175,7 +175,7 @@ noncomputable def PeriodicSpherePacking.scale (S : PeriodicSpherePacking d) {c :
     specialize hε' x hx
     simp only [DistribMulAction.toLinearMap_apply, AddSubgroupClass.coe_norm,
       Submodule.mk_eq_zero] at hx' hε'
-    rw [norm_smul, norm_eq_abs, abs_eq_self.mpr hc.le, mul_lt_mul_left hc] at hx'
+    rw [norm_smul, norm_eq_abs, abs_eq_self.mpr hc.le, mul_lt_mul_iff_right₀ hc] at hx'
     exact hε' hx'
   lattice_isZLattice := by
     use ?_
@@ -219,7 +219,7 @@ lemma SpherePacking.scale_balls {S : SpherePacking d} {c : ℝ} (hc : 0 < c) :
       rw [dist_eq_norm] at hxy ⊢
       rw [← smul_sub, norm_smul, Real.norm_eq_abs, abs_eq_self.mpr this]
       apply lt_of_lt_of_le (b := c⁻¹ * (c * S.separation / 2))
-      · exact (mul_lt_mul_left h).mpr hxy
+      · exact (mul_lt_mul_iff_right₀ h).mpr hxy
       · rw [mul_div_assoc, ← mul_assoc, inv_mul_cancel₀ hc.ne.symm, one_mul]
     · rw [smul_smul, mul_inv_cancel₀ hc.ne.symm, one_smul]
   · intro h

SpherePacking/CohnElkies/LPBound.lean

@@ -370,9 +370,9 @@ private theorem calc_steps (hd : 0 < d) (hf : Summable f) :
             -- First, we apply the fact that two sides are equal if they're equal in ℂ.
             apply congrArg re
             -- Next, we apply the fact that two sums are equal if their summands are.
-            apply congrArg _ _
+            congr 1
             ext x
-            apply congrArg _ _
+            congr 1
             ext y
             -- Now that we've isolated the innermost sum, we can use the PSF-L.
             exact SchwartzMap.PoissonSummation_Lattices P.lattice f (x - ↑y)
@@ -419,12 +419,12 @@ private theorem calc_steps (hd : 0 < d) (hf : Summable f) :
             -- are really trying to show are equal.
             apply congrArg re
             apply congrArg _ _
-            apply congrArg _ _
+            congr 1
             ext m
             apply congrArg _ _
-            apply congrArg _ _
+            congr 1
             ext x
-            apply congrArg _ _
+            congr 1
             ext y
             simp only [sub_eq_neg_add, RCLike.wInner_neg_left, ofReal_neg, mul_neg, mul_comm]
             rw [RCLike.wInner_add_left]
@@ -439,15 +439,15 @@ private theorem calc_steps (hd : 0 < d) (hf : Summable f) :
         := by
             apply congrArg re
             apply congrArg _ _
-            apply congrArg _ _
+            congr 1
             ext m
             simp only [mul_assoc]
             apply congrArg _ _
             rw [← tsum_mul_right]
-            apply congrArg _ _
+            congr 1
             ext x
             rw [← tsum_mul_left]
-            apply congrArg _ _
+            congr 1
             ext y
             simp only [RCLike.wInner_neg_left, ofReal_neg, mul_neg]
   _ = ((1 / ZLattice.covolume P.lattice) * ∑' m : bilinFormOfRealInner.dualSubmodule P.lattice, (𝓕 f
@@ -460,11 +460,11 @@ private theorem calc_steps (hd : 0 < d) (hf : Summable f) :
         := by
             apply congrArg re
             apply congrArg _ _
-            apply congrArg _ _
+            congr 1
             ext m
             apply congrArg _ _
             rw [conj_tsum]
-            apply congrArg _ _
+            congr 1
             ext x
             exact Complex.exp_neg_real_I_eq_conj (x : EuclideanSpace ℝ (Fin d)) m
   _ = (1 / ZLattice.covolume P.lattice) * ∑' m : bilinFormOfRealInner.dualSubmodule P.lattice,

SpherePacking/ForMathlib/Cusps.lean

@@ -0,0 +1,17 @@
+import Mathlib.NumberTheory.ModularForms.BoundedAtCusp
+
+open scoped MatrixGroups ModularForm UpperHalfPlane
+
+theorem zero_at_cusps_of_zero_at_infty {f : ℍ → ℂ} {c : OnePoint ℝ} {k : ℤ}
+    {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic]
+    (hc : IsCusp c 𝒢) (hb : ∀ A ∈ 𝒮ℒ, UpperHalfPlane.IsZeroAtImInfty (f ∣[k] A)) :
+    c.IsZeroAt f k := by
+  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
+  refine (OnePoint.isZeroAt_iff_forall_SL2Z hc).mpr fun A hA ↦ hb A ⟨A, rfl⟩
+
+theorem bounded_at_cusps_of_bounded_at_infty {f : ℍ → ℂ} {c : OnePoint ℝ} {k : ℤ}
+    {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic]
+    (hc : IsCusp c 𝒢) (hb : ∀ A ∈ 𝒮ℒ, UpperHalfPlane.IsBoundedAtImInfty (f ∣[k] A)) :
+    c.IsBoundedAt f k := by
+  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
+  exact (OnePoint.isBoundedAt_iff_forall_SL2Z hc).mpr fun A hA ↦ hb A ⟨A, rfl⟩

SpherePacking/ForMathlib/Encard.lean

@@ -202,8 +202,8 @@ protected theorem tsum_subtype_biUnion_le (f : α → ℕ∞) (s : Finset ι) (t
 
 protected theorem tsum_subtype_iUnion_le [Fintype ι] (f : α → ℕ∞) (t : ι → Set α) :
     ∑' x : ⋃ i, t i, f x ≤ ∑ i, ∑' x : t i, f x := by
-  rw [← tsum_fintype]
-  exact ENat.tsum_subtype_iUnion_le_tsum f t
+  have : ∑ i, ∑' x : t i, f x = ∑' i, ∑' x : t i, f x := by rw [tsum_fintype]
+  exact this ▸ ENat.tsum_subtype_iUnion_le_tsum f t
 
 theorem tsum_subtype_iUnion_eq_tsum (f : α → ℕ∞) (t : ι → Set α) (ht : Pairwise (Disjoint on t)) :
     ∑' x : ⋃ i, t i, f x = ∑' i, ∑' x : t i, f x :=

SpherePacking/ForMathlib/InvPowSummability.lean

@@ -76,8 +76,8 @@ theorem Summable_of_Inv_Pow_Summable'
     dsimp only [Summable, HasSum]
     use 0
     intro ε hε
-    simp only [Filter.mem_map, Filter.mem_atTop_sets, ge_iff_le, le_of_subsingleton,
-      Set.mem_preimage, true_implies, exists_const]
+    simp only [SummationFilter.unconditional_filter, Filter.mem_map, Filter.mem_atTop_sets,
+      ge_iff_le, le_of_subsingleton, Set.mem_preimage, forall_const, exists_const]
     intro b
     rw [eq_top_of_bot_eq_top rfl b]
     simp only [Finset.top_eq_univ, Finset.univ_eq_empty, Finset.sum_empty]

SpherePacking/MagicFunction/PolyFourierCoeffBound.lean

@@ -130,7 +130,7 @@ lemma aux_8 : 0 < ∏' (n : ℕ+), (1 - rexp (-2 * π * ↑↑n * z.im)) ^ 24 :=
     apply Summable.neg
     simp_rw [smul_eq_mul]
     conv =>
-      rhs
+      lhs
       equals (fun (b : ℕ) => Real.exp (-2 * π * b * z.im)) ∘ (PNat.val) => rfl
 
     apply Summable.subtype
@@ -163,7 +163,7 @@ lemma aux_11 : 0 < ∏' (n : ℕ+), (1 - rexp (-π * ↑↑n)) ^ 24 := by
     apply Summable.neg
     simp_rw [smul_eq_mul]
     conv =>
-      rhs
+      lhs
       equals (fun (b : ℕ) => Real.exp (-π * b)) ∘ (PNat.val) => rfl
 
     apply Summable.subtype
@@ -302,7 +302,7 @@ by
         · simp_rw [sub_eq_add_neg]
           apply Real.summable_log_one_add_of_summable
           apply Summable.neg
-          conv => rhs; equals (fun (b : ℕ) => Real.exp (-2 * π * b * z.im)) ∘ (PNat.val) => rfl
+          conv => lhs; equals (fun (b : ℕ) => Real.exp (-2 * π * b * z.im)) ∘ (PNat.val) => rfl
           apply Summable.subtype
           simp_rw [mul_comm, mul_assoc, Real.summable_exp_nat_mul_iff]
           simp [pi_pos, UpperHalfPlane.im_pos]
@@ -372,7 +372,7 @@ private lemma step_12 :
       calc π * ↑↑n
       _ ≤ π * ↑↑n * 1 := by rw [mul_one]
       _ < π * ↑↑n * z.im * 2 := by
-        rw [mul_assoc (π * ↑↑n), mul_lt_mul_left (by positivity)]
+        rw [mul_assoc (π * ↑↑n), mul_lt_mul_iff_right₀ (by positivity)]
         linarith
     · sorry
     · sorry

SpherePacking/MagicFunction/a/IntegralEstimates/I2.lean

@@ -84,7 +84,7 @@ lemma parametrisation_eq : ∀ t ∈ Ioo (0 : ℝ) 1,
       exact zero_ne_one ((h₁.symm).trans h₂)
   _ = _ := by
       conv_lhs => rw [div_mul_div_comm (-1) (t + I)]
-      simp only [neg_mul, one_mul, neg_sub, div_mul_eq_mul_div, div_add_div_same]
+      simp only [neg_mul, one_mul, neg_sub, div_mul_eq_mul_div, ← add_div]
       congr
       · ac_rfl
       · ring_nf

SpherePacking/MagicFunction/a/IntegralEstimates/I4.lean

@@ -90,7 +90,7 @@ lemma parametrisation_eq : ∀ t ∈ Ioo (0 : ℝ) 1,
       norm_num1 at h₂
   _ = _ := by
       conv_lhs => rw [div_mul_div_comm (-1) (-t + I)]
-      simp only [neg_mul, one_mul, neg_sub, div_mul_eq_mul_div, div_add_div_same]
+      simp only [neg_mul, one_mul, neg_sub, div_mul_eq_mul_div, ← add_div]
       congr
       · ring
       · ring_nf