From ad4e39226b4f393f9d57f9389d67a508f9d96a2a Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Wed, 20 May 2026 12:25:04 -0500
Subject: [PATCH 01/21] Add `YoungDiagram` conversion

---
 .../Enumerative/Partition/Basic.lean          | 29 ++++++++++++++++---
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index 6ce7063d65d58b..0cc86725a6249a 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Order.Antidiag.Finsupp
 public import Mathlib.Combinatorics.Enumerative.Composition
+public import Mathlib.Combinatorics.Young.YoungDiagram
 public import Mathlib.Tactic.ApplyFun
 
 /-!
@@ -31,10 +32,6 @@ related results.
 The representation of a partition as a multiset is very handy as multisets are very flexible and
 already have a well-developed API.
 
-## TODO
-
-Link this to Young diagrams.
-
 ## Tags
 
 Partition
@@ -229,6 +226,30 @@ theorem countRestricted_two (n : ℕ) : countRestricted n 2 = distincts n := by
 def oddDistincts (n : ℕ) : Finset n.Partition :=
   odds n ∩ distincts n
 
+/-- Convert a Young diagram to a partition. -/
+def ofYoungDiagram (μ : YoungDiagram) : Partition (μ.card) where
+  parts := μ.rowLens
+  parts_pos := μ.pos_of_mem_rowLens _
+  parts_sum := by
+    have hf : ∀ c ∈ μ.cells, c.fst ∈ Finset.range (μ.colLen 0) := by
+      intro c hc
+      rw [Finset.mem_range, ← YoungDiagram.mem_iff_lt_colLen]
+      exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
+    have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.fst = i}).card = μ.rowLen i := by
+      intro i _hi
+      rw [YoungDiagram.rowLen_eq_card]
+      rfl
+    simp only [sum_coe]
+    rw [YoungDiagram.card, Finset.card_eq_sum_card_fiberwise hf, Finset.sum_congr rfl hr,
+      YoungDiagram.rowLens, ← List.sum_toFinset, List.toFinset_range]
+    exact List.nodup_range
+
+/-- Convert a partition to a Young diagram. -/
+def toYoungDiagram (p : Partition n) : YoungDiagram :=
+  YoungDiagram.ofRowLens
+    (p.parts.sort (· ≥ ·))
+    (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
+
 end Partition
 
 end Nat

From 73823e2184dc157fbe9a7dbd6443c023eae33aca Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Fri, 22 May 2026 01:24:00 -0500
Subject: [PATCH 02/21] Add equivalence and conjugation

---
 .../Enumerative/Partition/Basic.lean          | 96 ++++++++++++++++---
 1 file changed, 83 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index 0cc86725a6249a..d992c4357b7065 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -226,30 +226,100 @@ theorem countRestricted_two (n : ℕ) : countRestricted n 2 = distincts n := by
 def oddDistincts (n : ℕ) : Finset n.Partition :=
   odds n ∩ distincts n
 
+end Partition
+
+/-! ### Conversion between Young diagrams -/
+
+private lemma youngDiagram_rowLens_sum_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card := by
+  have hf : ∀ c ∈ μ.cells, c.fst ∈ Finset.range (μ.colLen 0) := by
+    intro c hc
+    rw [Finset.mem_range, ← YoungDiagram.mem_iff_lt_colLen]
+    exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
+  have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.fst = i}).card = μ.rowLen i := by
+    intro i _hi
+    rw [YoungDiagram.rowLen_eq_card]
+    rfl
+  rw [YoungDiagram.card, Finset.card_eq_sum_card_fiberwise hf, Finset.sum_congr rfl hr,
+    YoungDiagram.rowLens, ← List.sum_toFinset, List.toFinset_range]
+  exact List.nodup_range
+
+namespace Partition
+
 /-- Convert a Young diagram to a partition. -/
-def ofYoungDiagram (μ : YoungDiagram) : Partition (μ.card) where
+def ofYoungDiagram {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Partition n where
   parts := μ.rowLens
   parts_pos := μ.pos_of_mem_rowLens _
   parts_sum := by
-    have hf : ∀ c ∈ μ.cells, c.fst ∈ Finset.range (μ.colLen 0) := by
-      intro c hc
-      rw [Finset.mem_range, ← YoungDiagram.mem_iff_lt_colLen]
-      exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
-    have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.fst = i}).card = μ.rowLen i := by
-      intro i _hi
-      rw [YoungDiagram.rowLen_eq_card]
-      rfl
     simp only [sum_coe]
-    rw [YoungDiagram.card, Finset.card_eq_sum_card_fiberwise hf, Finset.sum_congr rfl hr,
-      YoungDiagram.rowLens, ← List.sum_toFinset, List.toFinset_range]
-    exact List.nodup_range
+    rw [youngDiagram_rowLens_sum_eq_card]
+    exact h
 
 /-- Convert a partition to a Young diagram. -/
-def toYoungDiagram (p : Partition n) : YoungDiagram :=
+def toYoungDiagram {n : ℕ} (p : Partition n) : YoungDiagram :=
   YoungDiagram.ofRowLens
     (p.parts.sort (· ≥ ·))
     (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
 
+theorem youngDiagram_rowLens_eq_sorted_parts {n : ℕ} (p : Partition n) :
+    p.toYoungDiagram.rowLens = (p.parts.sort (· ≥ ·)) := by
+  rw [Partition.toYoungDiagram, YoungDiagram.rowLens_ofRowLens_eq_self]
+  simp only [ge_iff_le, mem_sort]
+  intro x
+  exact p.parts_pos
+
+theorem youngDiagram_rowLens_eq_parts {n : ℕ} (p : Partition n) :
+    ↑p.toYoungDiagram.rowLens = p.parts := by
+  rw [youngDiagram_rowLens_eq_sorted_parts, Multiset.sort_eq]
+
+theorem youngDiagram_card_eq_parts_sum {n : ℕ} (p : Partition n) :
+    p.toYoungDiagram.card = n := by
+  rw [← youngDiagram_rowLens_sum_eq_card, youngDiagram_rowLens_eq_sorted_parts]
+  calc (p.parts.sort (· ≥ ·)).sum
+        = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
+      _ = p.parts.sum := by rw [Multiset.sort_eq]
+      _ = n := p.parts_sum
+
+theorem ofYoungDiagram_toYoungDiagram_eq_self {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
+    (ofYoungDiagram μ h).toYoungDiagram = μ := by
+  rw [ofYoungDiagram, toYoungDiagram]
+  simp only
+  conv =>
+    lhs
+    congr
+    rw [Multiset.coe_sort]
+    exact List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise
+  exact YoungDiagram.ofRowLens_to_rowLens_eq_self
+
+theorem toYoungDiagram_ofYoungDiagram_eq_self {n : ℕ} (p : Partition n) :
+    ofYoungDiagram p.toYoungDiagram (youngDiagram_card_eq_parts_sum p) = p := by
+  rw [ofYoungDiagram]
+  apply Nat.Partition.ext
+  simp only
+  rw [youngDiagram_rowLens_eq_parts]
+
+/-- Equivalence between partitions and Young diagrams of appropriate size. -/
+def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram // μ.card = n } where
+  toFun p := ⟨p.toYoungDiagram, youngDiagram_card_eq_parts_sum p⟩
+  invFun μ := ofYoungDiagram μ μ.2
+  left_inv := toYoungDiagram_ofYoungDiagram_eq_self
+  right_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofYoungDiagram_toYoungDiagram_eq_self h)
+
+/-- Conjugate a partition (equivalent to transposing its Young diagram). -/
+def conjugate {n : ℕ} (p : Partition n) : Partition n :=
+  Partition.ofYoungDiagram p.toYoungDiagram.transpose (by
+    have hs : p.toYoungDiagram.transpose.card = p.toYoungDiagram.card := by
+      simp [YoungDiagram.transpose, YoungDiagram.card]
+    rw [hs, youngDiagram_card_eq_parts_sum]
+  )
+
+/-- Conjugation is an involution. -/
+@[simp]
+theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
+  apply Nat.Partition.ext
+  change (↑(p.conjugate.toYoungDiagram.transpose.rowLens) : Multiset ℕ) = p.parts
+  rw [conjugate, ofYoungDiagram_toYoungDiagram_eq_self, YoungDiagram.transpose_transpose,
+    youngDiagram_rowLens_eq_parts]
+
 end Partition
 
 end Nat

From a19cde8de5d83b56724902913277fc8193e5d8e4 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Fri, 22 May 2026 01:38:46 -0500
Subject: [PATCH 03/21] Prefer implicit binder

---
 Mathlib/Combinatorics/Enumerative/Partition/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index d992c4357b7065..ea77af5d8b862c 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -290,7 +290,7 @@ theorem ofYoungDiagram_toYoungDiagram_eq_self {n : ℕ} {μ : YoungDiagram} (h :
     exact List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise
   exact YoungDiagram.ofRowLens_to_rowLens_eq_self
 
-theorem toYoungDiagram_ofYoungDiagram_eq_self {n : ℕ} (p : Partition n) :
+theorem toYoungDiagram_ofYoungDiagram_eq_self {n : ℕ} {p : Partition n} :
     ofYoungDiagram p.toYoungDiagram (youngDiagram_card_eq_parts_sum p) = p := by
   rw [ofYoungDiagram]
   apply Nat.Partition.ext
@@ -301,7 +301,7 @@ theorem toYoungDiagram_ofYoungDiagram_eq_self {n : ℕ} (p : Partition n) :
 def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram // μ.card = n } where
   toFun p := ⟨p.toYoungDiagram, youngDiagram_card_eq_parts_sum p⟩
   invFun μ := ofYoungDiagram μ μ.2
-  left_inv := toYoungDiagram_ofYoungDiagram_eq_self
+  left_inv := fun _ => toYoungDiagram_ofYoungDiagram_eq_self
   right_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofYoungDiagram_toYoungDiagram_eq_self h)
 
 /-- Conjugate a partition (equivalent to transposing its Young diagram). -/

From 9b69192e5662c4fb3eba5d78681382b564eb0574 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Fri, 22 May 2026 01:40:27 -0500
Subject: [PATCH 04/21] Namespace nits

---
 Mathlib/Combinatorics/Enumerative/Partition/Basic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index ea77af5d8b862c..e12dfc6bc5301d 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -262,7 +262,7 @@ def toYoungDiagram {n : ℕ} (p : Partition n) : YoungDiagram :=
 
 theorem youngDiagram_rowLens_eq_sorted_parts {n : ℕ} (p : Partition n) :
     p.toYoungDiagram.rowLens = (p.parts.sort (· ≥ ·)) := by
-  rw [Partition.toYoungDiagram, YoungDiagram.rowLens_ofRowLens_eq_self]
+  rw [toYoungDiagram, YoungDiagram.rowLens_ofRowLens_eq_self]
   simp only [ge_iff_le, mem_sort]
   intro x
   exact p.parts_pos
@@ -293,7 +293,7 @@ theorem ofYoungDiagram_toYoungDiagram_eq_self {n : ℕ} {μ : YoungDiagram} (h :
 theorem toYoungDiagram_ofYoungDiagram_eq_self {n : ℕ} {p : Partition n} :
     ofYoungDiagram p.toYoungDiagram (youngDiagram_card_eq_parts_sum p) = p := by
   rw [ofYoungDiagram]
-  apply Nat.Partition.ext
+  apply Partition.ext
   simp only
   rw [youngDiagram_rowLens_eq_parts]
 
@@ -306,7 +306,7 @@ def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram /
 
 /-- Conjugate a partition (equivalent to transposing its Young diagram). -/
 def conjugate {n : ℕ} (p : Partition n) : Partition n :=
-  Partition.ofYoungDiagram p.toYoungDiagram.transpose (by
+  ofYoungDiagram p.toYoungDiagram.transpose (by
     have hs : p.toYoungDiagram.transpose.card = p.toYoungDiagram.card := by
       simp [YoungDiagram.transpose, YoungDiagram.card]
     rw [hs, youngDiagram_card_eq_parts_sum]
@@ -315,7 +315,7 @@ def conjugate {n : ℕ} (p : Partition n) : Partition n :=
 /-- Conjugation is an involution. -/
 @[simp]
 theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
-  apply Nat.Partition.ext
+  apply Partition.ext
   change (↑(p.conjugate.toYoungDiagram.transpose.rowLens) : Multiset ℕ) = p.parts
   rw [conjugate, ofYoungDiagram_toYoungDiagram_eq_self, YoungDiagram.transpose_transpose,
     youngDiagram_rowLens_eq_parts]

From 1caea906923b34853dd6bf2c836e25a2c88d896f Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Fri, 22 May 2026 15:04:13 -0500
Subject: [PATCH 05/21] Nits

---
 .../Enumerative/Partition/Basic.lean              | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index e12dfc6bc5301d..4d6a0728a412c4 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -231,11 +231,11 @@ end Partition
 /-! ### Conversion between Young diagrams -/
 
 private lemma youngDiagram_rowLens_sum_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card := by
-  have hf : ∀ c ∈ μ.cells, c.fst ∈ Finset.range (μ.colLen 0) := by
+  have hf : ∀ c ∈ μ.cells, c.1 ∈ Finset.range (μ.colLen 0) := by
     intro c hc
     rw [Finset.mem_range, ← YoungDiagram.mem_iff_lt_colLen]
     exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
-  have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.fst = i}).card = μ.rowLen i := by
+  have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.1 = i}).card = μ.rowLen i := by
     intro i _hi
     rw [YoungDiagram.rowLen_eq_card]
     rfl
@@ -274,10 +274,11 @@ theorem youngDiagram_rowLens_eq_parts {n : ℕ} (p : Partition n) :
 theorem youngDiagram_card_eq_parts_sum {n : ℕ} (p : Partition n) :
     p.toYoungDiagram.card = n := by
   rw [← youngDiagram_rowLens_sum_eq_card, youngDiagram_rowLens_eq_sorted_parts]
-  calc (p.parts.sort (· ≥ ·)).sum
-        = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
-      _ = p.parts.sum := by rw [Multiset.sort_eq]
-      _ = n := p.parts_sum
+  calc
+    (p.parts.sort (· ≥ ·)).sum
+      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
+    _ = p.parts.sum := by rw [Multiset.sort_eq]
+    _ = n := p.parts_sum
 
 theorem ofYoungDiagram_toYoungDiagram_eq_self {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
     (ofYoungDiagram μ h).toYoungDiagram = μ := by
@@ -298,7 +299,7 @@ theorem toYoungDiagram_ofYoungDiagram_eq_self {n : ℕ} {p : Partition n} :
   rw [youngDiagram_rowLens_eq_parts]
 
 /-- Equivalence between partitions and Young diagrams of appropriate size. -/
-def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram // μ.card = n } where
+def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram | μ.card = n } where
   toFun p := ⟨p.toYoungDiagram, youngDiagram_card_eq_parts_sum p⟩
   invFun μ := ofYoungDiagram μ μ.2
   left_inv := fun _ => toYoungDiagram_ofYoungDiagram_eq_self

From e7b7763b70a459639c93173367cf1c7758cae439 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Fri, 22 May 2026 18:00:48 -0500
Subject: [PATCH 06/21] Fix names

---
 .../Enumerative/Partition/Basic.lean          | 30 +++++++++----------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index 4d6a0728a412c4..a2f1ec50a2a18a 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -260,27 +260,27 @@ def toYoungDiagram {n : ℕ} (p : Partition n) : YoungDiagram :=
     (p.parts.sort (· ≥ ·))
     (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
 
-theorem youngDiagram_rowLens_eq_sorted_parts {n : ℕ} (p : Partition n) :
+theorem rowLens_toYoungDiagram_eq_sort_parts {n : ℕ} (p : Partition n) :
     p.toYoungDiagram.rowLens = (p.parts.sort (· ≥ ·)) := by
   rw [toYoungDiagram, YoungDiagram.rowLens_ofRowLens_eq_self]
   simp only [ge_iff_le, mem_sort]
   intro x
   exact p.parts_pos
 
-theorem youngDiagram_rowLens_eq_parts {n : ℕ} (p : Partition n) :
+theorem rowLens_toYoungDiagram_eq_parts {n : ℕ} (p : Partition n) :
     ↑p.toYoungDiagram.rowLens = p.parts := by
-  rw [youngDiagram_rowLens_eq_sorted_parts, Multiset.sort_eq]
+  rw [rowLens_toYoungDiagram_eq_sort_parts, Multiset.sort_eq]
 
-theorem youngDiagram_card_eq_parts_sum {n : ℕ} (p : Partition n) :
+theorem card_toYoungDiagram {n : ℕ} (p : Partition n) :
     p.toYoungDiagram.card = n := by
-  rw [← youngDiagram_rowLens_sum_eq_card, youngDiagram_rowLens_eq_sorted_parts]
+  rw [← youngDiagram_rowLens_sum_eq_card, rowLens_toYoungDiagram_eq_sort_parts]
   calc
     (p.parts.sort (· ≥ ·)).sum
       = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
     _ = p.parts.sum := by rw [Multiset.sort_eq]
     _ = n := p.parts_sum
 
-theorem ofYoungDiagram_toYoungDiagram_eq_self {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
+theorem toYoungDiagram_ofYoungDiagram {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
     (ofYoungDiagram μ h).toYoungDiagram = μ := by
   rw [ofYoungDiagram, toYoungDiagram]
   simp only
@@ -291,26 +291,26 @@ theorem ofYoungDiagram_toYoungDiagram_eq_self {n : ℕ} {μ : YoungDiagram} (h :
     exact List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise
   exact YoungDiagram.ofRowLens_to_rowLens_eq_self
 
-theorem toYoungDiagram_ofYoungDiagram_eq_self {n : ℕ} {p : Partition n} :
-    ofYoungDiagram p.toYoungDiagram (youngDiagram_card_eq_parts_sum p) = p := by
+theorem ofYoungDiagram_toYoungDiagram {n : ℕ} {p : Partition n} :
+    ofYoungDiagram p.toYoungDiagram (card_toYoungDiagram p) = p := by
   rw [ofYoungDiagram]
   apply Partition.ext
   simp only
-  rw [youngDiagram_rowLens_eq_parts]
+  rw [rowLens_toYoungDiagram_eq_parts]
 
 /-- Equivalence between partitions and Young diagrams of appropriate size. -/
 def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram | μ.card = n } where
-  toFun p := ⟨p.toYoungDiagram, youngDiagram_card_eq_parts_sum p⟩
+  toFun p := ⟨p.toYoungDiagram, card_toYoungDiagram p⟩
   invFun μ := ofYoungDiagram μ μ.2
-  left_inv := fun _ => toYoungDiagram_ofYoungDiagram_eq_self
-  right_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofYoungDiagram_toYoungDiagram_eq_self h)
+  left_inv := fun _ => ofYoungDiagram_toYoungDiagram
+  right_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (toYoungDiagram_ofYoungDiagram h)
 
 /-- Conjugate a partition (equivalent to transposing its Young diagram). -/
 def conjugate {n : ℕ} (p : Partition n) : Partition n :=
   ofYoungDiagram p.toYoungDiagram.transpose (by
     have hs : p.toYoungDiagram.transpose.card = p.toYoungDiagram.card := by
       simp [YoungDiagram.transpose, YoungDiagram.card]
-    rw [hs, youngDiagram_card_eq_parts_sum]
+    rw [hs, card_toYoungDiagram]
   )
 
 /-- Conjugation is an involution. -/
@@ -318,8 +318,8 @@ def conjugate {n : ℕ} (p : Partition n) : Partition n :=
 theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
   apply Partition.ext
   change (↑(p.conjugate.toYoungDiagram.transpose.rowLens) : Multiset ℕ) = p.parts
-  rw [conjugate, ofYoungDiagram_toYoungDiagram_eq_self, YoungDiagram.transpose_transpose,
-    youngDiagram_rowLens_eq_parts]
+  rw [conjugate, toYoungDiagram_ofYoungDiagram, YoungDiagram.transpose_transpose,
+    rowLens_toYoungDiagram_eq_parts]
 
 end Partition
 

From 2afbc1058efee801bb7c707f308025541a59822a Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Fri, 22 May 2026 18:13:25 -0500
Subject: [PATCH 07/21] Move Young diagram lemma

---
 .../Enumerative/Partition/Basic.lean          | 21 ++-----------------
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 15 +++++++++++++
 2 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index a2f1ec50a2a18a..f64f7e4c25cada 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -226,32 +226,15 @@ theorem countRestricted_two (n : ℕ) : countRestricted n 2 = distincts n := by
 def oddDistincts (n : ℕ) : Finset n.Partition :=
   odds n ∩ distincts n
 
-end Partition
-
 /-! ### Conversion between Young diagrams -/
 
-private lemma youngDiagram_rowLens_sum_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card := by
-  have hf : ∀ c ∈ μ.cells, c.1 ∈ Finset.range (μ.colLen 0) := by
-    intro c hc
-    rw [Finset.mem_range, ← YoungDiagram.mem_iff_lt_colLen]
-    exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
-  have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.1 = i}).card = μ.rowLen i := by
-    intro i _hi
-    rw [YoungDiagram.rowLen_eq_card]
-    rfl
-  rw [YoungDiagram.card, Finset.card_eq_sum_card_fiberwise hf, Finset.sum_congr rfl hr,
-    YoungDiagram.rowLens, ← List.sum_toFinset, List.toFinset_range]
-  exact List.nodup_range
-
-namespace Partition
-
 /-- Convert a Young diagram to a partition. -/
 def ofYoungDiagram {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Partition n where
   parts := μ.rowLens
   parts_pos := μ.pos_of_mem_rowLens _
   parts_sum := by
     simp only [sum_coe]
-    rw [youngDiagram_rowLens_sum_eq_card]
+    rw [YoungDiagram.sum_rowLens_eq_card]
     exact h
 
 /-- Convert a partition to a Young diagram. -/
@@ -273,7 +256,7 @@ theorem rowLens_toYoungDiagram_eq_parts {n : ℕ} (p : Partition n) :
 
 theorem card_toYoungDiagram {n : ℕ} (p : Partition n) :
     p.toYoungDiagram.card = n := by
-  rw [← youngDiagram_rowLens_sum_eq_card, rowLens_toYoungDiagram_eq_sort_parts]
+  rw [← YoungDiagram.sum_rowLens_eq_card, rowLens_toYoungDiagram_eq_sort_parts]
   calc
     (p.parts.sort (· ≥ ·)).sum
       = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 05f06844c2d4eb..05d33e98055c56 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -5,9 +5,11 @@ Authors: Jake Levinson
 -/
 module
 
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Data.Finset.Preimage
 public import Mathlib.Data.Finset.Prod
 public import Mathlib.Data.SetLike.Basic
+public import Mathlib.Order.Interval.Finset.Nat
 public import Mathlib.Order.UpperLower.Basic
 
 /-!
@@ -379,6 +381,19 @@ theorem pos_of_mem_rowLens (μ : YoungDiagram) (x : ℕ) (hx : x ∈ μ.rowLens)
   obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx
   rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi
 
+lemma sum_rowLens_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card := by
+  have hf : ∀ c ∈ μ.cells, c.1 ∈ Finset.range (μ.colLen 0) := by
+    intro c hc
+    rw [Finset.mem_range, ← YoungDiagram.mem_iff_lt_colLen]
+    exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
+  have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.1 = i}).card = μ.rowLen i := by
+    intro i _hi
+    rw [YoungDiagram.rowLen_eq_card]
+    rfl
+  rw [YoungDiagram.card, Finset.card_eq_sum_card_fiberwise hf, Finset.sum_congr rfl hr,
+    YoungDiagram.rowLens, ← List.sum_toFinset, List.toFinset_range]
+  exact List.nodup_range
+
 end RowLens
 
 section EquivListRowLens

From a54c616106aa13f7310cc82ce2066ce3ba1bf344 Mon Sep 17 00:00:00 2001
From: KG <41345727+kg583@users.noreply.github.com>
Date: Fri, 22 May 2026 22:25:47 -0500
Subject: [PATCH 08/21] Golfs

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
Co-authored-by: Noah Walker <noahwalker3.14@gmail.com>
---
 .../Enumerative/Partition/Basic.lean          | 38 +++++++------------
 Mathlib/Combinatorics/Young/YoungDiagram.lean |  3 +-
 2 files changed, 14 insertions(+), 27 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index f64f7e4c25cada..a64ad4afdcbf5e 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -232,10 +232,7 @@ def oddDistincts (n : ℕ) : Finset n.Partition :=
 def ofYoungDiagram {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Partition n where
   parts := μ.rowLens
   parts_pos := μ.pos_of_mem_rowLens _
-  parts_sum := by
-    simp only [sum_coe]
-    rw [YoungDiagram.sum_rowLens_eq_card]
-    exact h
+  parts_sum := by simp [YoungDiagram.sum_rowLens_eq_card, h]
 
 /-- Convert a partition to a Young diagram. -/
 def toYoungDiagram {n : ℕ} (p : Partition n) : YoungDiagram :=
@@ -244,16 +241,15 @@ def toYoungDiagram {n : ℕ} (p : Partition n) : YoungDiagram :=
     (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
 
 theorem rowLens_toYoungDiagram_eq_sort_parts {n : ℕ} (p : Partition n) :
-    p.toYoungDiagram.rowLens = (p.parts.sort (· ≥ ·)) := by
-  rw [toYoungDiagram, YoungDiagram.rowLens_ofRowLens_eq_self]
-  simp only [ge_iff_le, mem_sort]
-  intro x
-  exact p.parts_pos
+    p.toYoungDiagram.rowLens = p.parts.sort (· ≥ ·) := by
+  grind [toYoungDiagram, YoungDiagram.rowLens_ofRowLens_eq_self, mem_sort]
 
+@[simp]
 theorem rowLens_toYoungDiagram_eq_parts {n : ℕ} (p : Partition n) :
     ↑p.toYoungDiagram.rowLens = p.parts := by
   rw [rowLens_toYoungDiagram_eq_sort_parts, Multiset.sort_eq]
 
+@[simp]
 theorem card_toYoungDiagram {n : ℕ} (p : Partition n) :
     p.toYoungDiagram.card = n := by
   rw [← YoungDiagram.sum_rowLens_eq_card, rowLens_toYoungDiagram_eq_sort_parts]
@@ -263,23 +259,17 @@ theorem card_toYoungDiagram {n : ℕ} (p : Partition n) :
     _ = p.parts.sum := by rw [Multiset.sort_eq]
     _ = n := p.parts_sum
 
+@[simp]
 theorem toYoungDiagram_ofYoungDiagram {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
     (ofYoungDiagram μ h).toYoungDiagram = μ := by
-  rw [ofYoungDiagram, toYoungDiagram]
-  simp only
-  conv =>
-    lhs
-    congr
-    rw [Multiset.coe_sort]
-    exact List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise
-  exact YoungDiagram.ofRowLens_to_rowLens_eq_self
+  simp [toYoungDiagram, ofYoungDiagram, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise, 
+    YoungDiagram.ofRowLens_to_rowLens_eq_self]
 
+@[simp]
 theorem ofYoungDiagram_toYoungDiagram {n : ℕ} {p : Partition n} :
     ofYoungDiagram p.toYoungDiagram (card_toYoungDiagram p) = p := by
-  rw [ofYoungDiagram]
-  apply Partition.ext
-  simp only
-  rw [rowLens_toYoungDiagram_eq_parts]
+  ext 
+  simp [ofYoungDiagram]
 
 /-- Equivalence between partitions and Young diagrams of appropriate size. -/
 def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram | μ.card = n } where
@@ -299,10 +289,8 @@ def conjugate {n : ℕ} (p : Partition n) : Partition n :=
 /-- Conjugation is an involution. -/
 @[simp]
 theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
-  apply Partition.ext
-  change (↑(p.conjugate.toYoungDiagram.transpose.rowLens) : Multiset ℕ) = p.parts
-  rw [conjugate, toYoungDiagram_ofYoungDiagram, YoungDiagram.transpose_transpose,
-    rowLens_toYoungDiagram_eq_parts]
+  ext
+  simp [conjugate]
 
 end Partition
 
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 05d33e98055c56..d84eb80d2c5ad6 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -388,8 +388,7 @@ lemma sum_rowLens_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card := by
     exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
   have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.1 = i}).card = μ.rowLen i := by
     intro i _hi
-    rw [YoungDiagram.rowLen_eq_card]
-    rfl
+    rw [YoungDiagram.rowLen_eq_card, row]
   rw [YoungDiagram.card, Finset.card_eq_sum_card_fiberwise hf, Finset.sum_congr rfl hr,
     YoungDiagram.rowLens, ← List.sum_toFinset, List.toFinset_range]
   exact List.nodup_range

From fe6087dedf7bb71f08eea488fb84a8c73856182d Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Sat, 23 May 2026 03:26:31 +0000
Subject: [PATCH 09/21] [pre-commit.ci lite] apply automatic fixes

---
 Mathlib/Combinatorics/Enumerative/Partition/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index a64ad4afdcbf5e..a6a5ab10aa959c 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -262,13 +262,13 @@ theorem card_toYoungDiagram {n : ℕ} (p : Partition n) :
 @[simp]
 theorem toYoungDiagram_ofYoungDiagram {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
     (ofYoungDiagram μ h).toYoungDiagram = μ := by
-  simp [toYoungDiagram, ofYoungDiagram, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise, 
+  simp [toYoungDiagram, ofYoungDiagram, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise,
     YoungDiagram.ofRowLens_to_rowLens_eq_self]
 
 @[simp]
 theorem ofYoungDiagram_toYoungDiagram {n : ℕ} {p : Partition n} :
     ofYoungDiagram p.toYoungDiagram (card_toYoungDiagram p) = p := by
-  ext 
+  ext
   simp [ofYoungDiagram]
 
 /-- Equivalence between partitions and Young diagrams of appropriate size. -/

From c18208705d6237f24a947b32d0728eb290bf2acc Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Fri, 22 May 2026 22:44:32 -0500
Subject: [PATCH 10/21] Extract out `transpose_card_eq_card`

---
 Mathlib/Combinatorics/Enumerative/Partition/Basic.lean | 4 +---
 Mathlib/Combinatorics/Young/YoungDiagram.lean          | 3 +++
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index a6a5ab10aa959c..f108efab5525d3 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -281,9 +281,7 @@ def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram |
 /-- Conjugate a partition (equivalent to transposing its Young diagram). -/
 def conjugate {n : ℕ} (p : Partition n) : Partition n :=
   ofYoungDiagram p.toYoungDiagram.transpose (by
-    have hs : p.toYoungDiagram.transpose.card = p.toYoungDiagram.card := by
-      simp [YoungDiagram.transpose, YoungDiagram.card]
-    rw [hs, card_toYoungDiagram]
+    rw [YoungDiagram.transpose_card_eq_card, card_toYoungDiagram]
   )
 
 /-- Conjugation is an involution. -/
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index d84eb80d2c5ad6..c1687a10347ef9 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -236,6 +236,9 @@ protected theorem transpose_mono {μ ν : YoungDiagram} (h_le : μ ≤ ν) : μ.
 def transposeOrderIso : YoungDiagram ≃o YoungDiagram :=
   ⟨⟨transpose, transpose, fun _ => by simp, fun _ => by simp⟩, by simp⟩
 
+lemma transpose_card_eq_card (μ : YoungDiagram) : μ.transpose.card = μ.card := by
+  simp [transpose, YoungDiagram.card]
+
 end Transpose
 
 section Rows

From d182b964041d834c2037fd545f6cc51457cf2946 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Sat, 23 May 2026 14:12:55 -0500
Subject: [PATCH 11/21] Move equivalence and split out `Conjugate`

---
 .../Enumerative/Partition/Basic.lean          | 65 -----------------
 .../Enumerative/Partition/Conjugate.lean      | 41 +++++++++++
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 69 ++++++++++++++++++-
 3 files changed, 108 insertions(+), 67 deletions(-)
 create mode 100644 Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
index f108efab5525d3..204768d1ce5877 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Algebra.Order.Antidiag.Finsupp
 public import Mathlib.Combinatorics.Enumerative.Composition
-public import Mathlib.Combinatorics.Young.YoungDiagram
 public import Mathlib.Tactic.ApplyFun
 
 /-!
@@ -226,70 +225,6 @@ theorem countRestricted_two (n : ℕ) : countRestricted n 2 = distincts n := by
 def oddDistincts (n : ℕ) : Finset n.Partition :=
   odds n ∩ distincts n
 
-/-! ### Conversion between Young diagrams -/
-
-/-- Convert a Young diagram to a partition. -/
-def ofYoungDiagram {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Partition n where
-  parts := μ.rowLens
-  parts_pos := μ.pos_of_mem_rowLens _
-  parts_sum := by simp [YoungDiagram.sum_rowLens_eq_card, h]
-
-/-- Convert a partition to a Young diagram. -/
-def toYoungDiagram {n : ℕ} (p : Partition n) : YoungDiagram :=
-  YoungDiagram.ofRowLens
-    (p.parts.sort (· ≥ ·))
-    (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
-
-theorem rowLens_toYoungDiagram_eq_sort_parts {n : ℕ} (p : Partition n) :
-    p.toYoungDiagram.rowLens = p.parts.sort (· ≥ ·) := by
-  grind [toYoungDiagram, YoungDiagram.rowLens_ofRowLens_eq_self, mem_sort]
-
-@[simp]
-theorem rowLens_toYoungDiagram_eq_parts {n : ℕ} (p : Partition n) :
-    ↑p.toYoungDiagram.rowLens = p.parts := by
-  rw [rowLens_toYoungDiagram_eq_sort_parts, Multiset.sort_eq]
-
-@[simp]
-theorem card_toYoungDiagram {n : ℕ} (p : Partition n) :
-    p.toYoungDiagram.card = n := by
-  rw [← YoungDiagram.sum_rowLens_eq_card, rowLens_toYoungDiagram_eq_sort_parts]
-  calc
-    (p.parts.sort (· ≥ ·)).sum
-      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
-    _ = p.parts.sum := by rw [Multiset.sort_eq]
-    _ = n := p.parts_sum
-
-@[simp]
-theorem toYoungDiagram_ofYoungDiagram {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
-    (ofYoungDiagram μ h).toYoungDiagram = μ := by
-  simp [toYoungDiagram, ofYoungDiagram, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise,
-    YoungDiagram.ofRowLens_to_rowLens_eq_self]
-
-@[simp]
-theorem ofYoungDiagram_toYoungDiagram {n : ℕ} {p : Partition n} :
-    ofYoungDiagram p.toYoungDiagram (card_toYoungDiagram p) = p := by
-  ext
-  simp [ofYoungDiagram]
-
-/-- Equivalence between partitions and Young diagrams of appropriate size. -/
-def equivPartitionYoungDiagram {n : ℕ} : Partition n ≃ { μ : YoungDiagram | μ.card = n } where
-  toFun p := ⟨p.toYoungDiagram, card_toYoungDiagram p⟩
-  invFun μ := ofYoungDiagram μ μ.2
-  left_inv := fun _ => ofYoungDiagram_toYoungDiagram
-  right_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (toYoungDiagram_ofYoungDiagram h)
-
-/-- Conjugate a partition (equivalent to transposing its Young diagram). -/
-def conjugate {n : ℕ} (p : Partition n) : Partition n :=
-  ofYoungDiagram p.toYoungDiagram.transpose (by
-    rw [YoungDiagram.transpose_card_eq_card, card_toYoungDiagram]
-  )
-
-/-- Conjugation is an involution. -/
-@[simp]
-theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
-  ext
-  simp [conjugate]
-
 end Partition
 
 end Nat
diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean b/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
new file mode 100644
index 00000000000000..ed65f513d2ddb6
--- /dev/null
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Kevin Gomez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Gomez
+-/
+module
+
+public import Mathlib.Combinatorics.Young.YoungDiagram
+
+/-!
+# Conjugate of a partition
+
+Given the Young diagram `μ` representing a partition `λ`, its conjugate `λ'` is the partition
+obtained by flipping `μ` about the main diagonal, i.e. the columns of `μ` are the parts of `λ'`.
+This is implemented here directly via `YoungDiagram.transpose`.
+
+See `YoungDiagram.ofPartition` and `YoungDiagram.toPartition` for direct manipulation of diagrams
+arising from partitions.
+-/
+
+@[expose] public section
+
+namespace Nat.Partition
+
+/-- Conjugate a partition (equivalent to transposing its Young diagram). -/
+def conjugate {n : ℕ} (p : Partition n) : Partition n :=
+  (YoungDiagram.ofPartition p).transpose.toPartition (by
+    rw [YoungDiagram.transpose_card_eq_card, YoungDiagram.card_ofPartition]
+  )
+
+/-- Conjugation is an involution. -/
+@[simp]
+theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
+  ext
+  simp [conjugate]
+
+/-- The finset of those partitions which are their own conjugate. -/
+def selfConjugate (n : ℕ) : Finset n.Partition :=
+  Finset.univ.filter fun p => p = p.conjugate
+
+end Nat.Partition
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index c1687a10347ef9..cea9eec6e7cc07 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -5,11 +5,10 @@ Authors: Jake Levinson
 -/
 module
 
-public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Combinatorics.Enumerative.Partition.Basic
 public import Mathlib.Data.Finset.Preimage
 public import Mathlib.Data.Finset.Prod
 public import Mathlib.Data.SetLike.Basic
-public import Mathlib.Order.Interval.Finset.Nat
 public import Mathlib.Order.UpperLower.Basic
 
 /-!
@@ -481,4 +480,70 @@ def equivListRowLens : YoungDiagram ≃ { w : List ℕ // w.SortedGE ∧ ∀ x 
 
 end EquivListRowLens
 
+section EquivPartition
+
+/-! ### Equivalence between Young diagrams and partitions
+
+This section defines the equivalence between Young diagrams `μ` with cardinality `n` and
+partitions of `n`, where each row of the diagram becomes a part of the partition:
+  `YoungDiagram.equivPartition :`
+  `{ μ : YoungDiagram | μ.card = n } ≃ Partition n`
+
+The two directions are `YoungDiagram.toPartition` and `YoungDiagram.ofPartition`.
+
+-/
+
+
+/-- Convert a Young diagram to a partition. -/
+def toPartition {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Nat.Partition n where
+  parts := μ.rowLens
+  parts_pos := μ.pos_of_mem_rowLens _
+  parts_sum := by simp [sum_rowLens_eq_card, h]
+
+/-- Convert a partition to a Young diagram. -/
+def ofPartition {n : ℕ} (p : Nat.Partition n) : YoungDiagram :=
+  ofRowLens
+    (p.parts.sort (· ≥ ·))
+    (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
+
+theorem rowLens_ofPartition_eq_sort_parts {n : ℕ} (p : Nat.Partition n) :
+    (ofPartition p).rowLens = p.parts.sort (· ≥ ·) := by
+  grind [ofPartition, rowLens_ofRowLens_eq_self, Multiset.mem_sort]
+
+@[simp]
+theorem rowLens_ofPartition_eq_parts {n : ℕ} (p : Nat.Partition n) :
+    ↑(ofPartition p).rowLens = p.parts := by
+  rw [rowLens_ofPartition_eq_sort_parts, Multiset.sort_eq]
+
+@[simp]
+theorem card_ofPartition {n : ℕ} (p : Nat.Partition n) :
+    (ofPartition p).card = n := by
+  rw [← sum_rowLens_eq_card, rowLens_ofPartition_eq_sort_parts]
+  calc
+    (p.parts.sort (· ≥ ·)).sum
+      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
+    _ = p.parts.sum := by rw [Multiset.sort_eq]
+    _ = n := p.parts_sum
+
+@[simp]
+theorem ofPartition_toPartition {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
+    ofPartition (μ.toPartition h) = μ := by
+  simp [ofPartition, toPartition, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise,
+    ofRowLens_to_rowLens_eq_self]
+
+@[simp]
+theorem toPartition_ofPartition {n : ℕ} {p : Nat.Partition n} :
+    (ofPartition p).toPartition (card_ofPartition p) = p := by
+  ext
+  simp [toPartition]
+
+/-- Equivalence between Young diagrams of cardinality `n` and partitions of `n`. -/
+def equivPartition {n : ℕ} : { μ : YoungDiagram | μ.card = n } ≃ Nat.Partition n where
+  toFun μ := toPartition μ μ.2
+  invFun p := ⟨ofPartition p, card_ofPartition p⟩
+  left_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofPartition_toPartition h)
+  right_inv := fun _ => toPartition_ofPartition
+
+end EquivPartition
+
 end YoungDiagram

From 39058444a06a6332f2a744c6331d208eac8e70c2 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Sat, 23 May 2026 14:39:51 -0500
Subject: [PATCH 12/21] Additional `@[simp]`s

---
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index cea9eec6e7cc07..c27f320e8ffd3c 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -235,6 +235,7 @@ protected theorem transpose_mono {μ ν : YoungDiagram} (h_le : μ ≤ ν) : μ.
 def transposeOrderIso : YoungDiagram ≃o YoungDiagram :=
   ⟨⟨transpose, transpose, fun _ => by simp, fun _ => by simp⟩, by simp⟩
 
+@[simp]
 lemma transpose_card_eq_card (μ : YoungDiagram) : μ.transpose.card = μ.card := by
   simp [transpose, YoungDiagram.card]
 
@@ -383,6 +384,7 @@ theorem pos_of_mem_rowLens (μ : YoungDiagram) (x : ℕ) (hx : x ∈ μ.rowLens)
   obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx
   rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi
 
+@[simp]
 lemma sum_rowLens_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card := by
   have hf : ∀ c ∈ μ.cells, c.1 ∈ Finset.range (μ.colLen 0) := by
     intro c hc

From b1a5d074314836e51fb826b21f3cd8a20c4262bc Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Sat, 23 May 2026 14:40:05 -0500
Subject: [PATCH 13/21] Add `Conjugate` to Mathlib

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index d211bbdb619507..51b0df1e3848a5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3516,6 +3516,7 @@ public import Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
 public import Mathlib.Combinatorics.Enumerative.InclusionExclusion
 public import Mathlib.Combinatorics.Enumerative.Partition
 public import Mathlib.Combinatorics.Enumerative.Partition.Basic
+public import Mathlib.Combinatorics.Enumerative.Partition.Conjugate
 public import Mathlib.Combinatorics.Enumerative.Partition.GenFun
 public import Mathlib.Combinatorics.Enumerative.Partition.Glaisher
 public import Mathlib.Combinatorics.Enumerative.Pentagonal

From 15d77a846db5bd59ad99b4fd7050842ac2766770 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Sat, 23 May 2026 23:10:47 -0500
Subject: [PATCH 14/21] Remove `selfConjugate` def (for now)

---
 Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean b/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
index ed65f513d2ddb6..70a1eb2b64bd2b 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
@@ -34,8 +34,4 @@ theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate
   ext
   simp [conjugate]
 
-/-- The finset of those partitions which are their own conjugate. -/
-def selfConjugate (n : ℕ) : Finset n.Partition :=
-  Finset.univ.filter fun p => p = p.conjugate
-
 end Nat.Partition

From a7c43217330d6449d9b061772696cc4d4d1eb17d Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Sat, 23 May 2026 23:14:02 -0500
Subject: [PATCH 15/21] Rename to `card_transpose`

---
 Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean | 2 +-
 Mathlib/Combinatorics/Young/YoungDiagram.lean              | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean b/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
index 70a1eb2b64bd2b..41b37c0b0f22c8 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
@@ -25,7 +25,7 @@ namespace Nat.Partition
 /-- Conjugate a partition (equivalent to transposing its Young diagram). -/
 def conjugate {n : ℕ} (p : Partition n) : Partition n :=
   (YoungDiagram.ofPartition p).transpose.toPartition (by
-    rw [YoungDiagram.transpose_card_eq_card, YoungDiagram.card_ofPartition]
+    rw [YoungDiagram.card_transpose, YoungDiagram.card_ofPartition]
   )
 
 /-- Conjugation is an involution. -/
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index c27f320e8ffd3c..8af609160670f1 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -236,7 +236,7 @@ def transposeOrderIso : YoungDiagram ≃o YoungDiagram :=
   ⟨⟨transpose, transpose, fun _ => by simp, fun _ => by simp⟩, by simp⟩
 
 @[simp]
-lemma transpose_card_eq_card (μ : YoungDiagram) : μ.transpose.card = μ.card := by
+lemma card_transpose (μ : YoungDiagram) : μ.transpose.card = μ.card := by
   simp [transpose, YoungDiagram.card]
 
 end Transpose

From 1fc2b96af62a73dc91b2dedf99f71c32c4b56d4c Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Sun, 24 May 2026 14:15:12 -0500
Subject: [PATCH 16/21] Redundant docstring

---
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 8af609160670f1..e2d88d626a9f87 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -487,9 +487,7 @@ section EquivPartition
 /-! ### Equivalence between Young diagrams and partitions
 
 This section defines the equivalence between Young diagrams `μ` with cardinality `n` and
-partitions of `n`, where each row of the diagram becomes a part of the partition:
-  `YoungDiagram.equivPartition :`
-  `{ μ : YoungDiagram | μ.card = n } ≃ Partition n`
+partitions of `n`, where each row of the diagram becomes a part of the partition.
 
 The two directions are `YoungDiagram.toPartition` and `YoungDiagram.ofPartition`.
 

From 3d512d89b0dbab68072ac7ac6f7dc8e90b17c300 Mon Sep 17 00:00:00 2001
From: KG <41345727+kg583@users.noreply.github.com>
Date: Sun, 24 May 2026 15:01:00 -0500
Subject: [PATCH 17/21] Use direct subtype

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
---
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index e2d88d626a9f87..449e9d25ff9ab2 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -538,7 +538,7 @@ theorem toPartition_ofPartition {n : ℕ} {p : Nat.Partition n} :
   simp [toPartition]
 
 /-- Equivalence between Young diagrams of cardinality `n` and partitions of `n`. -/
-def equivPartition {n : ℕ} : { μ : YoungDiagram | μ.card = n } ≃ Nat.Partition n where
+def equivPartition {n : ℕ} : { μ : YoungDiagram // μ.card = n } ≃ Nat.Partition n where
   toFun μ := toPartition μ μ.2
   invFun p := ⟨ofPartition p, card_ofPartition p⟩
   left_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofPartition_toPartition h)

From 8affb65058421377be3081888678ff0f04399471 Mon Sep 17 00:00:00 2001
From: KG <41345727+kg583@users.noreply.github.com>
Date: Fri, 26 Jun 2026 12:19:51 -0500
Subject: [PATCH 18/21] Whitespace lint
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
---
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 449e9d25ff9ab2..437d66548b6817 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -490,10 +490,8 @@ This section defines the equivalence between Young diagrams `μ` with cardinalit
 partitions of `n`, where each row of the diagram becomes a part of the partition.
 
 The two directions are `YoungDiagram.toPartition` and `YoungDiagram.ofPartition`.
-
 -/
 
-
 /-- Convert a Young diagram to a partition. -/
 def toPartition {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Nat.Partition n where
   parts := μ.rowLens

From a9e05b3c270074ee39e368a2096c786cc7a28238 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Wed, 1 Jul 2026 17:25:57 -0500
Subject: [PATCH 19/21] Add `@[simp]`

---
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 43274608e5567a..7abdaa18afd660 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -504,6 +504,7 @@ def ofPartition {n : ℕ} (p : Nat.Partition n) : YoungDiagram :=
     (p.parts.sort (· ≥ ·))
     (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
 
+@[simp]
 theorem rowLens_ofPartition_eq_sort_parts {n : ℕ} (p : Nat.Partition n) :
     (ofPartition p).rowLens = p.parts.sort (· ≥ ·) := by
   grind [ofPartition, rowLens_ofRowLens_eq_self, Multiset.mem_sort]

From 3bb7bcccb45d266821c4471724fb1cd4769ba1ec Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Wed, 1 Jul 2026 17:36:55 -0500
Subject: [PATCH 20/21] Remove `rowLens_ofPartition_eq_parts`

---
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 7abdaa18afd660..8e97afbc608fad 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -509,11 +509,6 @@ theorem rowLens_ofPartition_eq_sort_parts {n : ℕ} (p : Nat.Partition n) :
     (ofPartition p).rowLens = p.parts.sort (· ≥ ·) := by
   grind [ofPartition, rowLens_ofRowLens_eq_self, Multiset.mem_sort]
 
-@[simp]
-theorem rowLens_ofPartition_eq_parts {n : ℕ} (p : Nat.Partition n) :
-    ↑(ofPartition p).rowLens = p.parts := by
-  rw [rowLens_ofPartition_eq_sort_parts, Multiset.sort_eq]
-
 @[simp]
 theorem card_ofPartition {n : ℕ} (p : Nat.Partition n) :
     (ofPartition p).card = n := by

From 8f7e4fe3b727f5a568bfc6880e1395d3b60b6667 Mon Sep 17 00:00:00 2001
From: KG <kgscience@hotmail.com>
Date: Wed, 1 Jul 2026 19:27:28 -0500
Subject: [PATCH 21/21] Move Young diagram definitions

---
 Mathlib.lean                                  |  2 +-
 .../Enumerative/Partition/Conjugate.lean      | 37 --------
 .../Enumerative/Partition/YoungDiagram.lean   | 91 +++++++++++++++++++
 Mathlib/Combinatorics/Young/YoungDiagram.lean | 61 +------------
 4 files changed, 94 insertions(+), 97 deletions(-)
 delete mode 100644 Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
 create mode 100644 Mathlib/Combinatorics/Enumerative/Partition/YoungDiagram.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 8fa878ba4b734e..42a513cfe0d882 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3549,9 +3549,9 @@ public import Mathlib.Combinatorics.Enumerative.DyckWord
 public import Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
 public import Mathlib.Combinatorics.Enumerative.InclusionExclusion
 public import Mathlib.Combinatorics.Enumerative.Partition.Basic
-public import Mathlib.Combinatorics.Enumerative.Partition.Conjugate
 public import Mathlib.Combinatorics.Enumerative.Partition.GenFun
 public import Mathlib.Combinatorics.Enumerative.Partition.Glaisher
+public import Mathlib.Combinatorics.Enumerative.Partition.YoungDiagram
 public import Mathlib.Combinatorics.Enumerative.Pentagonal
 public import Mathlib.Combinatorics.Enumerative.Schroder
 public import Mathlib.Combinatorics.Enumerative.Stirling
diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean b/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
deleted file mode 100644
index 41b37c0b0f22c8..00000000000000
--- a/Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-/-
-Copyright (c) 2026 Kevin Gomez. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kevin Gomez
--/
-module
-
-public import Mathlib.Combinatorics.Young.YoungDiagram
-
-/-!
-# Conjugate of a partition
-
-Given the Young diagram `μ` representing a partition `λ`, its conjugate `λ'` is the partition
-obtained by flipping `μ` about the main diagonal, i.e. the columns of `μ` are the parts of `λ'`.
-This is implemented here directly via `YoungDiagram.transpose`.
-
-See `YoungDiagram.ofPartition` and `YoungDiagram.toPartition` for direct manipulation of diagrams
-arising from partitions.
--/
-
-@[expose] public section
-
-namespace Nat.Partition
-
-/-- Conjugate a partition (equivalent to transposing its Young diagram). -/
-def conjugate {n : ℕ} (p : Partition n) : Partition n :=
-  (YoungDiagram.ofPartition p).transpose.toPartition (by
-    rw [YoungDiagram.card_transpose, YoungDiagram.card_ofPartition]
-  )
-
-/-- Conjugation is an involution. -/
-@[simp]
-theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
-  ext
-  simp [conjugate]
-
-end Nat.Partition
diff --git a/Mathlib/Combinatorics/Enumerative/Partition/YoungDiagram.lean b/Mathlib/Combinatorics/Enumerative/Partition/YoungDiagram.lean
new file mode 100644
index 00000000000000..66642de0bba792
--- /dev/null
+++ b/Mathlib/Combinatorics/Enumerative/Partition/YoungDiagram.lean
@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2026 Kevin Gomez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Gomez
+-/
+module
+
+public import Mathlib.Combinatorics.Enumerative.Partition.Basic
+public import Mathlib.Combinatorics.Young.YoungDiagram
+
+/-!
+# Young diagram of a partition
+
+This file defines the equivalence between Young diagrams `μ` with cardinality `n` and
+partitions of `n`, where each row of the diagram becomes a part of the partition.
+The two directions are `YoungDiagram.toPartition` and `YoungDiagram.ofPartition`.
+
+Using this equivalence, the conjugate of a partition is also defined. Given the Young
+diagram `μ` representing a partition `λ`, its conjugate `λ'` is the partition obtained
+by flipping `μ` about the main diagonal, i.e. the columns of `μ` are the parts of `λ'`.
+This is implemented here directly via `YoungDiagram.transpose`.
+
+-/
+
+@[expose] public section
+
+namespace YoungDiagram
+
+/-- Convert a Young diagram to a partition. -/
+def toPartition {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Nat.Partition n where
+  parts := μ.rowLens
+  parts_pos := μ.pos_of_mem_rowLens _
+  parts_sum := by simp [sum_rowLens_eq_card, h]
+
+/-- Convert a partition to a Young diagram. -/
+def ofPartition {n : ℕ} (p : Nat.Partition n) : YoungDiagram :=
+  ofRowLens
+    (p.parts.sort (· ≥ ·))
+    (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
+
+@[simp]
+theorem rowLens_ofPartition_eq_sort_parts {n : ℕ} (p : Nat.Partition n) :
+    (ofPartition p).rowLens = p.parts.sort (· ≥ ·) := by
+  grind [ofPartition, rowLens_ofRowLens_eq_self, Multiset.mem_sort]
+
+@[simp]
+theorem card_ofPartition {n : ℕ} (p : Nat.Partition n) :
+    (ofPartition p).card = n := by
+  rw [← sum_rowLens_eq_card, rowLens_ofPartition_eq_sort_parts]
+  calc
+    (p.parts.sort (· ≥ ·)).sum
+      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
+    _ = p.parts.sum := by rw [Multiset.sort_eq]
+    _ = n := p.parts_sum
+
+@[simp]
+theorem ofPartition_toPartition {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
+    ofPartition (μ.toPartition h) = μ := by
+  simp [ofPartition, toPartition, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise,
+    ofRowLens_to_rowLens_eq_self]
+
+@[simp]
+theorem toPartition_ofPartition {n : ℕ} {p : Nat.Partition n} :
+    (ofPartition p).toPartition (card_ofPartition p) = p := by
+  ext
+  simp [toPartition]
+
+/-- Equivalence between Young diagrams of cardinality `n` and partitions of `n`. -/
+def equivPartition {n : ℕ} : { μ : YoungDiagram // μ.card = n } ≃ Nat.Partition n where
+  toFun μ := toPartition μ μ.2
+  invFun p := ⟨ofPartition p, card_ofPartition p⟩
+  left_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofPartition_toPartition h)
+  right_inv := fun _ => toPartition_ofPartition
+
+end YoungDiagram
+
+namespace Nat.Partition
+
+/-- Conjugate a partition (equivalent to transposing its Young diagram). -/
+def conjugate {n : ℕ} (p : Partition n) : Partition n :=
+  (YoungDiagram.ofPartition p).transpose.toPartition (by
+    rw [YoungDiagram.card_transpose, YoungDiagram.card_ofPartition]
+  )
+
+/-- Conjugation is an involution. -/
+@[simp]
+theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
+  ext
+  simp [conjugate]
+
+end Nat.Partition
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 8e97afbc608fad..d10e02861c9842 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -5,11 +5,12 @@ Authors: Jake Levinson
 -/
 module
 
-public import Mathlib.Combinatorics.Enumerative.Partition.Basic
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Data.Finset.Preimage
 public import Mathlib.Data.Finset.Prod
 public import Mathlib.Data.SetLike.Basic
 public import Mathlib.Order.UpperLower.Basic
+public import Mathlib.Order.Interval.Finset.Nat
 
 /-!
 # Young diagrams
@@ -482,62 +483,4 @@ def equivListRowLens : YoungDiagram ≃ { w : List ℕ // w.SortedGE ∧ ∀ x 
 
 end EquivListRowLens
 
-section EquivPartition
-
-/-! ### Equivalence between Young diagrams and partitions
-
-This section defines the equivalence between Young diagrams `μ` with cardinality `n` and
-partitions of `n`, where each row of the diagram becomes a part of the partition.
-
-The two directions are `YoungDiagram.toPartition` and `YoungDiagram.ofPartition`.
--/
-
-/-- Convert a Young diagram to a partition. -/
-def toPartition {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Nat.Partition n where
-  parts := μ.rowLens
-  parts_pos := μ.pos_of_mem_rowLens _
-  parts_sum := by simp [sum_rowLens_eq_card, h]
-
-/-- Convert a partition to a Young diagram. -/
-def ofPartition {n : ℕ} (p : Nat.Partition n) : YoungDiagram :=
-  ofRowLens
-    (p.parts.sort (· ≥ ·))
-    (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
-
-@[simp]
-theorem rowLens_ofPartition_eq_sort_parts {n : ℕ} (p : Nat.Partition n) :
-    (ofPartition p).rowLens = p.parts.sort (· ≥ ·) := by
-  grind [ofPartition, rowLens_ofRowLens_eq_self, Multiset.mem_sort]
-
-@[simp]
-theorem card_ofPartition {n : ℕ} (p : Nat.Partition n) :
-    (ofPartition p).card = n := by
-  rw [← sum_rowLens_eq_card, rowLens_ofPartition_eq_sort_parts]
-  calc
-    (p.parts.sort (· ≥ ·)).sum
-      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
-    _ = p.parts.sum := by rw [Multiset.sort_eq]
-    _ = n := p.parts_sum
-
-@[simp]
-theorem ofPartition_toPartition {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
-    ofPartition (μ.toPartition h) = μ := by
-  simp [ofPartition, toPartition, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise,
-    ofRowLens_to_rowLens_eq_self]
-
-@[simp]
-theorem toPartition_ofPartition {n : ℕ} {p : Nat.Partition n} :
-    (ofPartition p).toPartition (card_ofPartition p) = p := by
-  ext
-  simp [toPartition]
-
-/-- Equivalence between Young diagrams of cardinality `n` and partitions of `n`. -/
-def equivPartition {n : ℕ} : { μ : YoungDiagram // μ.card = n } ≃ Nat.Partition n where
-  toFun μ := toPartition μ μ.2
-  invFun p := ⟨ofPartition p, card_ofPartition p⟩
-  left_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofPartition_toPartition h)
-  right_inv := fun _ => toPartition_ofPartition
-
-end EquivPartition
-
 end YoungDiagram