chore: bump mathlib (#262)

Author: pitmonticone

Carleson/Classical/HilbertKernel.lean

@@ -118,7 +118,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧
       intro t ht
       have : f = fun t ↦ c t / d t := rfl
       rw [this]
-      have : f' = fun t ↦ ((c' t * d t - c t * d' t) / d t ^ 2) := by ext t; ring_nf
+      have : f' = fun t ↦ ((c' t * d t - c t * d' t) / d t ^ 2) := by ext t; ring
       rw [this]
       apply HasDerivAt.div _ _ _
       · exact cdef ▸ c'def ▸ HasDerivAt.const_sub _ (HasDerivAt.ofReal_comp (hasDerivAt_id' _))

Carleson/Discrete/ExceptionalSet.lean

@@ -287,10 +287,10 @@ lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))
         simp_rw [stackSize, Q₁, mem_setOf_eq]
         congr
       have lcast : (2 : ℝ≥0∞) ^ (n + 1) = ((2 ^ (n + 1) : ℕ) : ℝ).toNNReal := by
-        rw [toNNReal_coe_nat, ENNReal.coe_natCast]; norm_cast
+        rw [Real.toNNReal_coe_nat, ENNReal.coe_natCast]; norm_cast
       have rcast : ∑ q ∈ Q₁, (𝓘 q : Set X).indicator (1 : X → ℝ≥0∞) x =
           (((∑ q ∈ Q₁, (𝓘 q : Set X).indicator (1 : X → ℕ) x) : ℕ) : ℝ).toNNReal := by
-        rw [toNNReal_coe_nat, ENNReal.coe_natCast, Nat.cast_sum]; congr!; simp [indicator]
+        rw [Real.toNNReal_coe_nat, ENNReal.coe_natCast, Nat.cast_sum]; congr!; simp [indicator]
       rw [lcast, rcast, ENNReal.coe_le_coe]
       exact Real.toNNReal_le_toNNReal (Nat.cast_le.mpr this)
     _ ≤ ∫⁻ x, ∑ q ∈ Q₁, (𝓘 q : Set X).indicator 1 x := setLIntegral_le_lintegral _ _
@@ -841,7 +841,7 @@ lemma third_exception_aux :
       refine lintegral_mono fun x ↦ ?_
       simp_rw [← ENNReal.coe_natCast, show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl,
         ← ENNReal.coe_zpow two_ne_zero, ← ENNReal.coe_mul, ENNReal.coe_le_coe,
-        ← toNNReal_coe_nat]
+        ← Real.toNNReal_coe_nat]
       have c2 : (2 : ℝ≥0) ^ (9 * a - j : ℤ) = ((2 : ℝ) ^ (9 * a - j : ℤ)).toNNReal := by
         refine ((fun h ↦ (Real.toNNReal_eq_iff_eq_coe h).mpr) ?_ rfl).symm
         positivity

Carleson/Discrete/ForestComplement.lean

@@ -194,7 +194,7 @@ lemma mem_iUnion_iff_mem_of_mem_ℭ {f : ℕ → ℕ → Set (𝔓 X)} (hp : p 
   · obtain ⟨n', k', _, mp⟩ := h
     have e := pairwiseDisjoint_ℭ (X := X).elim (mem_univ (k, n)) (mem_univ (k', n'))
       (not_disjoint_iff.mpr ⟨p, hp.1, hf k' n' mp⟩)
-    rw [Prod.mk.inj_iff] at e
+    rw [Prod.mk_inj] at e
     exact e.1 ▸ e.2 ▸ mp
   · use n, k, hp.2
 

Carleson/ForestOperator/LargeSeparation.lean

@@ -621,7 +621,7 @@ lemma holder_correlation_rearrange (hf : BoundedCompactSupport f) :
       simp_rw [mul_add]; apply lintegral_add_right
       apply hf.stronglyMeasurable.measurable.enorm.mul (Measurable.enorm (Measurable.sub ?_ ?_)) <;>
         exact (continuous_conj.comp_stronglyMeasurable
-          (measurable_Ks.comp measurable_prod_mk_right).stronglyMeasurable).measurable
+          (measurable_Ks.comp measurable_prodMk_right).stronglyMeasurable).measurable
     _ ≤ (∫⁻ y in E p, ‖f y‖ₑ * ‖conj (Ks (𝔰 p) y x)‖ₑ * ‖- Q y x + Q y x' + 𝒬 u x - 𝒬 u x'‖ₑ) +
         ∫⁻ y in E p, ‖f y‖ₑ * ‖conj (Ks (𝔰 p) y x) - conj (Ks (𝔰 p) y x')‖ₑ := by
       simp_rw [mul_assoc]; gcongr with y; rw [enorm_mul]; gcongr

Carleson/ForestOperator/RemainingTiles.lean

@@ -349,7 +349,7 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) (s' : ℤ) :
   gcongr
   rw [Real.toNNReal_mul (by positivity), Real.toNNReal_rpow_of_nonneg (by positivity),
     Real.toNNReal_mul (by positivity), ← Real.rpow_intCast,
-    Real.toNNReal_rpow_of_nonneg (by positivity), NNReal.toNNReal_coe_nat]
+    Real.toNNReal_rpow_of_nonneg (by positivity), Real.toNNReal_coe_nat]
   simp only [Nat.cast_pow, Nat.cast_ofNat, Real.toNNReal_ofNat, Int.cast_neg, ← pow_mul]
   rw [← mul_assoc, ← pow_succ, C7_6_4, ← NNReal.rpow_natCast, ← NNReal.rpow_intCast, Int.cast_neg]
   congr!

Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean

@@ -172,7 +172,7 @@ theorem eLpNorm_top_convolution_le' {p q : ℝ≥0∞} (hpq : p.IsConjExponent q
     eLpNorm (f ⋆[L, μ] g) ∞ μ ≤ ENNReal.ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
   refine eLpNorm_top_convolution_le_aux hpq hf.enorm ?_ ?_ c hL
   · intro x; exact (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x)).enorm
-  · intro x; exact eLpNorm_comp_measurePreserving hg (μ.measurePreserving_sub_left x)
+  · intro x; apply eLpNorm_comp_measurePreserving hg (Measure.measurePreserving_sub_left μ x)
 
 -- Auxiliary inequality used to prove versions with simpler conditions on `f` and `g`
 open ENNReal in
@@ -427,7 +427,7 @@ theorem eLpNorm_convolution_le_of_norm_le_mul' {p q r : ℝ≥0∞}
     eLpNorm (f ⋆[L, μ] g) r μ ≤ .ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
   refine eLpNorm_convolution_le_of_norm_le_mul_aux hp hq hr hpqr hf.enorm ?_ ?_ ?_ c hL
   · intro x; exact hg.enorm.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x)
-  · intro x; exact eLpNorm_comp_measurePreserving hg (μ.measurePreserving_sub_left x)
+  · intro x; apply eLpNorm_comp_measurePreserving hg (μ.measurePreserving_sub_left x)
   · exact hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub μ μ) |>.enorm.pow_const _
 
 /-- **Young's convolution inequality**: the `ℒr` seminorm of a convolution `(f ⋆[L, μ] g)` is

Carleson/ToMathlib/WeakType.lean

@@ -578,7 +578,7 @@ lemma distribution_add_le' {A : ℝ≥0∞} {g₁ g₂ : α → ε}
 lemma HasStrongType.const_smul {𝕜 E' α α' : Type*} [NormedAddCommGroup E']
     {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} {T : (α → ε) → (α' → E')}
     {p p' : ℝ≥0∞} {μ : Measure α} {ν : Measure α'} {c : ℝ≥0} (h : HasStrongType T p p' μ ν c)
-    [NormedRing 𝕜] [MulActionWithZero 𝕜 E'] [BoundedSMul 𝕜 E'] (k : 𝕜) :
+    [NormedRing 𝕜] [MulActionWithZero 𝕜 E'] [IsBoundedSMul 𝕜 E'] (k : 𝕜) :
     HasStrongType (k • T) p p' μ ν (‖k‖₊ * c) := by
   refine fun f hf ↦ ⟨AEStronglyMeasurable.const_smul (h f hf).1 k, eLpNorm_const_smul_le.trans ?_⟩
   simp only [ENNReal.smul_def, smul_eq_mul, coe_mul, mul_assoc]
@@ -595,7 +595,7 @@ lemma HasStrongType.const_mul {E' α α' : Type*} [NormedRing E']
 lemma HasWeakType.const_smul {𝕜 E' α α' : Type*} [NormedAddCommGroup E']
     {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} {T : (α → ε) → (α' → E')}
     {p p' : ℝ≥0∞} {μ : Measure α} {ν : Measure α'} {c : ℝ≥0} (h : HasWeakType T p p' μ ν c)
-    [NormedRing 𝕜] [MulActionWithZero 𝕜 E'] [BoundedSMul 𝕜 E'] (k : 𝕜) :
+    [NormedRing 𝕜] [MulActionWithZero 𝕜 E'] [IsBoundedSMul 𝕜 E'] (k : 𝕜) :
     HasWeakType (k • T) p p' μ ν (‖k‖₊ * c) := by
   intro f hf
   refine ⟨aestronglyMeasurable_const.smul (h f hf).1, ?_⟩

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e708dc8be75d27f10bf6c0c76ed0b76760ecc50",
+   "rev": "c529790e37592678166f414cfaaa095c32fe1a60",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f2fb9809751c4646c68c329b14f7d229a93176fd",
+   "rev": "5105c4f21aae2d8dc15b4568951810140e6027cd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",