chore: bump to v4.23.0-rc2 (#497)

Author: pitmonticone

Carleson/Antichain/AntichainTileCount.lean

@@ -188,7 +188,7 @@ lemma stack_density (𝔄 : Set (𝔓 X)) (ϑ : Θ X) (N : ℕ) (L : Grid X) :
         _ ≤ 2^a * dens₁ (𝔄' : Set (𝔓 X)) * volume (L : Set X) := by
           have hIL : 𝓘 p = L := by simp_rw [← hp.2]
           have h2a : ((2 : ℝ≥0∞) ^ a)⁻¹ = 2^(-(a : ℤ)) := by
-            rw [← zpow_natCast, ENNReal.zpow_neg two_ne_zero ENNReal.ofNat_ne_top]
+            rw [← zpow_natCast, ENNReal.zpow_neg]
           rw [← ENNReal.div_le_iff (ne_of_gt (hIL ▸ volume_coeGrid_pos (defaultD_pos a)))
             (by finiteness), ← ENNReal.div_le_iff' (Ne.symm (NeZero.ne' (2 ^ a))) (by finiteness),
             ENNReal.div_eq_inv_mul, h2a, dens₁]

Carleson/Antichain/TileCorrelation.lean

@@ -439,7 +439,7 @@ lemma bound_6_2_29 (ha : 4 ≤ a) {p p' : 𝔓 X} (x2 : E p) :
     _ = 2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 1) * 2 ^ (11 * a) /
         (2 ^ (3 * a) * volume (ball x2.1 (D ^ 𝔰 p))) := by
       rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (by left; positivity) (by left; simp),
-        ← mul_assoc, ← zpow_natCast _ (3 * a), ← ENNReal.zpow_neg two_ne_zero ENNReal.ofNat_ne_top]
+        ← mul_assoc, ← zpow_natCast _ (3 * a), ← ENNReal.zpow_neg]
       congr
     _ ≤ C6_1_5 a / (2 ^ (3 * a) * volume (ball x2.1 (D ^ 𝔰 p))) := by
       gcongr; exact ENNReal.coe_le_coe.mpr (C6_1_5_bound ha)

Carleson/Discrete/ExceptionalSet.lean

@@ -410,7 +410,7 @@ lemma lintegral_Ioc_layervol_one {l : ℕ} :
   calc
     _ = ∫⁻ t in Ioc (l : ℝ) (l + 1), layervol (X := X) k n (l + 1) := by
       refine setLIntegral_congr_fun measurableSet_Ioc fun t ht ↦ ?_
-      unfold layervol; congr with x; simp_rw [mem_setOf]; constructor <;> intro h
+      unfold layervol; congr with x; constructor <;> intro h
       · rw [indicator_sum_eq_natCast, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le]
         rw [indicator_sum_eq_natCast, ← Nat.ceil_le] at h; convert h; symm
         rwa [Nat.ceil_eq_iff (by omega), add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]

Carleson/Discrete/ForestComplement.lean

@@ -367,11 +367,12 @@ variable {p' : 𝔓 X} {l : ℝ≥0} (hl : 2 ≤ l)
   (qp' : 2 ^ (4 * a - n : ℤ) < l ^ (-a : ℤ) * volume (E₂ l p') / volume (𝓘 p' : Set X))
 include hl qp'
 
+omit hl in
 lemma lt_quotient_rearrange :
     (2 ^ (4 * a) * l ^ a : ℝ≥0) * 2 ^ (-n : ℤ) < volume (E₂ l p') / volume (𝓘 p' : Set X) := by
   rw [mul_div_assoc] at qp'; convert ENNReal.div_lt_of_lt_mul' qp' using 1
   rw [ENNReal.div_eq_inv_mul,
-    ← ENNReal.zpow_neg (by exact_mod_cast (zero_lt_two.trans_le hl).ne') ENNReal.coe_ne_top,
+    ← ENNReal.zpow_neg,
     neg_neg, ENNReal.coe_mul, mul_rotate, mul_assoc, ENNReal.coe_pow, zpow_natCast]
   congr 1
   rw [ENNReal.coe_pow, ENNReal.coe_ofNat, ← zpow_natCast,
@@ -381,7 +382,7 @@ lemma lt_quotient_rearrange :
 lemma l_upper_bound : l < 2 ^ n := by
   have ql1 : volume (E₂ l p') / volume (𝓘 p' : Set X) ≤ 1 := by
     apply ENNReal.div_le_of_le_mul; rw [one_mul]; exact measure_mono (E₂_subset ..)
-  replace qp' := (lt_quotient_rearrange hl qp').trans_le ql1
+  replace qp' := (lt_quotient_rearrange qp').trans_le ql1
   rw [← ENNReal.mul_lt_mul_right (c := 2 ^ (n : ℤ)) (by simp) (by simp), one_mul, mul_assoc,
     ← ENNReal.zpow_add two_ne_zero ENNReal.ofNat_ne_top, neg_add_cancel, zpow_zero, mul_one,
     show (2 ^ (n : ℤ) : ℝ≥0∞) = (2 ^ (n : ℤ) : ℝ≥0) by simp, ENNReal.coe_lt_coe,
@@ -399,7 +400,7 @@ lemma exists_𝔒_with_le_quotient :
   have ltq : (2 ^ (4 * a) * l ^ a : ℝ≥0) * 2 ^ (-n : ℤ) <
       ∑ p'' ∈ 𝔒 p' l, volume (E₁ p'') / volume (𝓘 p'' : Set X) :=
     calc
-      _ < volume (E₂ l p') / volume (𝓘 p' : Set X) := lt_quotient_rearrange hl qp'
+      _ < volume (E₂ l p') / volume (𝓘 p' : Set X) := lt_quotient_rearrange qp'
       _ ≤ volume (⋃ p'' ∈ 𝔒 p' l, E₁ p'') / volume (𝓘 p' : Set X) := by
         gcongr; simp_rw [E₁, E₂, smul, toTileLike, TileLike.toSet]; intro x mx
         have rsub := biUnion_Ω (i := 𝓘 p'); rw [range_subset_iff] at rsub; specialize rsub x

Carleson/ForestOperator/LargeSeparation.lean

@@ -1255,7 +1255,7 @@ lemma global_tree_control1_edist_part1
       rw [← mul_assoc, ← mul_div_assoc, mul_assoc _ _ ((D : ℝ≥0∞) ^ _), mul_comm _ (_ * _),
         mul_div_assoc, mul_comm (_ ^ _ * _)]; congr
       rw [div_eq_mul_inv, ENNReal.mul_rpow_of_nonneg _ _ (by positivity),
-        ← ENNReal.zpow_neg (by simp) (by simp), ← ENNReal.rpow_intCast, ← ENNReal.rpow_mul,
+        ← ENNReal.zpow_neg, ← ENNReal.rpow_intCast, ← ENNReal.rpow_mul,
         ← div_eq_mul_inv, Int.cast_neg]
     _ = C7_5_5 a * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S,
         ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) ∧ 𝔰 p = k,

Carleson/Psi.lean

@@ -765,7 +765,7 @@ private lemma enorm_Ks_sub_Ks_le_far {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0
     trans 8 * ↑D * (D ^ (s - 1) / 8 / ↑D ^ s)
     on_goal 2 => gcongr
     apply le_of_eq
-    rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ← ENNReal.zpow_neg (by simp) (by simp)]
+    rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ← ENNReal.zpow_neg]
     suffices 1 = (8 * (8 : ℝ≥0∞)⁻¹) * (D ^ (1 : ℤ) * D ^ (-s) * D ^ (s - 1)) by
       apply this.trans
       rw [zpow_one]

Carleson/ToMathlib/WeakType.lean

@@ -613,7 +613,7 @@ lemma distribution_smul_left {f : α → ε'} {c : ℝ≥0} (hc : c ≠ 0) :
     exact ENNReal.coe_ne_zero.mpr hc
   unfold distribution
   congr with x
-  simp only [Pi.smul_apply, mem_setOf_eq]
+  simp only [Pi.smul_apply]
   rw [← @ENNReal.mul_lt_mul_right (t / ‖c‖ₑ) _ (‖c‖ₑ) h₀ coe_ne_top,
     enorm_smul_eq_mul (c := c) _, ENNReal.div_mul_cancel h₀ coe_ne_top, mul_comm]
 
@@ -625,7 +625,7 @@ lemma distribution_smul_left' {f : α → E} {c : 𝕜} (hc : c ≠ 0) :
   have h₀ : ‖c‖ₑ ≠ 0 := enorm_ne_zero.mpr hc
   unfold distribution
   congr with x
-  simp only [Pi.smul_apply, mem_setOf_eq]
+  simp only [Pi.smul_apply]
   rw [← @ENNReal.mul_lt_mul_right (t / ‖c‖ₑ) _ (‖c‖ₑ) h₀ coe_ne_top,
     enorm_smul _, mul_comm, ENNReal.div_mul_cancel h₀ coe_ne_top]
 

Carleson/TwoSidedCarleson/NontangentialOperator.lean

@@ -456,7 +456,6 @@ lemma radius_change {g : X → ℂ} (hg : BoundedFiniteSupport g volume) (hr : r
       rw [ENNReal.div_le_iff' (by simp) (by simp)]
       calc _
         _ = volume (ball x (2 ^ 3 * (R / 4))) := by
-          congr
           ring_nf
         _ ≤ (defaultA a) ^ 3 * volume (ball x (R / 4)) := by
           apply measure_ball_two_le_same_iterate
@@ -469,7 +468,6 @@ lemma radius_change {g : X → ℂ} (hg : BoundedFiniteSupport g volume) (hr : r
           gcongr
           apply measure_ball_two_le_same
         _ = 2 ^ (4 * a) * volume (ball x' (R / 4)) := by
-          unfold defaultA
           push_cast
           ring_nf
     _= 2 ^ (a ^ 3 + 4 * a) := by

Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean

@@ -397,9 +397,15 @@ lemma ball_covering_finite (hO : IsOpen O ∧ O ≠ univ) {U : Set X} {r' : X 
   · calc
       _ = {i | ¬i < U.card ∧ x ∈ ball (c i) (3 * r i)}.encard +
           {i | i < U.card ∧ x ∈ ball (c i) (3 * r i)}.encard := by
-        rw [← encard_union_eq]; swap
+        have : {i | x ∈ ball (c i) (3 * r i)} =
+            {i | ¬ i < U.card ∧ x ∈ ball (c i) (3 * r i)} ∪
+                {i | i < U.card ∧ x ∈ ball (c i) (3 * r i)} := by
+          ext i; refine ⟨fun hx ↦ ?_, fun h ↦ ?_⟩
+          · by_cases hi : i < U.card; exact Or.inr ⟨hi, hx⟩; exact Or.inl ⟨hi, hx⟩
+          · rcases h with ⟨_, hx⟩ | ⟨_, hx⟩ <;> exact hx
+        rw [← encard_union_eq]
+        · congr
         · exact disjoint_left.mpr fun i mi₁ mi₂ ↦ mi₁.1 mi₂.1
-        congr; ext i; simp only [mem_setOf_eq, mem_union]; tauto
       _ = 0 + {u ∈ U.toSet | x ∈ ball u (3 * r' u)}.encard := by
         congr
         · simp_rw [encard_eq_zero, eq_empty_iff_forall_notMem, mem_setOf_eq, not_and]; intro i hi

lake-manifest.json

@@ -15,20 +15,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
+   "rev": "90c0e186fd333cbdddbe0e5148aa3cd2d24dcf9a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "v4.23.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
+   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -45,57 +45,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
+   "rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
+   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.68",
+   "inputRev": "v0.0.71",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
+   "rev": "523c8ee53f7057447fc62ec14e506fda4cf63dfa",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
+   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
+   "rev": "6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",