Bump mathlib

LeanAPAP/FiniteField.lean

@@ -120,7 +120,7 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N
     calc
       γ ^ (-(↑p)⁻¹ : ℝ) = √(γ⁻¹ ^ ((↑⌈1 + log γ⁻¹⌉₊)⁻¹ : ℝ)) := by
         rw [rpow_neg hγ.le, inv_rpow hγ.le]
-        unfold_let p
+        unfold p
         push_cast
         rw [mul_inv_rev, rpow_mul, sqrt_eq_rpow, one_div, inv_rpow] <;> positivity
       _ ≤ √(γ⁻¹ ^ ((1 + log γ⁻¹)⁻¹ : ℝ)) := by gcongr; assumption; exact Nat.le_ceil _
@@ -262,7 +262,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
   let q' : ℕ := 2 * ⌈p' + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊
   have : 0 < 𝓛 γ := curlog_pos hγ.le hγ₁
   have hα₀ : 0 < α := by positivity
-  have hα₁ : α ≤ 1 := by unfold_let α; exact mod_cast A.dens_le_one
+  have hα₁ : α ≤ 1 := by unfold α; exact mod_cast A.dens_le_one
   have : 0 < p := by positivity
   have : 0 < log (6 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith)
   have : 0 < p' := pos_iff_ne_zero.2 $ by rintro rfl; simp at unbalancing; linarith
@@ -273,9 +273,9 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
   have :=
     calc
       (q' : ℝ) ≤ ↑(2 * ⌈2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p + 2 ^ 8 * ε⁻¹ ^ 2 * (64 / ε)⌉₊) := by
-        unfold_let q'; gcongr; exact log_le_self (by positivity)
+        unfold q'; gcongr; exact log_le_self (by positivity)
       _ = 2 * ⌈2 ^ 13 * ε⁻¹ ^ 2 * ⌈𝓛 γ⌉₊ + 2 ^ 14 * ε⁻¹ ^ 3 * 1⌉₊ := by
-        unfold_let p; push_cast; ring_nf
+        unfold p; push_cast; ring_nf
       _ ≤ 2 * ⌈2 ^ 13 * ε⁻¹ ^ 3 * (2 * 𝓛 γ) + 2 ^ 14 * ε⁻¹ ^ 3 * 𝓛 γ⌉₊ := by
         gcongr
         · assumption
@@ -306,13 +306,13 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           · norm_num
         _ ≤ ⌈2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ := Nat.le_ceil _
         _ = ↑(1 * ⌈0 + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊) := by rw [one_mul, zero_add]
-        _ ≤ q' := by unfold_let q'; gcongr; norm_num; positivity) hA₀
+        _ ≤ q' := by unfold q'; gcongr; norm_num; positivity) hA₀
   have :=
     calc
       p' = 1 * ⌈(p' + 0 : ℝ)⌉₊ := by simp
-      _ ≤ q' := by unfold_let q'; gcongr; norm_num; positivity
+      _ ≤ q' := by unfold q'; gcongr; norm_num; positivity
   have : card G • (f ○ f) + 1 = card G • (μ A ○ μ A) := by
-    unfold_let f
+    unfold f
     rw [← balance_dconv, balance, smul_sub, smul_const, Fintype.card_smul_expect]
     simp [sum_dconv, hA₀]
   have :=

LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean

@@ -1,5 +1,5 @@
 import Mathlib.Algebra.DirectSum.AddChar
-import Mathlib.GroupTheory.FiniteAbelian
+import Mathlib.GroupTheory.FiniteAbelian.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Prereqs.AddChar.Basic
 

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -124,14 +124,14 @@ lemma mem_chordSet_iff_norm_width : x ∈ B.chordSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.
 
 /-! ### Lattice structure -/
 
-noncomputable instance : Sup (BohrSet G) where
-  sup B₁ B₂ :=
+noncomputable instance : Max (BohrSet G) where
+  max B₁ B₂ :=
     { frequencies := B₁.frequencies ∩ B₂.frequencies,
       ewidth := fun ψ => B₁.ewidth ψ ⊔ B₂.ewidth ψ,
       mem_frequencies := fun ψ => by simp [mem_frequencies] }
 
-noncomputable instance : Inf (BohrSet G) where
-  inf B₁ B₂ :=
+noncomputable instance : Min (BohrSet G) where
+  min B₁ B₂ :=
     { frequencies := B₁.frequencies ∪ B₂.frequencies,
       ewidth := fun ψ => B₁.ewidth ψ ⊓ B₂.ewidth ψ,
       mem_frequencies := fun ψ => by simp [mem_frequencies] }

LeanAPAP/Prereqs/Chang.lean

@@ -53,8 +53,8 @@ example : 0 < changConst := by positivity
 
 end Mathlib.Meta.Positivity
 
-lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G}
-    (hs : AddDissociated (s : Set G)) (n : ℕ) :
+lemma AddDissociated.boringEnergy_le [MeasurableSpace G] [DiscreteMeasurableSpace G] [DecidableEq G]
+    {s : Finset G} (hs : AddDissociated (s : Set G)) (n : ℕ) :
     boringEnergy n s ≤ changConst ^ n * n ^ n * #s ^ n := by
   obtain rfl | hn := eq_or_ne n 0
   · simp
@@ -193,5 +193,5 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
   calc
     α⁻¹ = exp (0 + log α⁻¹) := by rw [zero_add, exp_log]; norm_cast; positivity
     _ ≤ exp ⌈0 + log α⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
-    _ ≤ exp β := by unfold_let β; gcongr; exact zero_le_one
+    _ ≤ exp β := by unfold β; gcongr; exact zero_le_one
   all_goals positivity

LeanAPAP/Prereqs/Energy.lean

@@ -45,8 +45,8 @@ lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭
 @[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = #s := by
   simp [boringEnergy_eq, indicate_apply]
 
-lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
-    ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) = boringEnergy n s := by
+lemma cLpNorm_dft_indicate_pow [MeasurableSpace G] [DiscreteMeasurableSpace G] (n : ℕ)
+    (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) = boringEnergy n s := by
   obtain rfl | hn := n.eq_zero_or_pos
   · simp
   refine Complex.ofReal_injective ?_
@@ -63,7 +63,8 @@ lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
       Nat.cast_eq_zero, Fintype.card_ne_zero, or_false, sq, Complex.ofReal_iterConv,
       (((indicate_isSelfAdjoint _).iterConv _).apply _).conj_eq, Complex.ofReal_comp_indicate]
 
-lemma cL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt #s := by
+lemma cL2Norm_dft_indicate [MeasurableSpace G] [DiscreteMeasurableSpace G] (s : Finset G) :
+    ‖dft (𝟭 s)‖ₙ_[2] = sqrt #s := by
   rw [eq_comm, sqrt_eq_iff_eq_sq, eq_comm]
   simpa using cLpNorm_dft_indicate_pow 1 s
   all_goals positivity

LeanAPAP/Prereqs/LpNorm/Compact.lean

@@ -248,13 +248,13 @@ private lemma cLpNorm_pos_of_pos {α E : Type*} {_ : MeasurableSpace α} [Discre
 @[positivity ‖_‖ₙ_[_]] def evalcLpNorm : PositivityExt where eval {u} α _z _p e := do
   match u, α, e with
   | 0, ~q(ℝ≥0), ~q(@cLpNorm $ι $E $instιmeas $instEnorm $p $f) =>
-    let pp ← (← core q(inferInstance) q(inferInstance) p).toNonzero _ _
+    let some pp := (← core q(inferInstance) q(inferInstance) p).toNonzero _ _ | failure
     try
       let _pE ← synthInstanceQ q(PartialOrder $E)
       assumeInstancesCommute
       let _ ← synthInstanceQ q(Fintype $ι)
       let _ ← synthInstanceQ q(DiscreteMeasurableSpace $ι)
-      let pf ← (← core q(inferInstance) q(inferInstance) f).toNonzero _ _
+      let some pf := (← core q(inferInstance) q(inferInstance) f).toNonzero _ _ | failure
       return .positive q(cLpNorm_pos_of_ne_zero $pp $pf)
     catch _ =>
       assumeInstancesCommute

LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean

@@ -243,13 +243,13 @@ private lemma dLpNorm_pos_of_pos {α E : Type*} {_ : MeasurableSpace α} [Discre
 @[positivity ‖_‖_[_]] def evalDLpNorm : PositivityExt where eval {u} α _z _p e := do
   match u, α, e with
   | 0, ~q(ℝ≥0), ~q(@dLpNorm $ι $E $instιmeas $instEnorm $p $f) =>
-    let pp ← (← core q(inferInstance) q(inferInstance) p).toNonzero _ _
+    let some pp := (← core q(inferInstance) q(inferInstance) p).toNonzero _ _ | failure
     try
       let _pE ← synthInstanceQ q(PartialOrder $E)
       assumeInstancesCommute
       let _ ← synthInstanceQ q(Fintype $ι)
       let _ ← synthInstanceQ q(DiscreteMeasurableSpace $ι)
-      let pf ← (← core q(inferInstance) q(inferInstance) f).toNonzero _ _
+      let some pf := (← core q(inferInstance) q(inferInstance) f).toNonzero _ _ | failure
       return .positive q(dLpNorm_pos_of_ne_zero $pp $pf)
     catch _ =>
       assumeInstancesCommute

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
+   "rev": "af731107d531b39cd7278c73f91c573f40340612",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "45d016d59cf45bcf8493a203e9564cfec5203d9b",
+   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0f1430e6f1193929f13905d450b2a44a54f3927e",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "88fac4fdcd3f426be4d972e0d3a7c78458e0bf01",
+   "rev": "62a2cc31bac6416736c17a57383a622c208f21cb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
+   "rev": "e18c6c23dd7cb1f12d79d6304262351df943aa37",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:v4.14.0-rc2