diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 5bb2f2816d..3a884cb805 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -8,13 +8,13 @@ import LeanAPAP.Mathlib.Algebra.BigOperators.Pi
 import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
 import LeanAPAP.Mathlib.Algebra.DirectSum.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Basic
+import LeanAPAP.Mathlib.Algebra.Group.Equiv.Basic
+import LeanAPAP.Mathlib.Algebra.Group.Hom.Defs
+import LeanAPAP.Mathlib.Algebra.Group.Hom.Instances
 import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
 import LeanAPAP.Mathlib.Algebra.GroupPower.Hom
 import LeanAPAP.Mathlib.Algebra.GroupPower.Order
 import LeanAPAP.Mathlib.Algebra.Group.TypeTags
-import LeanAPAP.Mathlib.Algebra.Hom.Equiv.Basic
-import LeanAPAP.Mathlib.Algebra.Hom.Group
-import LeanAPAP.Mathlib.Algebra.Hom.GroupInstances
 import LeanAPAP.Mathlib.Algebra.Module.Basic
 import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical
diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Basic.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Basic.lean
index d359057fb2..718f07bc65 100644
--- a/LeanAPAP/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Basic.lean
@@ -59,7 +59,7 @@ def processBigOpBinder (processed : (Array (Term × Term)))
     | `(bigOpBinder| $x:term) =>
       match x with
       | `(($a + $b = $n)) => -- Maybe this is too cute.
-        return processed |>.push (← `(⟨$a, $b⟩), ← `(Finset.Nat.antidiagonal $n))
+        return processed |>.push (← `(⟨$a, $b⟩), ← `(Finset.HasAntidiagonal.antidiagonal $n))
       | _ => return processed |>.push (x, ← ``(Finset.univ))
     | `(bigOpBinder| $x : $t) => return processed |>.push (x, ← ``((Finset.univ : Finset $t)))
     | `(bigOpBinder| $x ∈ $s) => return processed |>.push (x, ← `(finset% $s))
diff --git a/LeanAPAP/Mathlib/Algebra/Hom/Equiv/Basic.lean b/LeanAPAP/Mathlib/Algebra/Group/Equiv/Basic.lean
similarity index 95%
rename from LeanAPAP/Mathlib/Algebra/Hom/Equiv/Basic.lean
rename to LeanAPAP/Mathlib/Algebra/Group/Equiv/Basic.lean
index 4e13447335..f7c3e9adb8 100644
--- a/LeanAPAP/Mathlib/Algebra/Hom/Equiv/Basic.lean
+++ b/LeanAPAP/Mathlib/Algebra/Group/Equiv/Basic.lean
@@ -1,4 +1,4 @@
-import Mathlib.Algebra.Hom.Equiv.Basic
+import Mathlib.Algebra.Group.Equiv.Basic
 
 open Function
 
diff --git a/LeanAPAP/Mathlib/Algebra/Hom/Group.lean b/LeanAPAP/Mathlib/Algebra/Group/Hom/Defs.lean
similarity index 91%
rename from LeanAPAP/Mathlib/Algebra/Hom/Group.lean
rename to LeanAPAP/Mathlib/Algebra/Group/Hom/Defs.lean
index 1216eb9a24..09e1b18684 100644
--- a/LeanAPAP/Mathlib/Algebra/Hom/Group.lean
+++ b/LeanAPAP/Mathlib/Algebra/Group/Hom/Defs.lean
@@ -1,4 +1,4 @@
-import Mathlib.Algebra.Hom.Group.Defs
+import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Tactic.Coe
 
 namespace AddMonoid.End
diff --git a/LeanAPAP/Mathlib/Algebra/Hom/GroupInstances.lean b/LeanAPAP/Mathlib/Algebra/Group/Hom/Instances.lean
similarity index 95%
rename from LeanAPAP/Mathlib/Algebra/Hom/GroupInstances.lean
rename to LeanAPAP/Mathlib/Algebra/Group/Hom/Instances.lean
index 90be043267..1b441e519a 100644
--- a/LeanAPAP/Mathlib/Algebra/Hom/GroupInstances.lean
+++ b/LeanAPAP/Mathlib/Algebra/Group/Hom/Instances.lean
@@ -1,4 +1,4 @@
-import Mathlib.Algebra.Hom.GroupInstances
+import Mathlib.Algebra.Group.Hom.Instances
 import Mathlib.Data.Pi.Algebra
 
 variable {α β : Type*}
diff --git a/LeanAPAP/Mathlib/Algebra/GroupPower/Hom.lean b/LeanAPAP/Mathlib/Algebra/GroupPower/Hom.lean
index 851a1ce7df..df8c01c4bc 100644
--- a/LeanAPAP/Mathlib/Algebra/GroupPower/Hom.lean
+++ b/LeanAPAP/Mathlib/Algebra/GroupPower/Hom.lean
@@ -1,5 +1,5 @@
-import LeanAPAP.Mathlib.Algebra.Hom.Group
-import LeanAPAP.Mathlib.Algebra.Hom.GroupInstances
+import LeanAPAP.Mathlib.Algebra.Group.Hom.Defs
+import LeanAPAP.Mathlib.Algebra.Group.Hom.Instances
 import LeanAPAP.Mathlib.GroupTheory.OrderOfElement
 
 open Finset Function
diff --git a/LeanAPAP/Mathlib/Data/Finset/NatAntidiagonal.lean b/LeanAPAP/Mathlib/Data/Finset/NatAntidiagonal.lean
index d3a4fbeb07..d88a946db6 100644
--- a/LeanAPAP/Mathlib/Data/Finset/NatAntidiagonal.lean
+++ b/LeanAPAP/Mathlib/Data/Finset/NatAntidiagonal.lean
@@ -17,10 +17,10 @@ lemma antidiagonal_congr' (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n
   exact antidiagonal_congr (swap_mem_antidiagonal hp) (swap_mem_antidiagonal hq)
 
 lemma antidiagonal_eq_map :
-    Nat.antidiagonal n =
+    antidiagonal n =
       (range (n + 1)).map ⟨fun i ↦ (i, n - i), fun _i _j h ↦ (Prod.ext_iff.1 h).1⟩ := rfl
 
-lemma antidiagonal_eq_image : Nat.antidiagonal n = (range (n + 1)).image fun i ↦ (i, n - i) := by
+lemma antidiagonal_eq_image : antidiagonal n = (range (n + 1)).image fun i ↦ (i, n - i) := by
   simp only [antidiagonal_eq_map, map_eq_image, Function.Embedding.coeFn_mk]
 
 end Nat
diff --git a/LeanAPAP/Mathlib/Data/Finset/Pointwise.lean b/LeanAPAP/Mathlib/Data/Finset/Pointwise.lean
index 7d378be520..ae9fff1500 100644
--- a/LeanAPAP/Mathlib/Data/Finset/Pointwise.lean
+++ b/LeanAPAP/Mathlib/Data/Finset/Pointwise.lean
@@ -3,7 +3,6 @@ import LeanAPAP.Mathlib.Data.Fintype.Pi
 import Mathlib.GroupTheory.GroupAction.Pi
 
 open Finset
-
 open scoped Pointwise
 
 namespace Finset
diff --git a/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean b/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean
index 5e1f0ffe72..0738fdf39a 100644
--- a/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean
+++ b/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean
@@ -101,7 +101,7 @@ lemma nsmul_apply (n : ℕ) (ψ : AddChar G R) (a : G) : (ψ ^ n) a = ψ a ^ n :
 variable {ι : Type*}
 
 @[simp, norm_cast]
-lemma coe_sum (s : Finset ι) (ψ : ι → AddChar G R) : ⇑(∑ i in s, ψ i) = ∏ i in s, ⇑ψ i := by
+lemma coe_sum (s : Finset ι) (ψ : ι → AddChar G R) : ∑ i in s, ψ i = ∏ i in s, ⇑(ψ i) := by
   induction s using Finset.cons_induction <;> simp [*]
 
 lemma sum_apply (s : Finset ι) (ψ : ι → AddChar G R) (a : G) :
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index 84fa8e7b7b..e0aa53b98c 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -152,8 +152,6 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
     · exact rpow_nonneg (sum_nonneg fun i _ ↦ by sorry) -- positivity
     · positivity
     · exact sum_nonneg fun i _ ↦ by sorry -- positivity
-    · sorry -- positivity
-    · sorry -- positivity
   set p' := 24 / ε * log (3 / ε) * p
   have hp' : 0 < p' := p'_pos hp hε₀ hε₁
   have : 1 - 8⁻¹ * ε ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ := by
diff --git a/LeanAPAP/Prereqs/Cut.lean b/LeanAPAP/Prereqs/Cut.lean
index aa94bce967..6be5d988a7 100644
--- a/LeanAPAP/Prereqs/Cut.lean
+++ b/LeanAPAP/Prereqs/Cut.lean
@@ -39,7 +39,7 @@ lemma mem_cut (s : Finset ι) (n : ℕ) (f : ι → ℕ) :
     exact hf _
 
 lemma cut_equiv_antidiag (n : ℕ) :
-    Equiv.finsetCongr (Equiv.boolArrowEquivProd _) (cut univ n) = Nat.antidiagonal n := by
+    Equiv.finsetCongr (Equiv.boolArrowEquivProd _) (cut univ n) = antidiagonal n := by
   ext ⟨x₁, x₂⟩
   simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk, ←
     Equiv.eq_symm_apply]
@@ -63,13 +63,13 @@ lemma cut_univ_fin_eq_antidiagonalTuple (n k : ℕ) : cut univ n = Nat.antidiago
   eq_empty_of_forall_not_mem fun x ↦ by simp [mem_cut, @eq_comm _ 0]
 
 lemma cut_insert [DecidableEq (ι → ℕ)] (n : ℕ) (a : ι) (s : Finset ι) (h : a ∉ s) :
-    cut (insert a s) n = (Nat.antidiagonal n).biUnion fun p : ℕ × ℕ ↦ (cut s p.snd).map
+    cut (insert a s) n = (antidiagonal n).biUnion fun p : ℕ × ℕ ↦ (cut s p.snd).map
       (addLeftEmbedding fun t ↦ if t = a then p.fst else 0) := by
   ext f
   rw [mem_cut, mem_biUnion, sum_insert h]
   constructor
   · rintro ⟨rfl, h₁⟩
-    simp only [exists_prop, Function.Embedding.coeFn_mk, mem_map, Nat.mem_antidiagonal, Prod.exists]
+    simp only [exists_prop, Function.Embedding.coeFn_mk, mem_map, mem_antidiagonal, Prod.exists]
     refine' ⟨f a, s.sum f, rfl, fun i ↦ if i = a then 0 else f i, _, _⟩
     · rw [mem_cut]
       refine' ⟨_, _⟩
@@ -85,7 +85,7 @@ lemma cut_insert [DecidableEq (ι → ℕ)] (n : ℕ) (a : ι) (s : Finset ι) (
       obtain rfl | h := eq_or_ne x a
       · simp
       · simp [if_neg h]
-  · simp only [mem_insert, Function.Embedding.coeFn_mk, mem_map, Nat.mem_antidiagonal, Prod.exists,
+  · simp only [mem_insert, Function.Embedding.coeFn_mk, mem_map, mem_antidiagonal, Prod.exists,
       exists_prop, mem_cut, not_or]
     rintro ⟨p, q, rfl, g, ⟨rfl, hg₂⟩, rfl⟩
     refine' ⟨_, _⟩
@@ -94,7 +94,7 @@ lemma cut_insert [DecidableEq (ι → ℕ)] (n : ℕ) (a : ι) (s : Finset ι) (
       simp [if_neg h₁, hg₂ _ h₂]
 
 lemma cut_insert_disjoint_bUnion (n : ℕ) (a : ι) (s : Finset ι) (h : a ∉ s) :
-    (Nat.antidiagonal n : Set (ℕ × ℕ)).PairwiseDisjoint fun p : ℕ × ℕ ↦
+    (antidiagonal n : Set (ℕ × ℕ)).PairwiseDisjoint fun p : ℕ × ℕ ↦
       (cut s p.snd).map (addLeftEmbedding fun t ↦ if t = a then p.fst else 0) := by
   simp only [Set.PairwiseDisjoint, Function.onFun_apply, Finset.disjoint_iff_ne, mem_map,
     Function.Embedding.coeFn_mk, Ne.def, forall_exists_index, Set.Pairwise, mem_coe, mem_cut,
diff --git a/LeanAPAP/Prereqs/LpNorm.lean b/LeanAPAP/Prereqs/LpNorm.lean
index 8545ebbb72..6c064f16e4 100644
--- a/LeanAPAP/Prereqs/LpNorm.lean
+++ b/LeanAPAP/Prereqs/LpNorm.lean
@@ -57,7 +57,7 @@ lemma l2norm_eq_sum (f : ∀ i, α i) : ‖f‖_[2] = sqrt (∑ i, ‖f i‖ ^ 2
 lemma L1norm_eq_sum (f : ∀ i, α i) : ‖f‖_[1] = ∑ i, ‖f i‖ := by simp [lpNorm_eq_sum']
 
 lemma L0norm_eq_card (f : ∀ i, α i) : ‖f‖_[0] = {i | f i ≠ 0}.toFinite.toFinset.card :=
-  PiLp.norm_eq_card _
+  (PiLp.norm_eq_card _).trans $ by simp
 
 lemma Linftynorm_eq_csupr (f : ∀ i, α i) : ‖f‖_[∞] = ⨆ i, ‖f i‖ := PiLp.norm_eq_ciSup _
 
diff --git a/LeanAPAP/Prereqs/Multinomial.lean b/LeanAPAP/Prereqs/Multinomial.lean
index 4c59c17f57..3e72e5577f 100644
--- a/LeanAPAP/Prereqs/Multinomial.lean
+++ b/LeanAPAP/Prereqs/Multinomial.lean
@@ -31,7 +31,7 @@ lemma multinomial_expansion' {α β : Type*} [DecidableEq α] [CommSemiring β]
     Pi.add_apply, eq_self_iff_true, if_true, Nat.cast_mul, prod_insert has, eq_self_iff_true,
     if_true, sum_add_distrib, sum_ite_eq', has, if_false, add_zero,
       addLeftEmbedding_eq_addRightEmbedding, addRightEmbedding_apply]
-  suffices : ∀ p : ℕ × ℕ, p ∈ Nat.antidiagonal n →
+  suffices : ∀ p : ℕ × ℕ, p ∈ antidiagonal n →
     ∑ f in cut s p.snd, ((f a + p.fst + s.sum f).choose (f a + p.fst) : β) *
       multinomial s (f + fun t ↦ ite (t = a) p.fst 0) *
         (x a ^ (f a + p.fst) * ∏ t : α in s, x t ^ (f t + ite (t = a) p.fst 0)) =
@@ -46,7 +46,7 @@ lemma multinomial_expansion' {α β : Type*} [DecidableEq α] [CommSemiring β]
   rw [mem_cut] at hf
   rw [hf.2 _ has, zero_add, hf.1]
   congr 2
-  · rw [Nat.mem_antidiagonal.1 hp]
+  · rw [mem_antidiagonal.1 hp]
   · rw [multinomial_congr]
     intro t ht
     rw [Pi.add_apply, if_neg, add_zero]
diff --git a/lake-manifest.json b/lake-manifest.json
index f43d5fe9ff..287d7493fa 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "3ce43c18f614b76e161f911b75a3e1ef641620ff",
+    "rev": "adefdc2a051225c3e96946f16d99bf93cd74ba12",
     "opts": {},
     "name": "mathlib",
     "inputRev?": null,
@@ -12,7 +12,7 @@
   {"git":
    {"url": "https://github.com/leanprover/doc-gen4",
     "subDir?": null,
-    "rev": "8bccb92b531248af1b6692d65486e8640c8bcd10",
+    "rev": "162de4ad98c7c79bc1fc0b1110816247679b3ce0",
     "opts": {},
     "name": "«doc-gen4»",
     "inputRev?": "main",
@@ -20,7 +20,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "727fa6aa1113c376ea1873812d1ab5c17a24f1d2",
+    "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
@@ -28,7 +28,7 @@
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
@@ -36,7 +36,7 @@
   {"git":
    {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "b601328752091a1cfcaebdd6b6b7c30dc5ffd946",
+    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
@@ -44,18 +44,18 @@
   {"git":
    {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
     "opts": {},
     "name": "Cli",
-    "inputRev?": "nightly",
+    "inputRev?": "main",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/ProofWidgets4",
     "subDir?": null,
-    "rev": "27715d1daf32b9657dc38cd52172d77b19bde4ba",
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.18",
+    "inputRev?": "v0.0.21",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/xubaiw/CMark.lean",
@@ -68,9 +68,9 @@
   {"git":
    {"url": "https://github.com/fgdorais/lean4-unicode-basic",
     "subDir?": null,
-    "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
+    "rev": "4ecf4f1f98d14d03a9e84fa1c082630fa69df88b",
     "opts": {},
-    "name": "«lean4-unicode-basic»",
+    "name": "UnicodeBasic",
     "inputRev?": "main",
     "inherited": true}},
   {"git":
diff --git a/lean-toolchain b/lean-toolchain
index 183a307edb..e8560170ab 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.3.0-rc1
diff --git a/scripts/update_mathlib.sh b/scripts/update_mathlib.sh
old mode 100644
new mode 100755