Bump mathlib

LeanAPAP/Extras/BSG.lean

@@ -258,10 +258,7 @@ lemma oneOfPair_bound_one :
           simp only [oneOfPair, ←filter_not, Prod.forall, not_le, not_lt, mem_filter] at hi
           exact hi.2.le
        _ = (X \ oneOfPair H X).card * ((3 / 4 : ℝ) * X.card) := by simp
-       _ ≤ X.card * ((3 / 4 : ℝ) * X.card) :=
-          mul_le_mul_of_nonneg_right
-            (Nat.cast_le.2 (card_le_card (sdiff_subset _ _)))
-            (by positivity)
+       _ ≤ X.card * ((3 / 4 : ℝ) * X.card) := by gcongr; exact sdiff_subset
        _ = _ := by ring
 
 lemma oneOfPair_bound_two (hH : H ⊆ X ×ˢ X) (Hcard : (7 / 8 : ℝ) * X.card ^ 2 ≤ H.card) :

LeanAPAP/Mathlib/Algebra/Group/AddChar.lean

@@ -1,13 +1,5 @@
 import Mathlib.Algebra.Group.AddChar
 
-/-!
-### TODO
-
-Rename
-* `map_add_mul` → `map_add_eq_mul`
-* `map_zero_one` → `map_zero_eq_one`
-* `map_nsmul_pow` → `map_nsmul_eq_pow`
--/
 
 open Finset hiding card
 open Fintype (card)
@@ -118,10 +110,10 @@ lemma compAddMonoidHom_injective_right (ψ : AddChar H R) (hψ : Injective ψ) :
 /-- The double dual embedding. -/
 def doubleDualEmb : G →+ AddChar (AddChar G R) R where
   toFun a := { toFun := fun ψ ↦ ψ a
-               map_zero_one' := by simp
-               map_add_mul' := by simp }
+               map_zero_eq_one' := by simp
+               map_add_eq_mul' := by simp }
   map_zero' := by ext; simp
-  map_add' _ _ := by ext; simp [map_add_mul]
+  map_add' _ _ := by ext; simp [map_add_eq_mul]
 
 @[simp] lemma doubleDualEmb_apply (a : G) (ψ : AddChar G R) : doubleDualEmb a ψ = ψ a := rfl
 
@@ -150,7 +142,7 @@ lemma sum_eq_ite (ψ : AddChar G R) : ∑ a, ψ a = if ψ = 0 then ↑(card G) e
   obtain ⟨x, hx⟩ := ne_one_iff.1 h
   refine' eq_zero_of_mul_eq_self_left hx _
   rw [Finset.mul_sum]
-  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_mul _ _ _).symm
+  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm
 
 lemma sum_eq_zero_iff_ne_zero : ∑ x, ψ x = 0 ↔ ψ ≠ 0 := by
   rw [sum_eq_ite, Ne.ite_eq_right_iff]
@@ -183,14 +175,6 @@ end CommMonoid
 section DivisionCommMonoid
 variable [DivisionCommMonoid R]
 
--- TODO: Replace `map_zsmul_zpow`
-@[simp]
-lemma map_zsmul_eq_zpow (ψ : AddChar G R) (n : ℤ) (a : G) : ψ (n • a) = ψ a ^ n :=
-  map_zpow ψ.toMonoidHom _ _
-
-lemma map_neg_eq_inv (ψ : AddChar G R) (x : G) : ψ (-x) = (ψ x)⁻¹ :=
-  eq_inv_of_mul_eq_one_left $ by simp [← map_add_mul]
-
 lemma neg_apply' (ψ : AddChar G R) (x : G) : (-ψ) x = (ψ x)⁻¹ :=
   map_neg_eq_inv _ _
 

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -442,7 +442,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
   set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C
   have hT' : T.Nonempty := by
     have := hS.card_pos -- TODO: positivity
-    have : 0 < _ := hKT.trans_lt' $ by positivity
+    have : (0 : ℝ) < T.card := hKT.trans_lt' $ by positivity
     simpa [card_pos] using this
   calc
     ‖μ T ∗^ k ∗ F - F‖_[∞]

LeanAPAP/Physics/DRC.lean

@@ -61,8 +61,8 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         ≤ A₁.card / B₁.card ∧
       (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
         ≤ A₂.card / B₂.card := by
-  have := hB.mono $ inter_subset_left _ _
-  have := hB.mono $ inter_subset_right _ _
+  have := hB.mono inter_subset_left
+  have := hB.mono inter_subset_right
   have hp₀ : p ≠ 0 := by positivity
   have := lpNorm_conv_pos hp₀ hB hA
   set M : ℝ :=
@@ -91,7 +91,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     < ∑ s, 𝟭 (univ.filter fun s ↦ M ^ 2 ≤ g s) s * g s *
         (2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x) by
     obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this
-    refine ⟨_, inter_subset_left _ $ c p A s, _, inter_subset_left _ $ c p A s, ?_⟩
+    refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩
     simp only [indicate_apply, mem_filter, mem_univ, true_and_iff, boole_mul] at hs
     split_ifs at hs with h; swap
     · simp only [zero_mul, l2Inner_eq_sum, Function.comp_apply, RCLike.inner_apply,
@@ -111,7 +111,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     · simp_rw [A₁, A₂, g, ←card_smul_mu, smul_dconv, dconv_smul, l2Inner_smul_left, star_trivial,
         nsmul_eq_mul, mul_assoc]
     any_goals positivity
-    all_goals exact Nat.cast_le.2 $ card_mono $ inter_subset_left _ _
+    all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left
   rw [←sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ←sum_mul, mul_right_comm, ←hgB, mul_left_comm,
     ←mul_assoc]
   simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and_iff, ←sum_filter,

LeanAPAP/Prereqs/AddChar/Basic.lean

@@ -2,15 +2,6 @@ import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Prereqs.Discrete.Convolution.Basic
 import LeanAPAP.Prereqs.Discrete.LpNorm.Basic
 
-/-!
-### TODO
-
-Rename
-* `map_add_mul` → `map_add_eq_mul`
-* `map_zero_one` → `map_zero_eq_one`
-* `map_nsmul_pow` → `map_nsmul_eq_pow`
--/
-
 open Finset hiding card
 open Fintype (card)
 open Function
@@ -29,7 +20,7 @@ variable [Finite G] [NormedField R]
   (ψ.toMonoidHom.isOfFinOrder $ isOfFinOrder_of_finite _).norm_eq_one
 
 @[simp] lemma coe_ne_zero (ψ : AddChar G R) : (ψ : G → R) ≠ 0 :=
-  Function.ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_one ψ⟩
+  Function.ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩
 
 end NormedField
 
@@ -53,7 +44,7 @@ lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0
   obtain ⟨x, hx⟩ := ne_one_iff.1 h
   refine' eq_zero_of_mul_eq_self_left hx _
   rw [Finset.mul_expect]
-  exact Fintype.expect_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_mul _ _ _).symm
+  exact Fintype.expect_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul _ _ _).symm
 
 lemma expect_eq_zero_iff_ne_zero : 𝔼 x, ψ x = 0 ↔ ψ ≠ 0 := by
   rw [expect_eq_ite, one_ne_zero.ite_eq_right_iff]

LeanAPAP/Prereqs/AddChar/Circle.lean

@@ -35,16 +35,16 @@ lemma exp_eq_one : expMapCircle r = 1 ↔ ∃ n : ℤ, r = n * (2 * π) := by
 
 noncomputable def e : AddChar ℝ circle where
   toFun r := expMapCircle (2 * π * r)
-  map_zero_one' := by simp
-  map_add_mul' := by simp [mul_add, Complex.exp_add]
+  map_zero_eq_one' := by simp
+  map_add_eq_mul' := by simp [mul_add, Complex.exp_add]
 
 lemma e_apply (r : ℝ) : e r = expMapCircle (2 * π * r) := rfl
 
 @[simp, norm_cast] lemma coe_e (r : ℝ) : ↑(e r) = Complex.exp ((2 * π * r : ℝ) * Complex.I) := rfl
 
 @[simp] lemma e_int (z : ℤ) : e z = 1 := exp_two_pi_mul_int _
 @[simp] lemma e_one : e 1 = 1 := by simpa using e_int 1
-@[simp] lemma e_add_int {z : ℤ} : e (r + z) = e r := by rw [map_add_mul, e_int, mul_one]
+@[simp] lemma e_add_int {z : ℤ} : e (r + z) = e r := by rw [map_add_eq_mul, e_int, mul_one]
 @[simp] lemma e_sub_int {z : ℤ} : e (r - z) = e r := by rw [map_sub_eq_div, e_int, div_one]
 @[simp] lemma e_fract (r : ℝ) : e (Int.fract r) = e r := by rw [Int.fract, e_sub_int]
 

LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean

@@ -25,8 +25,8 @@ namespace AddChar
 
 private def zmodAuxAux (n : ℕ) : ℤ →+ Additive circle where
   toFun x := Additive.ofMul (e $ x / n)
-  map_zero' := by dsimp; rw [Int.cast_zero, zero_div, ofMul_eq_zero, map_zero_one]
-  map_add' x y := by rw [←ofMul_mul, Equiv.apply_eq_iff_eq, Int.cast_add, add_div, map_add_mul]
+  map_zero' := by dsimp; rw [Int.cast_zero, zero_div, ofMul_eq_zero, map_zero_eq_one]
+  map_add' x y := by rw [←ofMul_mul, Equiv.apply_eq_iff_eq, Int.cast_add, add_div, map_add_eq_mul]
 
 @[simp]
 lemma zmodAuxAux_apply (n : ℕ) (z : ℤ) : zmodAuxAux n z = Additive.ofMul (e $ z / n) := rfl
@@ -71,7 +71,7 @@ def zmod (n : ℕ) (x : ZMod n) : AddChar (ZMod n) circle :=
 @[simp] lemma zmod_add (n : ℕ) : ∀ x y : ZMod n, zmod n (x + y) = zmod n x * zmod n y := by
   simp only [DFunLike.ext_iff, ZMod.intCast_surjective.forall, ←Int.cast_add, AddChar.mul_apply,
     zmod_apply]
-  simp [add_mul, add_div, map_add_mul]
+  simp [add_mul, add_div, map_add_eq_mul]
 
 -- probably an evil lemma
 -- @[simp] lemma zmod_apply (n : ℕ) (x y : ZMod n) : zmod n x y = e (x * y / n) :=
@@ -91,8 +91,8 @@ lemma zmod_injective (hn : n ≠ 0) : Injective (zmod n) := by
 
 def zmodHom (n : ℕ) : AddChar (ZMod n) (AddChar (ZMod n) circle) where
   toFun := zmod n
-  map_zero_one' := by simp
-  map_add_mul' := by simp
+  map_zero_eq_one' := by simp
+  map_add_eq_mul' := by simp
 
 def mkZModAux {ι : Type} [DecidableEq ι] (n : ι → ℕ) (u : ∀ i, ZMod (n i)) :
     AddChar (⨁ i, ZMod (n i)) circle :=
@@ -108,8 +108,8 @@ def circleEquivComplex [Finite α] : AddChar α circle ≃+ AddChar α ℂ where
   toFun ψ := toMonoidHomEquiv'.symm $ circle.subtype.comp ψ.toMonoidHom
   invFun ψ :=
     { toFun := fun a ↦ (⟨ψ a, mem_circle_iff_abs.2 $ ψ.norm_apply _⟩ : circle)
-      map_zero_one' := by simp
-      map_add_mul' := fun a b ↦ by ext : 1; simp [map_add_mul] }
+      map_zero_eq_one' := by simp
+      map_add_eq_mul' := fun a b ↦ by ext : 1; simp [map_add_eq_mul] }
   left_inv ψ := by ext : 1; simp
   right_inv ψ := by ext : 1; simp
   map_add' ψ χ := rfl
@@ -157,14 +157,14 @@ lemma complexBasis_apply (ψ : AddChar α ℂ) : complexBasis α ψ = ψ := by r
 lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 := by
   refine' ⟨_, fun ha ↦ _⟩
   · rintro ⟨ψ, hψ⟩ rfl
-    exact hψ ψ.map_zero_one
+    exact hψ ψ.map_zero_eq_one
   classical
   by_contra! h
   let f : α → ℂ := fun b ↦ if a = b then 1 else 0
   have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
   have h₁ := congr_fun ((complexBasis α).sum_repr f) a
   simp only [complexBasis_apply, Fintype.sum_apply, Pi.smul_apply, h, smul_eq_mul, mul_one,
-    map_zero_one, if_pos rfl, if_neg ha, f] at h₀ h₁
+    map_zero_eq_one, if_pos rfl, if_neg ha, f] at h₀ h₁
   exact one_ne_zero (h₁.symm.trans h₀)
 
 lemma forall_apply_eq_zero : (∀ ψ : AddChar α ℂ, ψ a = 1) ↔ a = 0 := by

LeanAPAP/Prereqs/Density.lean

@@ -153,8 +153,8 @@ lemma dens_sdiff (h : s ⊆ t) : dens[𝕜] (t \ s) = dens t - dens s := by
 
 lemma le_dens_sdiff (s t : Finset α) : dens[𝕜] t - dens s ≤ dens (t \ s) :=
   calc
-    _ ≤ dens t - dens (s ∩ t) := tsub_le_tsub_left (dens_mono (inter_subset_left s t)) _
-    _ = dens[𝕜] (t \ s) := by rw [← dens_sdiff (inter_subset_right s t), sdiff_inter_self_right t s]
+    _ ≤ dens t - dens (s ∩ t) := tsub_le_tsub_left (dens_mono inter_subset_left) _
+    _ = dens[𝕜] (t \ s) := by rw [← dens_sdiff inter_subset_right, sdiff_inter_self_right t s]
 
 end Lattice
 

LeanAPAP/Prereqs/Discrete/DFT/Basic.lean

@@ -55,7 +55,7 @@ lemma dft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = ⟪ψ, f⟫_
   unfold dft
   simp_rw [l2Inner_eq_sum, nl2Inner_eq_expect, map_sum, map_mul, starRingEnd_self_apply, sum_mul,
     mul_sum, expect_sum_comm, mul_mul_mul_comm _ (conj $ f _), ←expect_mul, ←
-    AddChar.inv_apply_eq_conj, ←map_neg_eq_inv, ←map_add_mul, AddChar.expect_apply_eq_ite,
+    AddChar.inv_apply_eq_conj, ←map_neg_eq_inv, ←map_add_eq_mul, AddChar.expect_apply_eq_ite,
     add_neg_eq_zero, boole_mul, Fintype.sum_ite_eq]
 
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
@@ -113,7 +113,7 @@ lemma dft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime
   simp_rw [dft_apply, l2Inner_eq_sum, dilate]
   rw [← Nat.card_eq_fintype_card] at hn
   refine (Fintype.sum_bijective _ hn.nsmul_right_bijective _ _  ?_).symm
-  simp only [pow_apply, ← map_nsmul_pow, zmod_val_inv_nsmul_nsmul hn, forall_const]
+  simp only [pow_apply, ← map_nsmul_eq_pow, zmod_val_inv_nsmul_nsmul hn, forall_const]
 
 @[simp] lemma dft_trivChar [DecidableEq α] : dft (trivChar : α → ℂ) = 1 := by
   ext; simp [trivChar_apply, dft_apply, l2Inner_eq_sum, ←map_sum]
@@ -133,7 +133,7 @@ lemma dft_conv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : dft (f ∗ g) ψ
     ((Equiv.refl _).prodShear Equiv.subRight).trans $ Equiv.prodComm _ _)  _ _ fun (a, b) ↦ ?_
   simp only [Equiv.trans_apply, Equiv.prodComm_apply, Equiv.prodShear_apply, Prod.fst_swap,
     Equiv.refl_apply, Prod.snd_swap, Equiv.subRight_apply, Prod.swap_prod_mk, Prod.forall]
-  rw [mul_mul_mul_comm, ←map_mul, ←map_add_mul, add_sub_cancel]
+  rw [mul_mul_mul_comm, ←map_mul, ←map_add_eq_mul, add_sub_cancel]
 
 lemma dft_dconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) :
     dft (f ○ g) ψ = dft f ψ * conj (dft g ψ) := by

LeanAPAP/Prereqs/Discrete/DFT/Compact.lean

@@ -48,7 +48,7 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫
   unfold cft
   simp_rw [l2Inner_eq_sum, nl2Inner_eq_expect, map_expect, map_mul, starRingEnd_self_apply,
     expect_mul, mul_expect, ← expect_sum_comm, mul_mul_mul_comm _ (conj $ f _), ← sum_mul, ←
-    AddChar.inv_apply_eq_conj, ←map_neg_eq_inv, ←map_add_mul, AddChar.sum_apply_eq_ite]
+    AddChar.inv_apply_eq_conj, ←map_neg_eq_inv, ←map_add_eq_mul, AddChar.sum_apply_eq_ite]
   simp [add_neg_eq_zero, card_univ, Fintype.card_ne_zero, NNRat.smul_def (α := ℂ)]
 
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
@@ -107,7 +107,7 @@ lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime
   simp_rw [cft_apply, nl2Inner_eq_expect, dilate]
   rw [← Nat.card_eq_fintype_card] at hn
   refine (Fintype.expect_bijective _ hn.nsmul_right_bijective _ _  ?_).symm
-  simp only [pow_apply, ← map_nsmul_pow, zmod_val_inv_nsmul_nsmul hn, forall_const]
+  simp only [pow_apply, ← map_nsmul_eq_pow, zmod_val_inv_nsmul_nsmul hn, forall_const]
 
 @[simp] lemma cft_trivNChar [DecidableEq α] : cft (trivNChar : α → ℂ) = 1 := by
   ext
@@ -131,7 +131,7 @@ lemma cft_nconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g
     ((Equiv.refl _).prodShear Equiv.subRight).trans $ Equiv.prodComm _ _)  _ _ fun (a, b) ↦ ?_
   simp only [Equiv.trans_apply, Equiv.prodComm_apply, Equiv.prodShear_apply, Prod.fst_swap,
     Equiv.refl_apply, Prod.snd_swap, Equiv.subRight_apply, Prod.swap_prod_mk, Prod.forall]
-  rw [mul_mul_mul_comm, ←map_mul, ←map_add_mul, add_sub_cancel]
+  rw [mul_mul_mul_comm, ←map_mul, ←map_add_eq_mul, add_sub_cancel]
 
 lemma cft_ndconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) :
     cft (f ○ₙ g) ψ = cft f ψ * conj (cft g ψ) := by

LeanAPAP/Prereqs/Expect/Basic.lean

@@ -202,10 +202,10 @@ lemma expect_image [DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m)
 end bij
 
 @[simp] lemma expect_inv_index [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) :
-    𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹ := expect_image $ inv_injective.injOn _
+    𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹ := expect_image inv_injective.injOn
 
 @[simp] lemma expect_neg_index [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → α) :
-    𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) := expect_image $ neg_injective.injOn _
+    𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) := expect_image neg_injective.injOn
 
 lemma _root_.map_expect {F : Type*} [FunLike F α β] [LinearMapClass F ℚ≥0 α β]
     (g : F) (f : ι → α) (s : Finset ι) :
@@ -423,7 +423,7 @@ variable [AddCommMonoid α] [Module ℚ≥0 α] {f : ι → α}
 See `Function.Bijective.expect_comp` for a version without `h`. -/
 lemma expect_bijective (e : ι → κ) (he : Bijective e) (f : ι → α) (g : κ → α)
     (h : ∀ x, f x = g (e x)) : 𝔼 i, f i = 𝔼 i, g i :=
-  expect_nbij (fun _ ↦ e _) (fun _ _ ↦ mem_univ _) (fun x _ ↦ h x) (he.injective.injOn _) $ by
+  expect_nbij e (fun _ _ ↦ mem_univ _) (fun x _ ↦ h x) he.injective.injOn $ by
     simpa using he.surjective.surjOn _
 
 /-- `Fintype.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in

lake-manifest.json

@@ -1,10 +1,10 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "dfe82086e9904edfc04eb0f5205c85647956897d",
+   "rev": "6a63eb6a326181df29d95a84ce1f16c1145e66d8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "d68b34fabd37681e6732be752b7e90aaac7aa0e0",
+   "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
+   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "6f758e582b2ad1cb121bf88aa1a178e284315af5",
+   "rev": "c995db1feabfe4b1d204e24ac689001d44484bc9",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -76,7 +76,7 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "effd8b8771cfd7ece69db99448168078e113c61f",
+   "rev": "ef8b0ae5d48e7d5f5d538bf8d66f6cdc7daba296",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -94,7 +94,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "87022a3314f973c59f130ee581afb4797d7f890e",
+   "rev": "4e570fed8c4147bdafbd5eada08503ed307252e0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

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