Update mathlib to 4.12.0-rc1

Carleson/AntichainOperator.lean

@@ -2,9 +2,6 @@ import Carleson.TileStructure
 import Carleson.HardyLittlewood
 import Carleson.Psi
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open scoped ShortVariables
 variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
   [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
@@ -260,7 +257,7 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (
     rw [one_le_div (add_pos_iff.mpr (Or.inr zero_lt_one)), two_mul, add_le_add_iff_left]
     exact le_of_lt (q_mem_Ioc X).1
   have hqq' : q' ≤ nnq := by -- Better proof?
-    rw [add_comm, div_le_iff (add_pos (zero_lt_one) hq0), mul_comm, mul_le_mul_iff_of_pos_left hq0,
+    rw [add_comm, div_le_iff₀ (add_pos (zero_lt_one) hq0), mul_comm, mul_le_mul_iff_of_pos_left hq0,
       ← one_add_one_eq_two, add_le_add_iff_left]
     exact (nnq_mem_Ioc X).1.le
   have hq'_inv : (q' - 1)⁻¹ ≤ 3 * (nnq - 1)⁻¹ := by

Carleson/Classical/Approximation.lean

@@ -72,7 +72,7 @@ lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) : ∃
     fourier_coe_apply', Complex.ofReal_mul, Complex.ofReal_ofNat, smul_eq_mul, Complex.real_smul,
     Complex.ofReal_inv, map_mul, map_inv₀, Complex.abs_ofReal, Complex.abs_ofNat]
   field_simp
-  rw [abs_of_nonneg Real.pi_pos.le, mul_comm Real.pi, div_le_iff Real.two_pi_pos, ←Complex.norm_eq_abs]
+  rw [abs_of_nonneg Real.pi_pos.le, mul_comm Real.pi, div_le_iff₀ Real.two_pi_pos, ←Complex.norm_eq_abs]
   calc ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (2 * Real.pi * Complex.I * n * x / (2 * Real.pi))) * f x‖
     _ = ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
       congr with x

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -48,6 +48,7 @@ def integer_linear (n : ℤ) : C(ℝ, ℝ) := ⟨fun (x : ℝ) ↦ n * x, by fun
 
 local notation "θ" => integer_linear
 
+set_option quotPrecheck false in
 local notation "Θ" => {(θ n) | n : ℤ}
 
 
@@ -454,7 +455,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
           by_cases hxy : x = y
           · rw [hxy]
             simp
-          rw [dist_eq_norm, ← div_le_iff (dist_pos.mpr hxy), Ldef, NNReal.coe_mk]
+          rw [dist_eq_norm, ← div_le_iff₀ (dist_pos.mpr hxy), Ldef, NNReal.coe_mk]
           apply le_ciSup_of_le _ x
           apply le_ciSup_of_le _ y
           apply le_ciSup_of_le _ hxy
@@ -464,7 +465,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             simp only [ne_eq, Set.mem_range, exists_prop, and_imp,
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
             intro h
-            rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
+            rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm]
             exact LipschitzWith.norm_sub_le hK _ _
           · use K
             rw [upperBounds]
@@ -473,7 +474,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             intro y
             apply Real.iSup_le _ NNReal.zero_le_coe
             intro h
-            rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
+            rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm]
             exact LipschitzWith.norm_sub_le hK _ _
           · use K
             rw [upperBounds]
@@ -484,7 +485,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             intro y
             apply Real.iSup_le _ NNReal.zero_le_coe
             intro h
-            rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
+            rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm]
             apply LipschitzWith.norm_sub_le hK
         · --prove main property of B
           intro y hy

Carleson/Classical/CarlesonOperatorReal.lean

@@ -94,7 +94,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
       use S
       constructor
       · intro s hs
-        apply Filter.eventually_of_forall
+        apply Filter.Eventually.of_forall
         intro y
         rw [bound_def, Fdef, norm_indicator_eq_indicator_norm]
         simp only
@@ -138,7 +138,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
       · --interesting part
         rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
         simp_rw [norm_norm]
-        apply Filter.eventually_of_forall
+        apply Filter.Eventually.of_forall
         apply F_bound_on_set
     · have contOn1 : ∀ (y : ℝ), ContinuousOn (fun s ↦ F x s y) (Set.Iio (dist x y)) := by
         intro y
@@ -202,7 +202,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         · right; linarith
       rw [MeasureTheory.ae_iff]
       exact MeasureTheory.measure_mono_null subset_finite (Finset.measure_zero _ _)
-    · exact Filter.eventually_of_forall fun r ↦ ((Measurable.of_uncurry_left
+    · exact Filter.Eventually.of_forall fun r ↦ ((Measurable.of_uncurry_left
         (measurable_mul_kernel f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable
   rw [this]
   apply measurable_biSup _

Carleson/Classical/ClassicalCarleson.lean

@@ -63,7 +63,7 @@ theorem classical_carleson {f : ℝ → ℂ}
     gcongr
     rw [ε'def, div_div]
     apply div_le_div_of_nonneg_left εpos.le (by norm_num)
-    rw [← div_le_iff' (by norm_num)]
+    rw [← div_le_iff₀' (by norm_num)]
     exact le_trans' (lt_C_control_approximation_effect εpos).le (by linarith [Real.two_le_pi])
   _ ≤ ε := by linarith
 

Carleson/Classical/ControlApproximationEffect.lean

@@ -127,7 +127,8 @@ lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-Real.pi)
     _ = 2 * (|x| / ‖1 - exp (I * x)‖) := by ring
     _ ≤ 2 * (Real.pi / 2) := by
       gcongr 2 * ?_
-      rw [div_le_iff' (by rwa [norm_pos_iff]), ←div_le_iff (by linarith [Real.pi_pos]), div_div_eq_mul_div, mul_div_assoc, mul_comm]
+      rw [div_le_iff₀' (by rwa [norm_pos_iff]), ← div_le_iff₀ (by linarith [Real.pi_pos]),
+        div_div_eq_mul_div, mul_div_assoc, mul_comm]
       apply lower_secant_bound' (by rfl)
       have : |x| ≤ Real.pi := by
         rwa [abs_le]
@@ -343,14 +344,14 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g Measu
           · conv => pattern ((g _) * _); rw [mul_comm]
             apply MeasureTheory.Integrable.bdd_mul' integrable₁ measurable₁.aestronglyMeasurable
             · rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
-              apply eventually_of_forall
+              apply Eventually.of_forall
               exact fun _ hy ↦ boundedness₁ hy.1.le
           · conv => pattern ((g _) * _); rw [mul_comm]
             apply MeasureTheory.Integrable.bdd_mul' integrable₁
             · apply Measurable.aestronglyMeasurable
               exact continuous_star.measurable.comp measurable₁
             · rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
-              apply eventually_of_forall
+              apply Eventually.of_forall
               intro y hy
               rw [RCLike.norm_conj]
               exact boundedness₁ hy.1.le
@@ -636,7 +637,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
     _ ≤ 2 * (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - Real.pi * δ))) ^ (2 : ℝ) := by
       rw [Real.rpow_mul MeasureTheory.measureReal_nonneg]
       gcongr
-      rw [Real.rpow_add' MeasureTheory.measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff' ε'_δ_expression_pos, ← mul_assoc]
+      rw [Real.rpow_add' MeasureTheory.measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff₀' ε'_δ_expression_pos, ← mul_assoc]
       apply mul_le_of_nonneg_of_le_div δ_mul_const_pos.le
       apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg
       rw[Real.rpow_neg MeasureTheory.measureReal_nonneg, div_inv_eq_mul]

Carleson/Classical/Helper.lean

@@ -19,7 +19,7 @@ lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measur
   · exact intervalIntegrable_const
   · exact measurable_g.aestronglyMeasurable
   · rw [Filter.EventuallyLE, ae_restrict_iff_subtype measurableSet_uIoc]
-    apply Filter.eventually_of_forall
+    apply Filter.Eventually.of_forall
     rw [Subtype.forall]
     exact fun x _ ↦ bddg x
 

Carleson/Classical/HilbertKernel.lean

@@ -252,7 +252,7 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} :
 
   /- Beginning of the main proof -/
   have y2ley' : y / 2 ≤ y' := by
-    rw [div_le_iff two_pos]
+    rw [div_le_iff₀ two_pos]
     calc y
       _ = 2 * (y - y') - y + 2 * y' := by ring
       _ ≤ 2 * |y - y'| - y + 2 * y' := by gcongr; exact le_abs_self _

Carleson/Classical/VanDerCorput.lean

@@ -36,7 +36,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
     case to the complex conjugate.-/
     push_neg at n_pos
     calc ‖∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x‖
-      _ = ‖(starRingEnd ℂ) (∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x)‖ := Eq.symm RCLike.norm_conj
+      _ = ‖(starRingEnd ℂ) (∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x)‖ := Eq.symm (RCLike.norm_conj _)
       _ = ‖∫ (x : ℝ) in a..b, cexp (I * ↑(-n) * ↑x) * ((starRingEnd ℂ) ∘ ϕ) x‖ := by
         rw [intervalIntegral.integral_of_le (by linarith), ← integral_conj, ← intervalIntegral.integral_of_le (by linarith)]
         congr
@@ -214,7 +214,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
           linarith [Real.two_le_pi]
         _ ≤ Real.pi * (n * (b - a) + n * (b - a)) := by
           gcongr
-          rwa [← div_le_iff' (Int.cast_pos.mpr n_pos)]
+          rwa [← div_le_iff₀' (Int.cast_pos.mpr n_pos)]
         _ = (b - a) * (2 * Real.pi) * n := by ring
       exact add_pos zero_lt_one (mul_pos (Int.cast_pos.mpr n_pos) (gt_of_ge_of_gt h pi_div_n_pos))
     _ = 2 * Real.pi * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by

Carleson/Defs.lean

@@ -1,9 +1,6 @@
 import Carleson.DoublingMeasure
 import Carleson.WeakType
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open MeasureTheory Measure NNReal Metric Complex Set TopologicalSpace Bornology Function
 open scoped ENNReal
 noncomputable section

Carleson/Discrete/Defs.lean

@@ -1,9 +1,6 @@
 import Carleson.Forest
 import Carleson.MinLayerTiles
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
 open scoped ENNReal
 open Classical -- We use quite some `Finset.filter`

Carleson/Discrete/ExceptionalSet.lean

@@ -1,9 +1,6 @@
 import Carleson.Discrete.Defs
 import Carleson.HardyLittlewood
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
 open scoped ENNReal
 open Classical -- We use quite some `Finset.filter`
@@ -74,7 +71,7 @@ lemma first_exception' : volume (G₁ : Set X) ≤ 2 ^ (- 5 : ℤ) * volume G :=
     exact mul_pos_iff.2 ⟨ENNReal.pow_pos two_pos _, measure_pos_of_superset subset_rfl hF⟩
   have K_ne_top : K ≠ ⊤ := by
     simp only [K]
-    refine ne_of_lt (div_lt_top (ne_of_lt (mul_lt_top (pow_ne_top two_ne_top) ?_)) hG)
+    refine (div_lt_top (mul_ne_top (pow_ne_top two_ne_top) ?_) hG).ne
     exact (measure_mono (ProofData.F_subset)).trans_lt measure_ball_lt_top |>.ne
   -- Define function `r : 𝔓 X → ℝ`, with garbage value `0` for `p ∉ highDensityTiles`
   have : ∀ p ∈ highDensityTiles, ∃ r ≥ 4 * (D : ℝ) ^ 𝔰 p,
@@ -206,8 +203,8 @@ lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))
     at mx
   simp_rw [mem_setOf_eq, and_assoc] at mx
   have mid0 : stackSize { p' ∈ 𝔐 k n | ¬𝓘 p' ≤ L ∧ Disjoint (𝓘 p' : Set X) L} x = 0 := by
-    simp_rw [stackSize, Finset.sum_eq_zero_iff, indicator_apply_eq_zero, imp_false,
-      Finset.mem_filter, Finset.mem_univ, true_and]
+    simp_rw [stackSize, Finset.sum_eq_zero_iff, indicator_apply_eq_zero,
+      show ¬(1 : X → ℕ) x = 0 by simp, imp_false, Finset.mem_filter, Finset.mem_univ, true_and]
     rintro y ⟨-, -, dj2⟩
     exact disjoint_right.mp dj2 mx₂
   rw [mid0, zero_add] at mx

Carleson/Discrete/Forests.lean

@@ -1,8 +1,5 @@
 import Carleson.Discrete.ExceptionalSet
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
 open scoped ENNReal
 open Classical -- We use quite some `Finset.filter`

Carleson/FinitaryCarleson.lean

@@ -1,9 +1,6 @@
 import Carleson.Discrete.Forests
 import Carleson.TileExistence
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology Classical
 open scoped ENNReal
 noncomputable section

Carleson/Forest.lean

@@ -1,8 +1,5 @@
 import Carleson.TileStructure
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open Set MeasureTheory Metric Function Complex Bornology Classical
 open scoped NNReal ENNReal ComplexConjugate
 noncomputable section

Carleson/GridStructure.lean

@@ -1,8 +1,5 @@
 import Carleson.Defs
 
--- https://github.com/leanprover/lean4/issues/4947
-attribute [-simp] Nat.reducePow
-
 open Set MeasureTheory Metric Function Complex Bornology
 open scoped NNReal ENNReal ComplexConjugate
 noncomputable section
@@ -63,7 +60,7 @@ variable {i j : Grid X}
 instance : Inhabited (Grid X) := ⟨topCube⟩
 instance : Fintype (Grid X) := GridStructure.fintype_Grid
 instance : Coe (Grid X) (Set X) := ⟨GridStructure.coeGrid⟩
-instance : Membership X (Grid X) := ⟨fun x i ↦ x ∈ (i : Set X)⟩
+instance : Membership X (Grid X) := ⟨fun i x ↦ x ∈ (i : Set X)⟩
 instance : PartialOrder (Grid X) := PartialOrder.lift _ GridStructure.inj
 /- These should probably not/only rarely be used. I comment them out for now,
 so that we don't accidentally use it. We can put it back if useful after all. -/
@@ -306,7 +303,7 @@ lemma dist_strictMono {I J : Grid X} (hpq : I < J) {f g : Θ X} :
     _ ≤ dist_{c I, 4 * D ^ s I} f g :=
       cdist_mono (ball_subset_ball (by simp_rw [div_eq_inv_mul, defaultD]; gcongr; norm_num))
     _ ≤ 2 ^ (-100 * (a : ℝ)) * dist_{c I, 4 * D ^ (s I + 1)} f g := by
-      rw [← div_le_iff' (by positivity), neg_mul, Real.rpow_neg zero_le_two, div_inv_eq_mul, mul_comm]
+      rw [← div_le_iff₀' (by positivity), neg_mul, Real.rpow_neg zero_le_two, div_inv_eq_mul, mul_comm]
       convert le_cdist_iterate (x := c I) (r := 4 * D ^ s I) (by positivity) f g (100 * a) using 1
       · norm_cast
       · apply dist_congr rfl

Carleson/HardyLittlewood.lean

@@ -60,8 +60,8 @@ private lemma P'_of_P [BorelSpace X] [ProperSpace X] [IsFiniteMeasureOnCompacts
       (coe_nnnorm_ae_le_eLpNormEssSup u μ).mono (by tauto)
     apply lt_of_le_of_lt (MeasureTheory.setLIntegral_mono_ae' measurableSet_ball hfg)
     rw [MeasureTheory.setLIntegral_const (ball c r) (eLpNormEssSup u μ)]
-    refine ENNReal.mul_lt_top ?_ (measure_ball_ne_top c r)
-    exact eLpNorm_exponent_top (f := u) ▸ hu.eLpNorm_lt_top |>.ne
+    refine ENNReal.mul_lt_top ?_ measure_ball_lt_top
+    exact eLpNorm_exponent_top (f := u) ▸ hu.eLpNorm_lt_top
   · have := hu.eLpNorm_lt_top
     simp [eLpNorm, one_ne_zero, reduceIte, ENNReal.one_ne_top, eLpNorm', ENNReal.one_toReal,
       ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self] at this
@@ -80,7 +80,7 @@ private lemma P'.add [MeasurableSpace E] [BorelSpace E]
 private lemma P'.smul [NormedSpace ℝ E] {f : X → E} (hf : P' μ f) (s : ℝ) : P' μ (s • f) := by
   refine ⟨AEStronglyMeasurable.const_smul hf.1 s, fun c r ↦ ?_⟩
   simp_rw [Pi.smul_apply, nnnorm_smul, ENNReal.coe_mul, lintegral_const_mul' _ _ ENNReal.coe_ne_top]
-  exact ENNReal.mul_lt_top ENNReal.coe_ne_top (hf.2 c r).ne
+  exact ENNReal.mul_lt_top ENNReal.coe_lt_top (hf.2 c r)
 
 -- The average that appears in the definition of `MB`
 variable (μ c r) in
@@ -165,7 +165,7 @@ protected theorem HasStrongType.MB_top [BorelSpace X] (h𝓑 : 𝓑.Countable) :
   intro f _
   use AEStronglyMeasurable.maximalFunction_toReal h𝓑
   simp only [ENNReal.coe_one, one_mul, eLpNorm_exponent_top]
-  refine essSup_le_of_ae_le _ (eventually_of_forall fun x ↦ ?_)
+  refine essSup_le_of_ae_le _ (Eventually.of_forall fun x ↦ ?_)
   simp_rw [ENNReal.nnorm_toReal]
   refine ENNReal.coe_toNNReal_le_self |>.trans ?_
   apply MB_le_eLpNormEssSup