From 4adcb48f561bb09dc6409f1f78a907947b4dce05 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 4 Nov 2024 20:10:29 +1100
Subject: [PATCH 01/18] bump toolchain

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 0bef727630..55b868d72c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:nightly-2024-11-04

From a65a608a98f1176b607352b9ae12fb817ec53cdc Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 4 Nov 2024 20:12:39 +1100
Subject: [PATCH 02/18] remove upstreamed

---
 Batteries/Data/Array/OfFn.lean |   4 --
 Batteries/Data/Fin/Basic.lean  |  54 --------------
 Batteries/Data/Fin/Lemmas.lean | 128 ---------------------------------
 Batteries/Data/List/Basic.lean |   8 ---
 Batteries/Data/List/OfFn.lean  |  34 ---------
 5 files changed, 228 deletions(-)

diff --git a/Batteries/Data/Array/OfFn.lean b/Batteries/Data/Array/OfFn.lean
index e02be7cba1..5233fd1f96 100644
--- a/Batteries/Data/Array/OfFn.lean
+++ b/Batteries/Data/Array/OfFn.lean
@@ -11,8 +11,4 @@ namespace Array
 
 /-! ### ofFn -/
 
-@[simp]
-theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by
-  apply ext_getElem <;> simp
-
 end Array
diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean
index b61481e33a..346f3006e5 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -14,57 +14,3 @@ def enum (n) : Array (Fin n) := Array.ofFn id
 
 /-- `list n` is the list of all elements of `Fin n` in order -/
 def list (n) : List (Fin n) := (enum n).toList
-
-/--
-Folds a monadic function over `Fin n` from left to right:
-```
-Fin.foldlM n f x₀ = do
-  let x₁ ← f x₀ 0
-  let x₂ ← f x₁ 1
-  ...
-  let xₙ ← f xₙ₋₁ (n-1)
-  pure xₙ
-```
--/
-@[inline] def foldlM [Monad m] (n) (f : α → Fin n → m α) (init : α) : m α := loop init 0 where
-  /--
-  Inner loop for `Fin.foldlM`.
-  ```
-  Fin.foldlM.loop n f xᵢ i = do
-    let xᵢ₊₁ ← f xᵢ i
-    ...
-    let xₙ ← f xₙ₋₁ (n-1)
-    pure xₙ
-  ```
-  -/
-  loop (x : α) (i : Nat) : m α := do
-    if h : i < n then f x ⟨i, h⟩ >>= (loop · (i+1)) else pure x
-  termination_by n - i
-
-/--
-Folds a monadic function over `Fin n` from right to left:
-```
-Fin.foldrM n f xₙ = do
-  let xₙ₋₁ ← f (n-1) xₙ
-  let xₙ₋₂ ← f (n-2) xₙ₋₁
-  ...
-  let x₀ ← f 0 x₁
-  pure x₀
-```
--/
-@[inline] def foldrM [Monad m] (n) (f : Fin n → α → m α) (init : α) : m α :=
-  loop ⟨n, Nat.le_refl n⟩ init where
-  /--
-  Inner loop for `Fin.foldrM`.
-  ```
-  Fin.foldrM.loop n f i xᵢ = do
-    let xᵢ₋₁ ← f (i-1) xᵢ
-    ...
-    let x₁ ← f 1 x₂
-    let x₀ ← f 0 x₁
-    pure x₀
-  ```
-  -/
-  loop : {i // i ≤ n} → α → m α
-  | ⟨0, _⟩, x => pure x
-  | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩
diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean
index 5010e1310f..d799e2e6f3 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -56,32 +56,6 @@ theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
 
 /-! ### foldlM -/
 
-theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
-    foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by
-  rw [foldlM.loop, dif_pos h]
-
-theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x := by
-  rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)]
-
-theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) :
-    foldlM.loop (n+1) f x i = f x ⟨i, h⟩ >>= (foldlM.loop n (fun x j => f x j.succ) . i) := by
-  if h' : i < n then
-    rw [foldlM_loop_lt _ _ h]
-    congr; funext
-    rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl
-  else
-    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
-    rw [foldlM_loop_lt]
-    congr; funext
-    rw [foldlM_loop_eq, foldlM_loop_eq]
-termination_by n - i
-
-@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x :=
-  foldlM_loop_eq ..
-
-theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) :
-    foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
-
 theorem foldlM_eq_foldlM_list [Monad m] (f : α → Fin n → m α) (x) :
     foldlM n f x = (list n).foldlM f x := by
   induction n generalizing x with
@@ -93,32 +67,6 @@ theorem foldlM_eq_foldlM_list [Monad m] (f : α → Fin n → m α) (x) :
 
 /-! ### foldrM -/
 
-theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) :
-    foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by
-  rw [foldrM.loop]
-
-theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) :
-    foldrM.loop n f ⟨i+1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, Nat.le_of_lt h⟩ := by
-  rw [foldrM.loop]
-
-theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) :
-    foldrM.loop (n+1) f ⟨i+1, h⟩ x =
-      foldrM.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x >>= f 0 := by
-  induction i generalizing x with
-  | zero =>
-    rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
-    conv => rhs; rw [←bind_pure (f 0 x)]
-    congr; funext; exact foldrM_loop_zero ..
-  | succ i ih =>
-    rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
-    congr; funext; exact ih ..
-
-@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x :=
-  foldrM_loop_zero ..
-
-theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
-    foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
-
 theorem foldrM_eq_foldrM_list [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
     foldrM n f x = (list n).foldrM f x := by
   induction n with
@@ -127,41 +75,6 @@ theorem foldrM_eq_foldrM_list [Monad m] [LawfulMonad m] (f : Fin n → α → m
 
 /-! ### foldl -/
 
-theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) :
-    foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by
-  rw [foldl.loop, dif_pos h]
-
-theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by
-  rw [foldl.loop, dif_neg (Nat.lt_irrefl _)]
-
-theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : i < n+1) :
-    foldl.loop (n+1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i := by
-  if h' : i < n then
-    rw [foldl_loop_lt _ _ h]
-    rw [foldl_loop_lt _ _ h', foldl_loop]; rfl
-  else
-    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
-    rw [foldl_loop_lt]
-    rw [foldl_loop_eq, foldl_loop_eq]
-
-@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x :=
-  foldl_loop_eq ..
-
-theorem foldl_succ (f : α → Fin (n+1) → α) (x) :
-    foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) :=
-  foldl_loop ..
-
-theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
-    foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by
-  rw [foldl_succ]
-  induction n generalizing x with
-  | zero => simp [foldl_succ, Fin.last]
-  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
-
-theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
-    foldl n f x = foldlM (m:=Id) n f x := by
-  induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
-
 theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
   induction n generalizing x with
   | zero => rw [foldl_zero, list_zero, List.foldl_nil]
@@ -169,48 +82,7 @@ theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list
 
 /-! ### foldr -/
 
-theorem foldr_loop_zero (f : Fin n → α → α) (x) :
-    foldr.loop n f ⟨0, Nat.zero_le _⟩ x = x := by
-  rw [foldr.loop]
-
-theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) :
-    foldr.loop n f ⟨i+1, h⟩ x = foldr.loop n f ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x) := by
-  rw [foldr.loop]
-
-theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) :
-    foldr.loop (n+1) f ⟨i+1, h⟩ x =
-      f 0 (foldr.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x) := by
-  induction i generalizing x <;> simp [foldr_loop_zero, foldr_loop_succ, *]
-
-@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x :=
-  foldr_loop_zero ..
-
-theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
-    foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
-
-theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
-    foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
-  induction n generalizing x with
-  | zero => simp [foldr_succ, Fin.last]
-  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
-
-theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
-    foldr n f x = foldrM (m:=Id) n f x := by
-  induction n <;> simp [foldr_succ, foldrM_succ, *]
-
 theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
   induction n with
   | zero => rw [foldr_zero, list_zero, List.foldr_nil]
   | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]
-
-theorem foldl_rev (f : Fin n → α → α) (x) :
-    foldl n (fun x i => f i.rev x) x = foldr n f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ]
-
-theorem foldr_rev (f : α → Fin n → α) (x) :
-     foldr n (fun i x => f x i.rev) x = foldl n f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 3e2460f18c..da8e21f3b8 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -548,14 +548,6 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
   rw [Array.foldl_toList_eq_flatMap]; rfl
   intros; apply Array.foldl_toList_eq_map
 
-/--
-`ofFn f` with `f : fin n → α` returns the list whose ith element is `f i`
-```
-ofFn f = [f 0, f 1, ... , f (n - 1)]
-```
--/
-def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []
-
 /-- `ofFnNthVal f i` returns `some (f i)` if `i < n` and `none` otherwise. -/
 def ofFnNthVal {n} (f : Fin n → α) (i : Nat) : Option α :=
   if h : i < n then some (f ⟨i, h⟩) else none
diff --git a/Batteries/Data/List/OfFn.lean b/Batteries/Data/List/OfFn.lean
index 93214cc99b..c66846e61a 100644
--- a/Batteries/Data/List/OfFn.lean
+++ b/Batteries/Data/List/OfFn.lean
@@ -12,38 +12,4 @@ import Batteries.Data.Fin.Lemmas
 
 namespace List
 
-@[simp]
-theorem length_ofFn (f : Fin n → α) : (ofFn f).length = n := by
-  simp only [ofFn]
-  induction n with
-  | zero => simp
-  | succ n ih => simp [Fin.foldr_succ, ih]
-
-@[simp]
-protected theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length) :
-    (ofFn f)[i] = f ⟨i, by simp_all⟩ := by
-  simp only [ofFn]
-  induction n generalizing i with
-  | zero => simp at h
-  | succ n ih =>
-    match i with
-    | 0 => simp [Fin.foldr_succ]
-    | i+1 =>
-      simp only [Fin.foldr_succ]
-      apply ih
-      simp_all
-
-@[simp]
-protected theorem getElem?_ofFn (f : Fin n → α) (i) : (ofFn f)[i]? = ofFnNthVal f i :=
-  if h : i < (ofFn f).length
-  then by
-    rw [getElem?_eq_getElem h, List.getElem_ofFn]
-    · simp only [length_ofFn] at h; simp [ofFnNthVal, h]
-  else by
-    rw [ofFnNthVal, dif_neg] <;>
-    simpa using h
-
-@[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
-  ext <;> simp
-
 end List

From d9e997fb60f8d4fcbf03270fbb696f7c87ee0e25 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Thu, 7 Nov 2024 09:15:48 +0000
Subject: [PATCH 03/18] Update lean-toolchain for testing
 https://github.com/leanprover/lean4/pull/5988

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 55b868d72c..6609c78fc7 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-04
+leanprover/lean4-pr-releases:pr-release-5988

From a7da4bae0da191e827ca63fd55671c8cde548d8b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 8 Nov 2024 07:59:32 +1100
Subject: [PATCH 04/18] bump toolchain and remove upstreamed

---
 Batteries/Data/Array/Lemmas.lean  | 48 -------------------------------
 Batteries/Data/List/Basic.lean    | 24 ----------------
 Batteries/Data/String/Lemmas.lean |  2 +-
 lean-toolchain                    |  2 +-
 4 files changed, 2 insertions(+), 74 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 8a5544089d..daf0493b88 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -22,48 +22,6 @@ theorem forIn_eq_forIn_toList [Monad m]
 
 /-! ### zipWith / zip -/
 
-theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
-    (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by
-  let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
-      (zipWithAux f as bs i cs).toList =
-        cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
-    intro i cs hia hib
-    unfold zipWithAux
-    by_cases h : i = as.size ∨ i = bs.size
-    case pos =>
-      have : ¬(i < as.size) ∨ ¬(i < bs.size) := by
-        cases h <;> simp_all only [Nat.not_lt, Nat.le_refl, true_or, or_true]
-      -- Cleaned up aesop output below
-      simp_all only [Nat.not_lt]
-      cases h <;> [(cases this); (cases this)]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_left, List.append_nil]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_left, List.append_nil]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_right, List.append_nil]
-        split <;> simp_all only [Nat.not_lt]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_right, List.append_nil]
-        split <;> simp_all only [Nat.not_lt]
-    case neg =>
-      rw [not_or] at h
-      have has : i < as.size := Nat.lt_of_le_of_ne hia h.1
-      have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2
-      simp only [has, hbs, dite_true]
-      rw [loop (i+1) _ has hbs, Array.push_toList]
-      have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl
-      let i_as : Fin as.toList.length := ⟨i, has⟩
-      let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
-      rw [h₁, List.append_assoc]
-      congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_getElem_toList,
-        getElem_eq_getElem_toList]
-      show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
-        ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
-        List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
-      simp only [length_toList, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
-  simp [zipWith, loop 0 #[] (by simp) (by simp)]
 @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
@@ -71,12 +29,6 @@ theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
     (as.zipWith bs f).size = min as.size bs.size := by
   rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
 
-theorem toList_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).toList = as.toList.zip bs.toList :=
-  toList_zipWith Prod.mk as bs
-@[deprecated (since := "2024-09-09")] alias data_zip := toList_zip
-@[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
-
 @[simp] theorem size_zip (as : Array α) (bs : Array β) :
     (as.zip bs).size = min as.size bs.size :=
   as.size_zipWith bs Prod.mk
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index da8e21f3b8..77adfc783b 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -163,32 +163,8 @@ Split a list at every occurrence of a separator element. The separators are not
   | [x], acc => acc.toListAppend [f x]
   | x :: xs, acc => go xs (acc.push x)
 
-/--
-`insertIdx n a l` inserts `a` into the list `l` after the first `n` elements of `l`
-```
-insertIdx 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
-```
--/
-def insertIdx (n : Nat) (a : α) : List α → List α :=
-  modifyTailIdx (cons a) n
-
 @[deprecated (since := "2024-10-21")] alias insertNth := insertIdx
 
-/-- Tail-recursive version of `insertIdx`. -/
-@[inline] def insertIdxTR (n : Nat) (a : α) (l : List α) : List α := go n l #[] where
-  /-- Auxiliary for `insertIdxTR`: `insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l`. -/
-  go : Nat → List α → Array α → List α
-  | 0, l, acc => acc.toListAppend (a :: l)
-  | _, [], acc => acc.toList
-  | n+1, a :: l, acc => go n l (acc.push a)
-
-theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l
-  | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx]
-  | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l]
-
-@[csimp] theorem insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR := by
-  funext α f n l; simp [insertIdxTR, insertIdxTR_go_eq]
-
 theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a := by cases l <;> rfl
 
 /--
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
index 5854890f25..749d4cfd7f 100644
--- a/Batteries/Data/String/Lemmas.lean
+++ b/Batteries/Data/String/Lemmas.lean
@@ -573,7 +573,7 @@ theorem extract (h₁ : ValidFor l (m ++ r) it₁) (h₂ : ValidFor (m.reverse +
     it₁.extract it₂ = ⟨m⟩ := by
   cases h₁.out; cases h₂.out
   simp only [Iterator.extract, List.reverseAux_eq, List.reverse_append, List.reverse_reverse,
-    List.append_assoc, ne_eq, not_true_eq_false, decide_False, utf8Len_append, utf8Len_reverse,
+    List.append_assoc, ne_eq, not_true_eq_false, decide_false, utf8Len_append, utf8Len_reverse,
     gt_iff_lt, pos_lt_eq, Nat.not_lt.2 (Nat.le_add_left ..), Bool.or_self, Bool.false_eq_true,
     ↓reduceIte]
   simpa [Nat.add_comm] using extract_of_valid l.reverse m r
diff --git a/lean-toolchain b/lean-toolchain
index 55b868d72c..305b342999 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-04
+leanprover/lean4:nightly-2024-11-07

From cd5fdf289d2b4a4804469853cc4445582ac4a331 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Fri, 8 Nov 2024 09:05:44 +0000
Subject: [PATCH 05/18] chore: bump to nightly-2024-11-08

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 305b342999..600020f1fa 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-07
+leanprover/lean4:nightly-2024-11-08

From 774ecca30ee46932f8d5f7178c59a69ade38609f Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sun, 10 Nov 2024 09:05:17 +0000
Subject: [PATCH 06/18] chore: bump to nightly-2024-11-10

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 600020f1fa..57168baca4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-08
+leanprover/lean4:nightly-2024-11-10

From 4fbc598626f02cae3d60708c04a09c311bb60369 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 11:55:21 +1100
Subject: [PATCH 07/18] fixes for leanprover/lean4#5988

---
 Batteries/Data/Array/Basic.lean     |  2 +-
 Batteries/Data/BinaryHeap.lean      |  8 ++++----
 Batteries/Data/ByteArray.lean       |  2 +-
 Batteries/Data/HashMap/Basic.lean   |  2 +-
 Batteries/Data/UnionFind/Basic.lean | 14 +++++++-------
 5 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 403c42d9e2..0ef6af9830 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -135,7 +135,7 @@ A proof by `get_elem_tactic` is provided as a default argument for `h`.
 This will perform the update destructively provided that `a` has a reference count of 1 when called.
 -/
 abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
-  a.set ⟨i, h⟩ x
+  a.set i x
 
 /--
 `swapN a i j hi hj` swaps two `Nat` indexed entries in an `Array α`.
diff --git a/Batteries/Data/BinaryHeap.lean b/Batteries/Data/BinaryHeap.lean
index b36ed97fd3..65f66e0f6e 100644
--- a/Batteries/Data/BinaryHeap.lean
+++ b/Batteries/Data/BinaryHeap.lean
@@ -135,7 +135,7 @@ def insertExtractMax (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt
   | none => (x, self)
   | some m =>
     if lt x m then
-      let a := self.1.set ⟨0, size_pos_of_max e⟩ x
+      let a := self.1.set 0 x (size_pos_of_max e)
       (m, ⟨heapifyDown lt a ⟨0, by simp only [Array.size_set, a]; exact size_pos_of_max e⟩⟩)
     else (x, self)
 
@@ -144,16 +144,16 @@ def replaceMax (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α l
   match e: self.max with
   | none => (none, ⟨self.1.push x⟩)
   | some m =>
-    let a := self.1.set ⟨0, size_pos_of_max e⟩ x
+    let a := self.1.set 0 x (size_pos_of_max e)
     (some m, ⟨heapifyDown lt a ⟨0, by simp only [Array.size_set, a]; exact size_pos_of_max e⟩⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/
 def decreaseKey (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
-  arr := heapifyDown lt (self.1.set i x) ⟨i, by rw [self.1.size_set]; exact i.2⟩
+  arr := heapifyDown lt (self.1.set i x i.isLt) ⟨i, by rw [self.1.size_set]; exact i.2⟩
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `self.get i ≤ x`. -/
 def increaseKey (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
-  arr := heapifyUp lt (self.1.set i x) ⟨i, by rw [self.1.size_set]; exact i.2⟩
+  arr := heapifyUp lt (self.1.set i x i.isLt) ⟨i, by rw [self.1.size_set]; exact i.2⟩
 
 end Batteries.BinaryHeap
 
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
index 6a95a241aa..fe2b750a08 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -45,7 +45,7 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
 /-! ### set -/
 
 @[simp] theorem data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
-    (a.set i v).data = a.data.set i v := rfl
+    (a.set i v).data = a.data.set i v i.isLt := rfl
 @[deprecated (since := "2024-08-13")] alias set_data := data_set
 
 @[simp] theorem size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
index 3fd1d3350d..3a1827faff 100644
--- a/Batteries/Data/HashMap/Basic.lean
+++ b/Batteries/Data/HashMap/Basic.lean
@@ -40,7 +40,7 @@ Note: this is marked `noncomputable` because it is only intended for specificati
 noncomputable def size (data : Buckets α β) : Nat := (data.1.toList.map (·.toList.length)).sum
 
 @[simp] theorem update_size (self : Buckets α β) (i d h) :
-    (self.update i d h).1.size = self.1.size := Array.size_uset ..
+    (self.update i d h).1.size = self.1.size := Array.size_uset _ _ _ h
 
 /-- Map a function over the values in the map. -/
 @[specialize] def mapVal (f : α → β → γ) (self : Buckets α β) : Buckets α γ :=
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index c48bb5bda1..75cace976d 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -45,19 +45,19 @@ theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·)
 theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size :=
   Decidable.not_imp_comm.1 parentD_of_not_lt
 
-theorem parentD_set {arr : Array UFNode} {x v i} :
-    parentD (arr.set x v) i = if x.1 = i then v.parent else parentD arr i := by
+theorem parentD_set {arr : Array UFNode} {x v i h} :
+    parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
   rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD]
   split
   · split <;> simp_all
-  · split <;> [(subst i; cases ‹¬_› x.2); rfl]
+  · split <;> [(subst i; cases ‹¬_› h); rfl]
 
-theorem rankD_set {arr : Array UFNode} {x v i} :
-    rankD (arr.set x v) i = if x.1 = i then v.rank else rankD arr i := by
+theorem rankD_set {arr : Array UFNode} {x v i h} :
+    rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by
   rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD]
   split
   · split <;> simp_all
-  · split <;> [(subst i; cases ‹¬_› x.2); rfl]
+  · split <;> [(subst i; cases ‹¬_› h); rfl]
 
 end UnionFind
 
@@ -454,7 +454,7 @@ def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
     else
       let arr₁ := self.set x {nx with parent := y}
       if nx.rank = ny.rank then
-        arr₁.set ⟨y, by simp [arr₁]⟩ {ny with rank := ny.rank + 1}
+        arr₁.set y {ny with rank := ny.rank + 1} (by simp [arr₁])
       else
         arr₁
 

From 8dfd1e4aa6c513ea3653fe4a6e6b4d380e44bf67 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Mon, 11 Nov 2024 04:19:05 +0000
Subject: [PATCH 08/18] Trigger CI for
 https://github.com/leanprover/lean4/pull/5988


From db9926ee642a55b4a4b80f882b2f5b22a2fee152 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Mon, 11 Nov 2024 04:43:52 +0000
Subject: [PATCH 09/18] Trigger CI for
 https://github.com/leanprover/lean4/pull/5988


From 433429762eb5e9efb6420292b1a4be97b47cd75b Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Mon, 11 Nov 2024 09:05:57 +0000
Subject: [PATCH 10/18] chore: bump to nightly-2024-11-11

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 57168baca4..c60eb4fd2a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-10
+leanprover/lean4:nightly-2024-11-11

From 3cf3e5e7011b1796704e41f7c3404c703a91f4aa Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Tue, 12 Nov 2024 09:05:53 +0000
Subject: [PATCH 11/18] chore: bump to nightly-2024-11-12

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index c60eb4fd2a..9e0b2f2e74 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-11
+leanprover/lean4:nightly-2024-11-12

From 007f1b1322eed097d2bdeac5ea2417b37c8b7c12 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:40:14 +1100
Subject: [PATCH 12/18] fixes

---
 Batteries/Data/Array/Basic.lean   | 6 +++---
 Batteries/Data/Array/Merge.lean   | 2 +-
 Batteries/Data/ByteArray.lean     | 6 +++---
 Batteries/Data/HashMap/Basic.lean | 5 ++---
 4 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 0ef6af9830..8be0bc967d 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -46,7 +46,7 @@ considered.
 protected def minD [ord : Ord α]
     (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
   if h: start < xs.size ∧ start < stop then
-    xs.minWith (xs.get ⟨start, h.left⟩) (start + 1) stop
+    xs.minWith xs[start] (start + 1) stop
   else
     d
 
@@ -60,7 +60,7 @@ considered.
 protected def min? [ord : Ord α]
     (xs : Array α) (start := 0) (stop := xs.size) : Option α :=
   if h : start < xs.size ∧ start < stop then
-    some $ xs.minD (xs.get ⟨start, h.left⟩) start stop
+    some $ xs.minD xs[start] start stop
   else
     none
 
@@ -201,7 +201,7 @@ subarray, or `none` if the subarray is empty.
 def popHead? (as : Subarray α) : Option (α × Subarray α) :=
   if h : as.start < as.stop
     then
-      let head := as.array.get ⟨as.start, Nat.lt_of_lt_of_le h as.stop_le_array_size⟩
+      let head := as.array[as.start]'(Nat.lt_of_lt_of_le h as.stop_le_array_size)
       let tail :=
         { as with
           start := as.start + 1
diff --git a/Batteries/Data/Array/Merge.lean b/Batteries/Data/Array/Merge.lean
index 4b806a35d6..252f7a6364 100644
--- a/Batteries/Data/Array/Merge.lean
+++ b/Batteries/Data/Array/Merge.lean
@@ -94,7 +94,7 @@ set_option linter.unusedVariables.funArgs false in
 `f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ`.
 -/
 def mergeAdjacentDups [eq : BEq α] (f : α → α → α) (xs : Array α) : Array α :=
-  if h : 0 < xs.size then go (mkEmpty xs.size) 1 (xs.get ⟨0, h⟩) else xs
+  if h : 0 < xs.size then go (mkEmpty xs.size) 1 xs[0] else xs
 where
   /-- Auxiliary definition for `mergeAdjacentDups`. -/
   go (acc : Array α) (i : Nat) (hd : α) :=
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
index fe2b750a08..86a495e2df 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -15,7 +15,7 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 /-! ### uget/uset -/
 
 @[simp] theorem uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) :
-    a.uset i v h = a.set ⟨i.toNat, h⟩ v := rfl
+    a.uset i v h = a.set i.toNat v := rfl
 
 /-! ### empty -/
 
@@ -60,7 +60,7 @@ theorem get_set_ne (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size
   Array.get_set_ne (h:=h) ..
 
 theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
-    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' :=
+    (a.set i v).set i v' = a.set i v' :=
   ByteArray.ext <| Array.set_set ..
 
 /-! ### copySlice -/
@@ -132,7 +132,7 @@ def ofFn (f : Fin n → UInt8) : ByteArray where
   simp [get, Fin.cast]
 
 @[simp] theorem getElem_ofFn (f : Fin n → UInt8) (i) (h : i < (ofFn f).size) :
-    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn ..
+    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn f ⟨i, h⟩
 
 private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where
   go (i : Nat) (acc : ByteArray) : ByteArray :=
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
index 3a1827faff..a8a93dd197 100644
--- a/Batteries/Data/HashMap/Basic.lean
+++ b/Batteries/Data/HashMap/Basic.lean
@@ -143,11 +143,10 @@ where
   destroying `source` in the process. -/
   go (i : Nat) (source : Array (AssocList α β)) (target : Buckets α β) : Buckets α β :=
     if h : i < source.size then
-      let idx : Fin source.size := ⟨i, h⟩
-      let es := source.get idx
+      let es := source[i]
       -- We remove `es` from `source` to make sure we can reuse its memory cells
       -- when performing es.foldl
-      let source := source.set idx .nil
+      let source := source.set i .nil
       let target := es.foldl reinsertAux target
       go (i+1) source target
     else target

From 322fd4470d789f36dc31de7db16e66ffc96ddb61 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:49:33 +1100
Subject: [PATCH 13/18] comment out UnionFind so I can fix Mathlib

---
 Batteries/Data/Array/Pairwise.lean  |    2 +-
 Batteries/Data/UnionFind/Basic.lean | 1168 +++++++++++++--------------
 2 files changed, 585 insertions(+), 585 deletions(-)

diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
index 82ace9609f..498c070540 100644
--- a/Batteries/Data/Array/Pairwise.lean
+++ b/Batteries/Data/Array/Pairwise.lean
@@ -20,7 +20,7 @@ that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is
 def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
 theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
-    ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by
+    ∀ (i j : Fin as.size), i < j → R (as.get i i.2) (as.get j j.2) := by
   unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList]
 
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index 75cace976d..d2386f122c 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -1,590 +1,590 @@
-/-
-Copyright (c) 2021 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-import Batteries.Tactic.Alias
-import Batteries.Tactic.Lint.Misc
-import Batteries.Tactic.SeqFocus
-import Batteries.Util.Panic
-import Batteries.Data.Array.Lemmas
-
-@[deprecated (since := "2024-10-05")]
-protected alias Batteries.UnionFind.panicWith := Batteries.panicWith
-
-namespace Batteries
-
-/-- Union-find node type -/
-structure UFNode where
-  /-- Parent of node -/
-  parent : Nat
-  /-- Rank of node -/
-  rank : Nat
-
-namespace UnionFind
-
-/-- Parent of a union-find node, defaults to self when the node is a root -/
-def parentD (arr : Array UFNode) (i : Nat) : Nat :=
-  if h : i < arr.size then (arr.get ⟨i, h⟩).parent else i
-
-/-- Rank of a union-find node, defaults to 0 when the node is a root -/
-def rankD (arr : Array UFNode) (i : Nat) : Nat :=
-  if h : i < arr.size then (arr.get ⟨i, h⟩).rank else 0
-
-theorem parentD_eq {arr : Array UFNode} {i} : parentD arr i.1 = (arr.get i).parent := dif_pos _
+-- /-
+-- Copyright (c) 2021 Mario Carneiro. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Mario Carneiro
+-- -/
+-- import Batteries.Tactic.Alias
+-- import Batteries.Tactic.Lint.Misc
+-- import Batteries.Tactic.SeqFocus
+-- import Batteries.Util.Panic
+-- import Batteries.Data.Array.Lemmas
+
+-- @[deprecated (since := "2024-10-05")]
+-- protected alias Batteries.UnionFind.panicWith := Batteries.panicWith
+
+-- namespace Batteries
+
+-- /-- Union-find node type -/
+-- structure UFNode where
+--   /-- Parent of node -/
+--   parent : Nat
+--   /-- Rank of node -/
+--   rank : Nat
+
+-- namespace UnionFind
+
+-- /-- Parent of a union-find node, defaults to self when the node is a root -/
+-- def parentD (arr : Array UFNode) (i : Nat) : Nat :=
+--   if h : i < arr.size then arr[i].parent else i
+
+-- /-- Rank of a union-find node, defaults to 0 when the node is a root -/
+-- def rankD (arr : Array UFNode) (i : Nat) : Nat :=
+--   if h : i < arr.size then arr[i].rank else 0
+
+-- theorem parentD_eq {arr : Array UFNode} {i : Nat} {h} : parentD arr i = arr[i].parent := dif_pos _
 
-theorem parentD_eq' {arr : Array UFNode} {i} (h) :
-    parentD arr i = (arr.get ⟨i, h⟩).parent := dif_pos _
+-- theorem parentD_eq' {arr : Array UFNode} {i} (h) :
+--     parentD arr i = arr[i].parent := dif_pos _
 
-theorem rankD_eq {arr : Array UFNode} {i} : rankD arr i.1 = (arr.get i).rank := dif_pos _
-
-theorem rankD_eq' {arr : Array UFNode} {i} (h) : rankD arr i = (arr.get ⟨i, h⟩).rank := dif_pos _
+-- theorem rankD_eq {arr : Array UFNode} {i : Fin arr.size} : rankD arr i = arr[i].rank := dif_pos _
+
+-- theorem rankD_eq' {arr : Array UFNode} {i} (h) : rankD arr i = arr[i].rank := dif_pos _
 
-theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·)
-
-theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size :=
-  Decidable.not_imp_comm.1 parentD_of_not_lt
+-- theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·)
+
+-- theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size :=
+--   Decidable.not_imp_comm.1 parentD_of_not_lt
 
-theorem parentD_set {arr : Array UFNode} {x v i h} :
-    parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
-  rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD]
-  split
-  · split <;> simp_all
-  · split <;> [(subst i; cases ‹¬_› h); rfl]
-
-theorem rankD_set {arr : Array UFNode} {x v i h} :
-    rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by
-  rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD]
-  split
-  · split <;> simp_all
-  · split <;> [(subst i; cases ‹¬_› h); rfl]
-
-end UnionFind
+-- theorem parentD_set {arr : Array UFNode} {x v i h} :
+--     parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
+--   rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD]
+--   split
+--   · split <;> simp_all
+--   · split <;> [(subst i; cases ‹¬_› h); rfl]
+
+-- theorem rankD_set {arr : Array UFNode} {x v i h} :
+--     rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by
+--   rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD]
+--   split
+--   · split <;> simp_all
+--   · split <;> [(subst i; cases ‹¬_› h); rfl]
+
+-- end UnionFind
 
-open UnionFind
-
-/-- ### Union-find data structure
+-- open UnionFind
+
+-- /-- ### Union-find data structure
 
-The `UnionFind` structure is an implementation of disjoint-set data structure
-that uses path compression to make the primary operations run in amortized
-nearly linear time. The nodes of a `UnionFind` structure `s` are natural
-numbers smaller than `s.size`. The structure associates with a canonical
-representative from its equivalence class. The structure can be extended
-using the `push` operation and equivalence classes can be updated using the
-`union` operation.
-
-The main operations for `UnionFind` are:
-
-* `empty`/`mkEmpty` are used to create a new empty structure.
-* `size` returns the size of the data structure.
-* `push` adds a new node to a structure, unlinked to any other node.
-* `union` links two nodes of the data structure, joining their equivalence
-  classes, and performs path compression.
-* `find` returns the canonical representative of a node and updates the data
-  structure using path compression.
-* `root` returns the canonical representative of a node without altering the
-  data structure.
-* `checkEquiv` checks whether two nodes have the same canonical representative
-  and updates the structure using path compression.
-
-Most use cases should prefer `find` over `root` to benefit from the speedup from path-compression.
-
-The main operations use `Fin s.size` to represent nodes of the union-find structure.
-Some alternatives are provided:
-
-* `unionN`, `findN`, `rootN`, `checkEquivN` use `Fin n` with a proof that `n = s.size`.
-* `union!`, `find!`, `root!`, `checkEquiv!` use `Nat` and panic when the indices are out of bounds.
-* `findD`, `rootD`, `checkEquivD` use `Nat` and treat out of bound indices as isolated nodes.
-
-The noncomputable relation `UnionFind.Equiv` is provided to use the equivalence relation from a
-`UnionFind` structure in the context of proofs.
--/
-structure UnionFind where
-  /-- Array of union-find nodes -/
-  arr : Array UFNode
-  /-- Validity for parent nodes -/
-  parentD_lt : ∀ {i}, i < arr.size → parentD arr i < arr.size
-  /-- Validity for rank -/
-  rankD_lt : ∀ {i}, parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
-
-namespace UnionFind
-
-/-- Size of union-find structure. -/
-@[inline] abbrev size (self : UnionFind) := self.arr.size
-
-/-- Create an empty union-find structure with specific capacity -/
-def mkEmpty (c : Nat) : UnionFind where
-  arr := Array.mkEmpty c
-  parentD_lt := nofun
-  rankD_lt := nofun
-
-/-- Empty union-find structure -/
-def empty := mkEmpty 0
-
-instance : EmptyCollection UnionFind := ⟨.empty⟩
-
-/-- Parent of union-find node -/
-abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
-
-theorem parent'_lt (self : UnionFind) (i : Fin self.size) :
-    (self.arr.get i).parent < self.size := by
-  simp only [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList]
-
-theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by
-  simp only [parentD]; split <;> simp only [*, parent'_lt]
-
-/-- Rank of union-find node -/
-abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
-
-theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i →
-    self.rank i < self.rank (self.parent i) := by simpa only [rank] using self.rankD_lt
-
-theorem rank'_lt (self : UnionFind) (i : Fin self.size) : (self.arr.get i).parent ≠ i →
-    self.rank i < self.rank (self.arr.get i).parent := by
-  simpa only [← parentD_eq] using self.rankD_lt
-
-/-- Maximum rank of nodes in a union-find structure -/
-noncomputable def rankMax (self : UnionFind) := self.arr.foldr (max ·.rank) 0 + 1
-
-theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) :
-    (self.arr.get i).rank < self.rankMax := by
-  let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
-    | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
-    | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
-  simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList]
-  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2)
-
-theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
-    rankD self.arr i < self.rankMax := by
-  simp [rankD]; split <;> [apply rank'_lt_rankMax; apply Nat.succ_pos]
-
-theorem lt_rankMax (self : UnionFind) (i : Nat) : self.rank i < self.rankMax := rankD_lt_rankMax ..
-
-theorem push_rankD (arr : Array UFNode) : rankD (arr.push ⟨arr.size, 0⟩) i = rankD arr i := by
-  simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
-  split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
-
-theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩) i = parentD arr i := by
-  simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
-  split <;> split <;> try simp
-  · exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
-  · cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
-
-/-- Add a new node to a union-find structure, unlinked with any other nodes -/
-def push (self : UnionFind) : UnionFind where
-  arr := self.arr.push ⟨self.arr.size, 0⟩
-  parentD_lt {i} := by
-    simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem]
-    split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt _); exact id]
-  rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt
-
-/-- Root of a union-find node. -/
-def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
-  let y := (self.arr.get x).parent
-  if h : y = x then
-    x
-  else
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
-    self.root ⟨y, self.parent'_lt x⟩
-termination_by self.rankMax - self.rank x
-
-@[inherit_doc root]
-def rootN (self : UnionFind) (x : Fin n) (h : n = self.size) : Fin n :=
-  match n, h with | _, rfl => self.root x
-
-/-- Root of a union-find node. Panics if index is out of bounds. -/
-def root! (self : UnionFind) (x : Nat) : Nat :=
-  if h : x < self.size then self.root ⟨x, h⟩ else panicWith x "index out of bounds"
-
-/-- Root of a union-find node. Returns input if index is out of bounds. -/
-def rootD (self : UnionFind) (x : Nat) : Nat :=
-  if h : x < self.size then self.root ⟨x, h⟩ else x
-
-@[nolint unusedHavesSuffices]
-theorem parent_root (self : UnionFind) (x : Fin self.size) :
-    (self.arr.get (self.root x)).parent = self.root x := by
-  rw [root]; split <;> [assumption; skip]
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-  apply parent_root
-termination_by self.rankMax - self.rank x
-
-theorem parent_rootD (self : UnionFind) (x : Nat) :
-    self.parent (self.rootD x) = self.rootD x := by
-  rw [rootD]
-  split
-  · simp [parentD, parent_root, -Array.get_eq_getElem]
-  · simp [parentD_of_not_lt, *]
-
-@[nolint unusedHavesSuffices]
-theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
-  simp only [rootD, Array.length_toList, parent_lt]
-  split
-  · simp only [parentD, ↓reduceDIte, *]
-    (conv => rhs; rw [root]); split
-    · rw [root, dif_pos] <;> simp_all
-    · simp
-  · simp only [not_false_eq_true, parentD_of_not_lt, *]
-
-theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x < self.size := by
-  simp only [rootD, Array.length_toList]; split <;> simp [*]
-
-@[nolint unusedHavesSuffices]
-theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by
-  refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩
-  rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
-
-theorem rootD_rootD {self : UnionFind} {x : Nat} : self.rootD (self.rootD x) = self.rootD x :=
-  rootD_eq_self.2 (parent_rootD ..)
-
-theorem rootD_ext {m1 m2 : UnionFind}
-    (H : ∀ x, m1.parent x = m2.parent x) {x} : m1.rootD x = m2.rootD x := by
-  if h : m2.parent x = x then
-    rw [rootD_eq_self.2 h, rootD_eq_self.2 ((H _).trans h)]
-  else
-    have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
-    rw [← rootD_parent, H, rootD_ext H, rootD_parent]
-termination_by m2.rankMax - m2.rank x
-
-theorem le_rank_root {self : UnionFind} {x : Nat} : self.rank x ≤ self.rank (self.rootD x) := by
-  if h : self.parent x = x then
-    rw [rootD_eq_self.2 h]; exact Nat.le_refl ..
-  else
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
-    rw [← rootD_parent]
-    exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
-termination_by self.rankMax - self.rank x
-
-theorem lt_rank_root {self : UnionFind} {x : Nat} :
-    self.rank x < self.rank (self.rootD x) ↔ self.parent x ≠ x := by
-  refine ⟨fun h h' => Nat.ne_of_lt h (by rw [rootD_eq_self.2 h']), fun h => ?_⟩
-  rw [← rootD_parent]
-  exact Nat.lt_of_lt_of_le (self.rank_lt h) le_rank_root
-
-/-- Auxiliary data structure for find operation -/
-structure FindAux (n : Nat) where
-  /-- Array of nodes -/
-  s : Array UFNode
-  /-- Index of root node -/
-  root : Fin n
-  /-- Size requirement -/
-  size_eq : s.size = n
-
-/-- Auxiliary function for find operation -/
-def findAux (self : UnionFind) (x : Fin self.size) : FindAux self.size :=
-  let y := (self.arr.get x).parent
-  if h : y = x then
-    ⟨self.arr, x, rfl⟩
-  else
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
-    let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt x⟩
-    ⟨arr₁.modify x fun s => { s with parent := root }, root, by simp [H]⟩
-termination_by self.rankMax - self.rank x
-
-@[nolint unusedHavesSuffices]
-theorem findAux_root {self : UnionFind} {x : Fin self.size} :
-    (findAux self x).root = self.root x := by
-  rw [findAux, root]
-  simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]
-  split <;> simp only
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-  exact findAux_root
-termination_by self.rankMax - self.rank x
-
-@[nolint unusedHavesSuffices]
-theorem findAux_s {self : UnionFind} {x : Fin self.size} :
-    (findAux self x).s = if (self.arr.get x).parent = x then self.arr else
-      (self.findAux ⟨_, self.parent'_lt x⟩).s.modify x fun s =>
-        { s with parent := self.rootD x } := by
-  rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
-  · rw [findAux]; split <;> rfl
-  · rw [← rootD_parent, parent, parentD_eq]
-    simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]
-    apply dif_pos
-    exact parent'_lt ..
-
-set_option linter.deprecated false in
-theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
-    rankD (findAux self x).s i = self.rank i := by
-  if h : i < self.size then
-    rw [findAux_s]; split <;> [rfl; skip]
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-    have := lt_of_parentD (by rwa [parentD_eq])
-    rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify]
-    split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
-  else
-    simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
-    rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
-termination_by self.rankMax - self.rank x
-
-set_option linter.deprecated false in
-theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
-    parentD (findAux self x).s i =
-    if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt x⟩).s i := by
-  rw [findAux_s]; split <;> [split; skip]
-  · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]
-  · rw [findAux_s]; simp [*, -Array.get_eq_getElem]
-  · next h =>
-    rw [parentD]; split <;> rename_i h'
-    · rw [Array.get_modify (by simpa using h')]
-      simp only [Array.data_length, @eq_comm _ i]
-      split <;> simp [← parentD_eq, -Array.get_eq_getElem]
-    · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
-      rw [parentD, dif_neg]; simpa using h'
-
-theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} :
-    parentD (findAux self x).s (self.rootD x) = self.rootD x := by
-  rw [parentD_findAux]; split <;> [rfl; rename_i h]
-  rw [rootD_eq_self, parent, parentD_eq] at h
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-  rw [← rootD_parent, parent, parentD_eq]
-  exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt x⟩)
-termination_by self.rankMax - self.rank x
-
-theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) :
-    parentD (findAux self x).s i < self.size := by
-  if h' : (self.arr.get x).parent = x then
-    rw [findAux_s, if_pos h']; apply self.parentD_lt h
-  else
-    rw [parentD_findAux]
-    split
-    · simp [rootD_lt]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-      apply parentD_findAux_lt h
-termination_by self.rankMax - self.rank x
-
-theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
-    parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨
-    parentD (findAux self x).s i = self.parent i := by
-  if h' : (self.arr.get x).parent = x then
-    rw [findAux_s, if_pos h']; exact .inr rfl
-  else
-    rw [parentD_findAux]
-    split
-    · simp [*]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-      exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
-        simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
-termination_by self.rankMax - self.rank x
-
-theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
-    parentD (findAux self x).s i ≠ i →
-    self.rank i < self.rank (parentD (findAux self x).s i) := by
-  if h' : (self.arr.get x).parent = x then
-    rw [findAux_s, if_pos h']; apply self.rank_lt
-  else
-    rw [parentD_findAux]; split <;> rename_i h <;> intro h'
-    · subst i; rwa [lt_rank_root, Ne, ← rootD_eq_self]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-      apply lt_rankD_findAux h'
-termination_by self.rankMax - self.rank x
-
-/-- Find root of a union-find node, updating the structure using path compression. -/
-def find (self : UnionFind) (x : Fin self.size) :
-    (s : UnionFind) × {_root : Fin s.size // s.size = self.size} :=
-  let r := self.findAux x
-  { 1.arr := r.s
-    2.1.val := r.root
-    1.parentD_lt := fun h => by
-      simp only [Array.length_toList, FindAux.size_eq] at *
-      exact parentD_findAux_lt h
-    1.rankD_lt := fun h => by rw [rankD_findAux, rankD_findAux]; exact lt_rankD_findAux h
-    2.1.isLt := show _ < r.s.size by rw [r.size_eq]; exact r.root.2
-    2.2 := by simp [size, r.size_eq] }
-
-@[inherit_doc find]
-def findN (self : UnionFind) (x : Fin n) (h : n = self.size) : UnionFind × Fin n :=
-  match n, h with | _, rfl => match self.find x with | ⟨s, r, h⟩ => (s, Fin.cast h r)
-
-/-- Find root of a union-find node, updating the structure using path compression.
-  Panics if index is out of bounds. -/
-def find! (self : UnionFind) (x : Nat) : UnionFind × Nat :=
-  if h : x < self.size then
-    match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
-  else
-    panicWith (self, x) "index out of bounds"
-
-/-- Find root of a union-find node, updating the structure using path compression.
-  Returns inputs unchanged when index is out of bounds. -/
-def findD (self : UnionFind) (x : Nat) : UnionFind × Nat :=
-  if h : x < self.size then
-    match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
-  else
-    (self, x)
-
-@[simp] theorem find_size (self : UnionFind) (x : Fin self.size) :
-    (self.find x).1.size = self.size := by simp [find, size, FindAux.size_eq]
-
-@[simp] theorem find_root_2 (self : UnionFind) (x : Fin self.size) :
-    (self.find x).2.1.1 = self.rootD x := by simp [find, findAux_root, rootD]
-
-@[simp] theorem find_parent_1 (self : UnionFind) (x : Fin self.size) :
-    (self.find x).1.parent x = self.rootD x := by
-  simp only [parent, Array.length_toList, find]
-  rw [parentD_findAux, if_pos rfl]
-
-theorem find_parent_or (self : UnionFind) (x : Fin self.size) (i) :
-    (self.find x).1.parent i = self.rootD i ∧ self.rootD i = self.rootD x ∨
-    (self.find x).1.parent i = self.parent i := parentD_findAux_or ..
-
-@[simp] theorem find_root_1 (self : UnionFind) (x : Fin self.size) (i : Nat) :
-    (self.find x).1.rootD i = self.rootD i := by
-  if h : (self.find x).1.parent i = i then
-    rw [rootD_eq_self.2 h]
-    obtain ⟨h1, _⟩ | h1 := find_parent_or self x i <;> rw [h1] at h
-    · rw [h]
-    · rw [rootD_eq_self.2 h]
-  else
-    have := Nat.sub_lt_sub_left ((self.find x).1.lt_rankMax _) ((self.find x).1.rank_lt h)
-    rw [← rootD_parent, find_root_1 self x ((self.find x).1.parent i)]
-    obtain ⟨h1, _⟩ | h1 := find_parent_or self x i
-    · rw [h1, rootD_rootD]
-    · rw [h1, rootD_parent]
-termination_by  (self.find x).1.rankMax - (self.find x).1.rank i
-decreasing_by exact this -- why is this needed? It is way slower without it
-
-/-- Link two union-find nodes -/
-def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
-  if x.1 = y then
-    self
-  else
-    let nx := self.get x
-    let ny := self.get y
-    if ny.rank < nx.rank then
-      self.set y {ny with parent := x}
-    else
-      let arr₁ := self.set x {nx with parent := y}
-      if nx.rank = ny.rank then
-        arr₁.set y {ny with rank := ny.rank + 1} (by simp [arr₁])
-      else
-        arr₁
-
-theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
-    (hroot : (arr.get x).rank < (arr.get y).rank ∨ (arr.get y).parent = y)
-    (H : (arr.get x).rank ≤ (arr.get y).rank) {i : Nat}
-    (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
-    (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
-    (hR : ∀ {i}, rankD arr' i =
-      if y.1 = i ∧ (arr.get x).rank = (arr.get y).rank then
-        (arr.get y).rank + 1
-      else rankD arr i) :
-    ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by
-  simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
-    split <;> rename_i h₂ <;> intro h
-  · simp [h₂] at h
-  · simp only [rankD_eq, Array.get_eq_getElem]
-    split <;> rename_i h₃
-    · rw [← h₃]; apply Nat.lt_succ_self
-    · exact Nat.lt_of_le_of_ne H h₃
-  · cases h₂.1
-    simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot
-    simp only [hroot, parentD_eq, not_true_eq_false] at h
-  · have := rankD_lt h
-    split <;> rename_i h₃
-    · rw [← rankD_eq, h₃.1]; exact Nat.lt_succ_of_lt this
-    · exact this
-
-theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
-    (h : (arr.get x).rank < (arr.get y).rank) {i : Nat}
-    (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) :
-    let arr' := arr.set x ⟨y, (arr.get x).rank⟩
-    parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
-  setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set
-    (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem])
-
-@[simp] theorem linkAux_size : (linkAux self x y).size = self.size := by
-  simp only [linkAux, Array.get_eq_getElem]
-  split <;> [rfl; split] <;> [skip; split] <;> simp
-
-/-- Link a union-find node to a root node. -/
-def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) : UnionFind where
-  arr := linkAux self.arr x y
-  parentD_lt h := by
-    simp only [Array.length_toList, linkAux_size] at *
-    simp only [linkAux, Array.get_eq_getElem]
-    split <;> [skip; split <;> [skip; split]]
-    · exact self.parentD_lt h
-    · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h]
-    · rw [parentD_set]; split
-      · exact self.parent'_lt _
-      · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
-    · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
-  rankD_lt := by
-    rw [parent, parentD_eq] at yroot
-    simp only [linkAux, Array.get_eq_getElem, ne_eq]
-    split <;> [skip; split <;> [skip; split]]
-    · exact self.rankD_lt
-    · exact setParent_rankD_lt ‹_› self.rankD_lt
-    · refine setParentBump_rankD_lt (.inr yroot) (Nat.le_of_eq ‹_›) self.rankD_lt (by
-        simp only [parentD_set, ite_eq_right_iff]
-        rintro rfl
-        simp [*, parentD_eq]) fun {i} => ?_
-      simp only [rankD_set, Fin.eta, Array.get_eq_getElem]
-      split
-      · simp_all
-      · simp_all only [Array.get_eq_getElem, Array.length_toList, Nat.lt_irrefl, not_false_eq_true,
-          and_true, ite_false, ite_eq_right_iff]
-        rintro rfl
-        simp [rankD_eq, *]
-    · exact setParent_rankD_lt (Nat.lt_of_le_of_ne (Nat.not_lt.1 ‹_›) ‹_›) self.rankD_lt
-
-@[inherit_doc link]
-def linkN (self : UnionFind) (x y : Fin n) (yroot : self.parent y = y) (h : n = self.size) :
-    UnionFind := match n, h with | _, rfl => self.link x y yroot
-
-/-- Link a union-find node to a root node. Panics if either index is out of bounds. -/
-def link! (self : UnionFind) (x y : Nat) (yroot : self.parent y = y) : UnionFind :=
-  if h : x < self.size ∧ y < self.size then
-    self.link ⟨x, h.1⟩ ⟨y, h.2⟩ yroot
-  else
-    panicWith self "index out of bounds"
-
-/-- Link two union-find nodes, uniting their respective classes. -/
-def union (self : UnionFind) (x y : Fin self.size) : UnionFind :=
-  let ⟨self₁, rx, ex⟩ := self.find x
-  have hy := by rw [ex]; exact y.2
-  match eq : self₁.find ⟨y, hy⟩ with
-  | ⟨self₂, ry, ey⟩ =>
-    self₂.link ⟨rx, by rw [ey]; exact rx.2⟩ ry <| by
-      have := find_root_1 self₁ ⟨y, hy⟩ (⟨y, hy⟩ : Fin _)
-      rw [← find_root_2, eq] at this; simp at this
-      rw [← this, parent_rootD]
-
-@[inherit_doc union]
-def unionN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind :=
-  match n, h with | _, rfl => self.union x y
-
-/-- Link two union-find nodes, uniting their respective classes.
-Panics if either index is out of bounds. -/
-def union! (self : UnionFind) (x y : Nat) : UnionFind :=
-  if h : x < self.size ∧ y < self.size then
-    self.union ⟨x, h.1⟩ ⟨y, h.2⟩
-  else
-    panicWith self "index out of bounds"
-
-/-- Check whether two union-find nodes are equivalent, updating structure using path compression. -/
-def checkEquiv (self : UnionFind) (x y : Fin self.size) : UnionFind × Bool :=
-  let ⟨s, ⟨r₁, _⟩, h⟩ := self.find x
-  let ⟨s, ⟨r₂, _⟩, _⟩ := s.find (h ▸ y)
-  (s, r₁ == r₂)
-
-@[inherit_doc checkEquiv]
-def checkEquivN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind × Bool :=
-  match n, h with | _, rfl => self.checkEquiv x y
-
-/-- Check whether two union-find nodes are equivalent, updating structure using path compression.
-Panics if either index is out of bounds. -/
-def checkEquiv! (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
-  if h : x < self.size ∧ y < self.size then
-    self.checkEquiv ⟨x, h.1⟩ ⟨y, h.2⟩
-  else
-    panicWith (self, false) "index out of bounds"
-
-/-- Check whether two union-find nodes are equivalent with path compression,
-returns `x == y` if either index is out of bounds -/
-def checkEquivD (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
-  let (s, x) := self.findD x
-  let (s, y) := s.findD y
-  (s, x == y)
-
-/-- Equivalence relation from a `UnionFind` structure -/
-def Equiv (self : UnionFind) (a b : Nat) : Prop := self.rootD a = self.rootD b
+-- The `UnionFind` structure is an implementation of disjoint-set data structure
+-- that uses path compression to make the primary operations run in amortized
+-- nearly linear time. The nodes of a `UnionFind` structure `s` are natural
+-- numbers smaller than `s.size`. The structure associates with a canonical
+-- representative from its equivalence class. The structure can be extended
+-- using the `push` operation and equivalence classes can be updated using the
+-- `union` operation.
+
+-- The main operations for `UnionFind` are:
+
+-- * `empty`/`mkEmpty` are used to create a new empty structure.
+-- * `size` returns the size of the data structure.
+-- * `push` adds a new node to a structure, unlinked to any other node.
+-- * `union` links two nodes of the data structure, joining their equivalence
+--   classes, and performs path compression.
+-- * `find` returns the canonical representative of a node and updates the data
+--   structure using path compression.
+-- * `root` returns the canonical representative of a node without altering the
+--   data structure.
+-- * `checkEquiv` checks whether two nodes have the same canonical representative
+--   and updates the structure using path compression.
+
+-- Most use cases should prefer `find` over `root` to benefit from the speedup from path-compression.
+
+-- The main operations use `Fin s.size` to represent nodes of the union-find structure.
+-- Some alternatives are provided:
+
+-- * `unionN`, `findN`, `rootN`, `checkEquivN` use `Fin n` with a proof that `n = s.size`.
+-- * `union!`, `find!`, `root!`, `checkEquiv!` use `Nat` and panic when the indices are out of bounds.
+-- * `findD`, `rootD`, `checkEquivD` use `Nat` and treat out of bound indices as isolated nodes.
+
+-- The noncomputable relation `UnionFind.Equiv` is provided to use the equivalence relation from a
+-- `UnionFind` structure in the context of proofs.
+-- -/
+-- structure UnionFind where
+--   /-- Array of union-find nodes -/
+--   arr : Array UFNode
+--   /-- Validity for parent nodes -/
+--   parentD_lt : ∀ {i}, i < arr.size → parentD arr i < arr.size
+--   /-- Validity for rank -/
+--   rankD_lt : ∀ {i}, parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
+
+-- namespace UnionFind
+
+-- /-- Size of union-find structure. -/
+-- @[inline] abbrev size (self : UnionFind) := self.arr.size
+
+-- /-- Create an empty union-find structure with specific capacity -/
+-- def mkEmpty (c : Nat) : UnionFind where
+--   arr := Array.mkEmpty c
+--   parentD_lt := nofun
+--   rankD_lt := nofun
+
+-- /-- Empty union-find structure -/
+-- def empty := mkEmpty 0
+
+-- instance : EmptyCollection UnionFind := ⟨.empty⟩
+
+-- /-- Parent of union-find node -/
+-- abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
+
+-- theorem parent'_lt (self : UnionFind) (i : Nat) (h) :
+--     self.arr[i].parent < self.size := by
+--   simp [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList, h]
+
+-- theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by
+--   simp only [parentD]; split <;> simp only [*, parent'_lt]
+
+-- /-- Rank of union-find node -/
+-- abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
+
+-- theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i →
+--     self.rank i < self.rank (self.parent i) := by simpa only [rank] using self.rankD_lt
+
+-- theorem rank'_lt (self : UnionFind) (i : Fin self.size) : (self.arr[i]).parent ≠ i →
+--     self.rank i < self.rank (self.arr[i]).parent := by
+--   simpa only [← parentD_eq] using self.rankD_lt
+
+-- /-- Maximum rank of nodes in a union-find structure -/
+-- noncomputable def rankMax (self : UnionFind) := self.arr.foldr (max ·.rank) 0 + 1
+
+-- theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) :
+--     (self.arr[i]).rank < self.rankMax := by
+--   let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
+--     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
+--     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
+--   simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList]
+--   exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2)
+
+-- theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
+--     rankD self.arr i < self.rankMax := by
+--   simp [rankD]; split <;> [apply rank'_lt_rankMax; apply Nat.succ_pos]
+
+-- theorem lt_rankMax (self : UnionFind) (i : Nat) : self.rank i < self.rankMax := rankD_lt_rankMax ..
+
+-- theorem push_rankD (arr : Array UFNode) : rankD (arr.push ⟨arr.size, 0⟩) i = rankD arr i := by
+--   simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
+--   split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
+
+-- theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩) i = parentD arr i := by
+--   simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
+--   split <;> split <;> try simp
+--   · exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
+--   · cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
+
+-- /-- Add a new node to a union-find structure, unlinked with any other nodes -/
+-- def push (self : UnionFind) : UnionFind where
+--   arr := self.arr.push ⟨self.arr.size, 0⟩
+--   parentD_lt {i} := by
+--     simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem]
+--     split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt _); exact id]
+--   rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt
+
+-- /-- Root of a union-find node. -/
+-- def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
+--   let y := (self.arr[x]).parent
+--   if h : y = x then
+--     x
+--   else
+--     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
+--     self.root ⟨y, self.parent'_lt x⟩
+-- termination_by self.rankMax - self.rank x
+
+-- @[inherit_doc root]
+-- def rootN (self : UnionFind) (x : Fin n) (h : n = self.size) : Fin n :=
+--   match n, h with | _, rfl => self.root x
+
+-- /-- Root of a union-find node. Panics if index is out of bounds. -/
+-- def root! (self : UnionFind) (x : Nat) : Nat :=
+--   if h : x < self.size then self.root ⟨x, h⟩ else panicWith x "index out of bounds"
+
+-- /-- Root of a union-find node. Returns input if index is out of bounds. -/
+-- def rootD (self : UnionFind) (x : Nat) : Nat :=
+--   if h : x < self.size then self.root ⟨x, h⟩ else x
+
+-- @[nolint unusedHavesSuffices]
+-- theorem parent_root (self : UnionFind) (x : Fin self.size) :
+--     (self.arr[self.root x]).parent = self.root x := by
+--   rw [root]; split <;> [assumption; skip]
+--   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+--   apply parent_root
+-- termination_by self.rankMax - self.rank x
+
+-- theorem parent_rootD (self : UnionFind) (x : Nat) :
+--     self.parent (self.rootD x) = self.rootD x := by
+--   rw [rootD]
+--   split
+--   · simp [parentD, parent_root, -Array.get_eq_getElem]
+--   · simp [parentD_of_not_lt, *]
+
+-- @[nolint unusedHavesSuffices]
+-- theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
+--   simp only [rootD, Array.length_toList, parent_lt]
+--   split
+--   · simp only [parentD, ↓reduceDIte, *]
+--     (conv => rhs; rw [root]); split
+--     · rw [root, dif_pos] <;> simp_all
+--     · simp
+--   · simp only [not_false_eq_true, parentD_of_not_lt, *]
+
+-- theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x < self.size := by
+--   simp only [rootD, Array.length_toList]; split <;> simp [*]
+
+-- @[nolint unusedHavesSuffices]
+-- theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by
+--   refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩
+--   rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
+
+-- theorem rootD_rootD {self : UnionFind} {x : Nat} : self.rootD (self.rootD x) = self.rootD x :=
+--   rootD_eq_self.2 (parent_rootD ..)
+
+-- theorem rootD_ext {m1 m2 : UnionFind}
+--     (H : ∀ x, m1.parent x = m2.parent x) {x} : m1.rootD x = m2.rootD x := by
+--   if h : m2.parent x = x then
+--     rw [rootD_eq_self.2 h, rootD_eq_self.2 ((H _).trans h)]
+--   else
+--     have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
+--     rw [← rootD_parent, H, rootD_ext H, rootD_parent]
+-- termination_by m2.rankMax - m2.rank x
+
+-- theorem le_rank_root {self : UnionFind} {x : Nat} : self.rank x ≤ self.rank (self.rootD x) := by
+--   if h : self.parent x = x then
+--     rw [rootD_eq_self.2 h]; exact Nat.le_refl ..
+--   else
+--     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
+--     rw [← rootD_parent]
+--     exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
+-- termination_by self.rankMax - self.rank x
+
+-- theorem lt_rank_root {self : UnionFind} {x : Nat} :
+--     self.rank x < self.rank (self.rootD x) ↔ self.parent x ≠ x := by
+--   refine ⟨fun h h' => Nat.ne_of_lt h (by rw [rootD_eq_self.2 h']), fun h => ?_⟩
+--   rw [← rootD_parent]
+--   exact Nat.lt_of_lt_of_le (self.rank_lt h) le_rank_root
+
+-- /-- Auxiliary data structure for find operation -/
+-- structure FindAux (n : Nat) where
+--   /-- Array of nodes -/
+--   s : Array UFNode
+--   /-- Index of root node -/
+--   root : Fin n
+--   /-- Size requirement -/
+--   size_eq : s.size = n
+
+-- /-- Auxiliary function for find operation -/
+-- def findAux (self : UnionFind) (x : Fin self.size) : FindAux self.size :=
+--   let y := self.arr[x].parent
+--   if h : y = x then
+--     ⟨self.arr, x, rfl⟩
+--   else
+--     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
+--     let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt x⟩
+--     ⟨arr₁.modify x fun s => { s with parent := root }, root, by simp [H]⟩
+-- termination_by self.rankMax - self.rank x
+
+-- @[nolint unusedHavesSuffices]
+-- theorem findAux_root {self : UnionFind} {x : Fin self.size} :
+--     (findAux self x).root = self.root x := by
+--   rw [findAux, root]
+--   simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]
+--   split <;> simp only
+--   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+--   exact findAux_root
+-- termination_by self.rankMax - self.rank x
+
+-- @[nolint unusedHavesSuffices]
+-- theorem findAux_s {self : UnionFind} {x : Fin self.size} :
+--     (findAux self x).s = if self.arr[x].parent = x then self.arr else
+--       (self.findAux ⟨_, self.parent'_lt x⟩).s.modify x fun s =>
+--         { s with parent := self.rootD x } := by
+--   rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
+--   · rw [findAux]; split <;> rfl
+--   · rw [← rootD_parent, parent, parentD_eq]
+--     simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]
+--     apply dif_pos
+--     exact parent'_lt ..
+
+-- set_option linter.deprecated false in
+-- theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
+--     rankD (findAux self x).s i = self.rank i := by
+--   if h : i < self.size then
+--     rw [findAux_s]; split <;> [rfl; skip]
+--     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+--     have := lt_of_parentD (by rwa [parentD_eq])
+--     rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify]
+--     split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
+--   else
+--     simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
+--     rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
+-- termination_by self.rankMax - self.rank x
+
+-- set_option linter.deprecated false in
+-- theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
+--     parentD (findAux self x).s i =
+--     if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt x⟩).s i := by
+--   rw [findAux_s]; split <;> [split; skip]
+--   · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]
+--   · rw [findAux_s]; simp [*, -Array.get_eq_getElem]
+--   · next h =>
+--     rw [parentD]; split <;> rename_i h'
+--     · rw [Array.get_modify (by simpa using h')]
+--       simp only [Array.data_length, @eq_comm _ i]
+--       split <;> simp [← parentD_eq, -Array.get_eq_getElem]
+--     · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
+--       rw [parentD, dif_neg]; simpa using h'
+
+-- theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} :
+--     parentD (findAux self x).s (self.rootD x) = self.rootD x := by
+--   rw [parentD_findAux]; split <;> [rfl; rename_i h]
+--   rw [rootD_eq_self, parent, parentD_eq] at h
+--   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+--   rw [← rootD_parent, parent, parentD_eq]
+--   exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt x⟩)
+-- termination_by self.rankMax - self.rank x
+
+-- theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) :
+--     parentD (findAux self x).s i < self.size := by
+--   if h' : self.arr[x].parent = x then
+--     rw [findAux_s, if_pos h']; apply self.parentD_lt h
+--   else
+--     rw [parentD_findAux]
+--     split
+--     · simp [rootD_lt]
+--     · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+--       apply parentD_findAux_lt h
+-- termination_by self.rankMax - self.rank x
+
+-- theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
+--     parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨
+--     parentD (findAux self x).s i = self.parent i := by
+--   if h' : self.arr[x].parent = x then
+--     rw [findAux_s, if_pos h']; exact .inr rfl
+--   else
+--     rw [parentD_findAux]
+--     split
+--     · simp [*]
+--     · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+--       exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
+--         simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
+-- termination_by self.rankMax - self.rank x
+
+-- theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
+--     parentD (findAux self x).s i ≠ i →
+--     self.rank i < self.rank (parentD (findAux self x).s i) := by
+--   if h' : self.arr[x].parent = x then
+--     rw [findAux_s, if_pos h']; apply self.rank_lt
+--   else
+--     rw [parentD_findAux]; split <;> rename_i h <;> intro h'
+--     · subst i; rwa [lt_rank_root, Ne, ← rootD_eq_self]
+--     · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+--       apply lt_rankD_findAux h'
+-- termination_by self.rankMax - self.rank x
+
+-- /-- Find root of a union-find node, updating the structure using path compression. -/
+-- def find (self : UnionFind) (x : Fin self.size) :
+--     (s : UnionFind) × {_root : Fin s.size // s.size = self.size} :=
+--   let r := self.findAux x
+--   { 1.arr := r.s
+--     2.1.val := r.root
+--     1.parentD_lt := fun h => by
+--       simp only [Array.length_toList, FindAux.size_eq] at *
+--       exact parentD_findAux_lt h
+--     1.rankD_lt := fun h => by rw [rankD_findAux, rankD_findAux]; exact lt_rankD_findAux h
+--     2.1.isLt := show _ < r.s.size by rw [r.size_eq]; exact r.root.2
+--     2.2 := by simp [size, r.size_eq] }
+
+-- @[inherit_doc find]
+-- def findN (self : UnionFind) (x : Fin n) (h : n = self.size) : UnionFind × Fin n :=
+--   match n, h with | _, rfl => match self.find x with | ⟨s, r, h⟩ => (s, Fin.cast h r)
+
+-- /-- Find root of a union-find node, updating the structure using path compression.
+--   Panics if index is out of bounds. -/
+-- def find! (self : UnionFind) (x : Nat) : UnionFind × Nat :=
+--   if h : x < self.size then
+--     match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
+--   else
+--     panicWith (self, x) "index out of bounds"
+
+-- /-- Find root of a union-find node, updating the structure using path compression.
+--   Returns inputs unchanged when index is out of bounds. -/
+-- def findD (self : UnionFind) (x : Nat) : UnionFind × Nat :=
+--   if h : x < self.size then
+--     match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
+--   else
+--     (self, x)
+
+-- @[simp] theorem find_size (self : UnionFind) (x : Fin self.size) :
+--     (self.find x).1.size = self.size := by simp [find, size, FindAux.size_eq]
+
+-- @[simp] theorem find_root_2 (self : UnionFind) (x : Fin self.size) :
+--     (self.find x).2.1.1 = self.rootD x := by simp [find, findAux_root, rootD]
+
+-- @[simp] theorem find_parent_1 (self : UnionFind) (x : Fin self.size) :
+--     (self.find x).1.parent x = self.rootD x := by
+--   simp only [parent, Array.length_toList, find]
+--   rw [parentD_findAux, if_pos rfl]
+
+-- theorem find_parent_or (self : UnionFind) (x : Fin self.size) (i) :
+--     (self.find x).1.parent i = self.rootD i ∧ self.rootD i = self.rootD x ∨
+--     (self.find x).1.parent i = self.parent i := parentD_findAux_or ..
+
+-- @[simp] theorem find_root_1 (self : UnionFind) (x : Fin self.size) (i : Nat) :
+--     (self.find x).1.rootD i = self.rootD i := by
+--   if h : (self.find x).1.parent i = i then
+--     rw [rootD_eq_self.2 h]
+--     obtain ⟨h1, _⟩ | h1 := find_parent_or self x i <;> rw [h1] at h
+--     · rw [h]
+--     · rw [rootD_eq_self.2 h]
+--   else
+--     have := Nat.sub_lt_sub_left ((self.find x).1.lt_rankMax _) ((self.find x).1.rank_lt h)
+--     rw [← rootD_parent, find_root_1 self x ((self.find x).1.parent i)]
+--     obtain ⟨h1, _⟩ | h1 := find_parent_or self x i
+--     · rw [h1, rootD_rootD]
+--     · rw [h1, rootD_parent]
+-- termination_by  (self.find x).1.rankMax - (self.find x).1.rank i
+-- decreasing_by exact this -- why is this needed? It is way slower without it
+
+-- /-- Link two union-find nodes -/
+-- def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
+--   if x.1 = y then
+--     self
+--   else
+--     let nx := self[x]
+--     let ny := self[y]
+--     if ny.rank < nx.rank then
+--       self.set y {ny with parent := x}
+--     else
+--       let arr₁ := self.set x {nx with parent := y}
+--       if nx.rank = ny.rank then
+--         arr₁.set y {ny with rank := ny.rank + 1} (by simp [arr₁])
+--       else
+--         arr₁
+
+-- theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
+--     (hroot : arr[x].rank < arr[y].rank ∨ arr[y].parent = y)
+--     (H : arr[x].rank ≤ arr[y].rank) {i : Nat}
+--     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
+--     (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
+--     (hR : ∀ {i}, rankD arr' i =
+--       if y.1 = i ∧ arr[x].rank = arr[y].rank then
+--         arr[y].rank + 1
+--       else rankD arr i) :
+--     ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by
+--   simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
+--     split <;> rename_i h₂ <;> intro h
+--   · simp [h₂] at h
+--   · simp only [rankD_eq, Array.get_eq_getElem]
+--     split <;> rename_i h₃
+--     · rw [← h₃]; apply Nat.lt_succ_self
+--     · exact Nat.lt_of_le_of_ne H h₃
+--   · cases h₂.1
+--     simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot
+--     simp only [hroot, parentD_eq, not_true_eq_false] at h
+--   · have := rankD_lt h
+--     split <;> rename_i h₃
+--     · rw [← rankD_eq, h₃.1]; exact Nat.lt_succ_of_lt this
+--     · exact this
+
+-- theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
+--     (h : arr[x].rank < arr[y].rank) {i : Nat}
+--     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) :
+--     let arr' := arr.set x ⟨y, arr[x].rank⟩
+--     parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
+--   setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set
+--     (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem])
+
+-- @[simp] theorem linkAux_size : (linkAux self x y).size = self.size := by
+--   simp only [linkAux, Array.get_eq_getElem]
+--   split <;> [rfl; split] <;> [skip; split] <;> simp
+
+-- /-- Link a union-find node to a root node. -/
+-- def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) : UnionFind where
+--   arr := linkAux self.arr x y
+--   parentD_lt h := by
+--     simp only [Array.length_toList, linkAux_size] at *
+--     simp only [linkAux, Array.get_eq_getElem]
+--     split <;> [skip; split <;> [skip; split]]
+--     · exact self.parentD_lt h
+--     · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h]
+--     · rw [parentD_set]; split
+--       · exact self.parent'_lt _
+--       · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
+--     · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
+--   rankD_lt := by
+--     rw [parent, parentD_eq] at yroot
+--     simp only [linkAux, Array.get_eq_getElem, ne_eq]
+--     split <;> [skip; split <;> [skip; split]]
+--     · exact self.rankD_lt
+--     · exact setParent_rankD_lt ‹_› self.rankD_lt
+--     · refine setParentBump_rankD_lt (.inr yroot) (Nat.le_of_eq ‹_›) self.rankD_lt (by
+--         simp only [parentD_set, ite_eq_right_iff]
+--         rintro rfl
+--         simp [*, parentD_eq]) fun {i} => ?_
+--       simp only [rankD_set, Fin.eta, Array.get_eq_getElem]
+--       split
+--       · simp_all
+--       · simp_all only [Array.get_eq_getElem, Array.length_toList, Nat.lt_irrefl, not_false_eq_true,
+--           and_true, ite_false, ite_eq_right_iff]
+--         rintro rfl
+--         simp [rankD_eq, *]
+--     · exact setParent_rankD_lt (Nat.lt_of_le_of_ne (Nat.not_lt.1 ‹_›) ‹_›) self.rankD_lt
+
+-- @[inherit_doc link]
+-- def linkN (self : UnionFind) (x y : Fin n) (yroot : self.parent y = y) (h : n = self.size) :
+--     UnionFind := match n, h with | _, rfl => self.link x y yroot
+
+-- /-- Link a union-find node to a root node. Panics if either index is out of bounds. -/
+-- def link! (self : UnionFind) (x y : Nat) (yroot : self.parent y = y) : UnionFind :=
+--   if h : x < self.size ∧ y < self.size then
+--     self.link ⟨x, h.1⟩ ⟨y, h.2⟩ yroot
+--   else
+--     panicWith self "index out of bounds"
+
+-- /-- Link two union-find nodes, uniting their respective classes. -/
+-- def union (self : UnionFind) (x y : Fin self.size) : UnionFind :=
+--   let ⟨self₁, rx, ex⟩ := self.find x
+--   have hy := by rw [ex]; exact y.2
+--   match eq : self₁.find ⟨y, hy⟩ with
+--   | ⟨self₂, ry, ey⟩ =>
+--     self₂.link ⟨rx, by rw [ey]; exact rx.2⟩ ry <| by
+--       have := find_root_1 self₁ ⟨y, hy⟩ (⟨y, hy⟩ : Fin _)
+--       rw [← find_root_2, eq] at this; simp at this
+--       rw [← this, parent_rootD]
+
+-- @[inherit_doc union]
+-- def unionN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind :=
+--   match n, h with | _, rfl => self.union x y
+
+-- /-- Link two union-find nodes, uniting their respective classes.
+-- Panics if either index is out of bounds. -/
+-- def union! (self : UnionFind) (x y : Nat) : UnionFind :=
+--   if h : x < self.size ∧ y < self.size then
+--     self.union ⟨x, h.1⟩ ⟨y, h.2⟩
+--   else
+--     panicWith self "index out of bounds"
+
+-- /-- Check whether two union-find nodes are equivalent, updating structure using path compression. -/
+-- def checkEquiv (self : UnionFind) (x y : Fin self.size) : UnionFind × Bool :=
+--   let ⟨s, ⟨r₁, _⟩, h⟩ := self.find x
+--   let ⟨s, ⟨r₂, _⟩, _⟩ := s.find (h ▸ y)
+--   (s, r₁ == r₂)
+
+-- @[inherit_doc checkEquiv]
+-- def checkEquivN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind × Bool :=
+--   match n, h with | _, rfl => self.checkEquiv x y
+
+-- /-- Check whether two union-find nodes are equivalent, updating structure using path compression.
+-- Panics if either index is out of bounds. -/
+-- def checkEquiv! (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
+--   if h : x < self.size ∧ y < self.size then
+--     self.checkEquiv ⟨x, h.1⟩ ⟨y, h.2⟩
+--   else
+--     panicWith (self, false) "index out of bounds"
+
+-- /-- Check whether two union-find nodes are equivalent with path compression,
+-- returns `x == y` if either index is out of bounds -/
+-- def checkEquivD (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
+--   let (s, x) := self.findD x
+--   let (s, y) := s.findD y
+--   (s, x == y)
+
+-- /-- Equivalence relation from a `UnionFind` structure -/
+-- def Equiv (self : UnionFind) (a b : Nat) : Prop := self.rootD a = self.rootD b

From eedab893ad8c86c657372c47a631f1c659abb9d8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:50:40 +1100
Subject: [PATCH 14/18] .

---
 Batteries/Data/UnionFind/Lemmas.lean | 278 +++++++++++++--------------
 1 file changed, 139 insertions(+), 139 deletions(-)

diff --git a/Batteries/Data/UnionFind/Lemmas.lean b/Batteries/Data/UnionFind/Lemmas.lean
index 9a7b0dac58..d94c75568c 100644
--- a/Batteries/Data/UnionFind/Lemmas.lean
+++ b/Batteries/Data/UnionFind/Lemmas.lean
@@ -1,139 +1,139 @@
-/-
-Copyright (c) 2021 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-import Batteries.Data.UnionFind.Basic
-
-namespace Batteries.UnionFind
-
-@[simp] theorem arr_empty : empty.arr = #[] := rfl
-@[simp] theorem parent_empty : empty.parent a = a := rfl
-@[simp] theorem rank_empty : empty.rank a = 0 := rfl
-@[simp] theorem rootD_empty : empty.rootD a = a := rfl
-
-@[simp] theorem arr_push {m : UnionFind} : m.push.arr = m.arr.push ⟨m.arr.size, 0⟩ := rfl
-
-@[simp] theorem parentD_push {arr : Array UFNode} :
-    parentD (arr.push ⟨arr.size, 0⟩) a = parentD arr a := by
-  simp [parentD]; split <;> split <;> try simp [Array.getElem_push, *]
-  · next h1 h2 =>
-    simp [Nat.lt_succ] at h1 h2
-    exact Nat.le_antisymm h2 h1
-  · next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
-
-@[simp] theorem parent_push {m : UnionFind} : m.push.parent a = m.parent a := by simp [parent]
-
-@[simp] theorem rankD_push {arr : Array UFNode} :
-    rankD (arr.push ⟨arr.size, 0⟩) a = rankD arr a := by
-  simp [rankD]; split <;> split <;> try simp [Array.getElem_push, *]
-  next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
-
-@[simp] theorem rank_push {m : UnionFind} : m.push.rank a = m.rank a := by simp [rank]
-
-@[simp] theorem rankMax_push {m : UnionFind} : m.push.rankMax = m.rankMax := by simp [rankMax]
-
-@[simp] theorem root_push {self : UnionFind} : self.push.rootD x = self.rootD x :=
-  rootD_ext fun _ => parent_push
-
-@[simp] theorem arr_link : (link self x y yroot).arr = linkAux self.arr x y := rfl
-
-theorem parentD_linkAux {self} {x y : Fin self.size} :
-    parentD (linkAux self x y) i =
-    if x.1 = y then
-      parentD self i
-    else
-      if (self.get y).rank < (self.get x).rank then
-        if y = i then x else parentD self i
-      else
-        if x = i then y else parentD self i := by
-  dsimp only [linkAux]; split <;> [rfl; split] <;> [rw [parentD_set]; split] <;> rw [parentD_set]
-  split <;> [(subst i; rwa [if_neg, parentD_eq]); rw [parentD_set]]
-
-theorem parent_link {self} {x y : Fin self.size} (yroot) {i} :
-    (link self x y yroot).parent i =
-    if x.1 = y then
-      self.parent i
-    else
-      if self.rank y < self.rank x then
-        if y = i then x else self.parent i
-      else
-        if x = i then y else self.parent i := by
-  simp [rankD_eq]; exact parentD_linkAux
-
-theorem root_link {self : UnionFind} {x y : Fin self.size}
-    (xroot : self.parent x = x) (yroot : self.parent y = y) :
-    ∃ r, (r = x ∨ r = y) ∧ ∀ i,
-      (link self x y yroot).rootD i =
-      if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
-  if h : x.1 = y then
-    refine ⟨x, .inl rfl, fun i => ?_⟩
-    rw [rootD_ext (m2 := self) (fun _ => by rw [parent_link, if_pos h])]
-    split <;> [obtain _ | _ := ‹_› <;> simp [*]; rfl]
-  else
-  have {x y : Fin self.size}
-      (xroot : self.parent x = x) (yroot : self.parent y = y) {m : UnionFind}
-      (hm : ∀ i, m.parent i = if y = i then x.1 else self.parent i) :
-      ∃ r, (r = x ∨ r = y) ∧ ∀ i,
-        m.rootD i = if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
-    let rec go (i) :
-        m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i := by
-      if h : m.parent i = i then
-        rw [rootD_eq_self.2 h]; rw [hm i] at h; split at h
-        · rw [if_pos, h]; simp [← h, rootD_eq_self, xroot]
-        · rw [rootD_eq_self.2 ‹_›]; split <;> [skip; rfl]
-          next h' => exact h'.resolve_right (Ne.symm ‹_›)
-      else
-        have _ := Nat.sub_lt_sub_left (m.lt_rankMax i) (m.rank_lt h)
-        rw [← rootD_parent, go (m.parent i)]
-        rw [hm i]; split <;> [subst i; rw [rootD_parent]]
-        simp [rootD_eq_self.2 xroot, rootD_eq_self.2 yroot]
-    termination_by m.rankMax - m.rank i
-    exact ⟨x, .inl rfl, go⟩
-  if hr : self.rank y < self.rank x then
-    exact this xroot yroot fun i => by simp [parent_link, h, hr]
-  else
-    simpa (config := {singlePass := true}) [or_comm] using
-      this yroot xroot fun i => by simp [parent_link, h, hr]
-
-nonrec theorem Equiv.rfl : Equiv self a a := rfl
-theorem Equiv.symm : Equiv self a b → Equiv self b a := .symm
-theorem Equiv.trans : Equiv self a b → Equiv self b c → Equiv self a c := .trans
-
-@[simp] theorem equiv_empty : Equiv empty a b ↔ a = b := by simp [Equiv]
-
-@[simp] theorem equiv_push : Equiv self.push a b ↔ Equiv self a b := by simp [Equiv]
-
-@[simp] theorem equiv_rootD : Equiv self (self.rootD a) a := by simp [Equiv, rootD_rootD]
-@[simp] theorem equiv_rootD_l : Equiv self (self.rootD a) b ↔ Equiv self a b := by
-  simp [Equiv, rootD_rootD]
-@[simp] theorem equiv_rootD_r : Equiv self a (self.rootD b) ↔ Equiv self a b := by
-  simp [Equiv, rootD_rootD]
-
-theorem equiv_find : Equiv (self.find x).1 a b ↔ Equiv self a b := by simp [Equiv, find_root_1]
-
-theorem equiv_link {self : UnionFind} {x y : Fin self.size}
-    (xroot : self.parent x = x) (yroot : self.parent y = y) :
-    Equiv (link self x y yroot) a b ↔
-    Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
-  have {m : UnionFind} {x y : Fin self.size}
-      (xroot : self.rootD x = x) (yroot : self.rootD y = y)
-      (hm : ∀ i, m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i) :
-      Equiv m a b ↔
-      Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
-    simp [Equiv, hm, xroot, yroot]
-    by_cases h1 : rootD self a = x <;> by_cases h2 : rootD self b = x <;>
-      simp [h1, h2, imp_false, Decidable.not_not]
-    · simp [h2, Ne.symm h2]; split <;> simp [@eq_comm _ _ (rootD self b), *]
-    · by_cases h1 : rootD self a = y <;> by_cases h2 : rootD self b = y <;>
-        simp [h1, h2, @eq_comm _ _ (rootD self b), *]
-  obtain ⟨r, ha, hr⟩ := root_link xroot yroot; revert hr
-  rw [← rootD_eq_self] at xroot yroot
-  obtain rfl | rfl := ha
-  · exact this xroot yroot
-  · simpa [or_comm, and_comm] using this yroot xroot
-
-theorem equiv_union {self : UnionFind} {x y : Fin self.size} :
-    Equiv (union self x y) a b ↔
-    Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
-  simp [union]; rw [equiv_link (by simp [← rootD_eq_self, rootD_rootD])]; simp [equiv_find]
+-- /-
+-- Copyright (c) 2021 Mario Carneiro. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Mario Carneiro
+-- -/
+-- import Batteries.Data.UnionFind.Basic
+
+-- namespace Batteries.UnionFind
+
+-- @[simp] theorem arr_empty : empty.arr = #[] := rfl
+-- @[simp] theorem parent_empty : empty.parent a = a := rfl
+-- @[simp] theorem rank_empty : empty.rank a = 0 := rfl
+-- @[simp] theorem rootD_empty : empty.rootD a = a := rfl
+
+-- @[simp] theorem arr_push {m : UnionFind} : m.push.arr = m.arr.push ⟨m.arr.size, 0⟩ := rfl
+
+-- @[simp] theorem parentD_push {arr : Array UFNode} :
+--     parentD (arr.push ⟨arr.size, 0⟩) a = parentD arr a := by
+--   simp [parentD]; split <;> split <;> try simp [Array.getElem_push, *]
+--   · next h1 h2 =>
+--     simp [Nat.lt_succ] at h1 h2
+--     exact Nat.le_antisymm h2 h1
+--   · next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
+
+-- @[simp] theorem parent_push {m : UnionFind} : m.push.parent a = m.parent a := by simp [parent]
+
+-- @[simp] theorem rankD_push {arr : Array UFNode} :
+--     rankD (arr.push ⟨arr.size, 0⟩) a = rankD arr a := by
+--   simp [rankD]; split <;> split <;> try simp [Array.getElem_push, *]
+--   next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
+
+-- @[simp] theorem rank_push {m : UnionFind} : m.push.rank a = m.rank a := by simp [rank]
+
+-- @[simp] theorem rankMax_push {m : UnionFind} : m.push.rankMax = m.rankMax := by simp [rankMax]
+
+-- @[simp] theorem root_push {self : UnionFind} : self.push.rootD x = self.rootD x :=
+--   rootD_ext fun _ => parent_push
+
+-- @[simp] theorem arr_link : (link self x y yroot).arr = linkAux self.arr x y := rfl
+
+-- theorem parentD_linkAux {self} {x y : Fin self.size} :
+--     parentD (linkAux self x y) i =
+--     if x.1 = y then
+--       parentD self i
+--     else
+--       if (self.get y).rank < (self.get x).rank then
+--         if y = i then x else parentD self i
+--       else
+--         if x = i then y else parentD self i := by
+--   dsimp only [linkAux]; split <;> [rfl; split] <;> [rw [parentD_set]; split] <;> rw [parentD_set]
+--   split <;> [(subst i; rwa [if_neg, parentD_eq]); rw [parentD_set]]
+
+-- theorem parent_link {self} {x y : Fin self.size} (yroot) {i} :
+--     (link self x y yroot).parent i =
+--     if x.1 = y then
+--       self.parent i
+--     else
+--       if self.rank y < self.rank x then
+--         if y = i then x else self.parent i
+--       else
+--         if x = i then y else self.parent i := by
+--   simp [rankD_eq]; exact parentD_linkAux
+
+-- theorem root_link {self : UnionFind} {x y : Fin self.size}
+--     (xroot : self.parent x = x) (yroot : self.parent y = y) :
+--     ∃ r, (r = x ∨ r = y) ∧ ∀ i,
+--       (link self x y yroot).rootD i =
+--       if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
+--   if h : x.1 = y then
+--     refine ⟨x, .inl rfl, fun i => ?_⟩
+--     rw [rootD_ext (m2 := self) (fun _ => by rw [parent_link, if_pos h])]
+--     split <;> [obtain _ | _ := ‹_› <;> simp [*]; rfl]
+--   else
+--   have {x y : Fin self.size}
+--       (xroot : self.parent x = x) (yroot : self.parent y = y) {m : UnionFind}
+--       (hm : ∀ i, m.parent i = if y = i then x.1 else self.parent i) :
+--       ∃ r, (r = x ∨ r = y) ∧ ∀ i,
+--         m.rootD i = if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
+--     let rec go (i) :
+--         m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i := by
+--       if h : m.parent i = i then
+--         rw [rootD_eq_self.2 h]; rw [hm i] at h; split at h
+--         · rw [if_pos, h]; simp [← h, rootD_eq_self, xroot]
+--         · rw [rootD_eq_self.2 ‹_›]; split <;> [skip; rfl]
+--           next h' => exact h'.resolve_right (Ne.symm ‹_›)
+--       else
+--         have _ := Nat.sub_lt_sub_left (m.lt_rankMax i) (m.rank_lt h)
+--         rw [← rootD_parent, go (m.parent i)]
+--         rw [hm i]; split <;> [subst i; rw [rootD_parent]]
+--         simp [rootD_eq_self.2 xroot, rootD_eq_self.2 yroot]
+--     termination_by m.rankMax - m.rank i
+--     exact ⟨x, .inl rfl, go⟩
+--   if hr : self.rank y < self.rank x then
+--     exact this xroot yroot fun i => by simp [parent_link, h, hr]
+--   else
+--     simpa (config := {singlePass := true}) [or_comm] using
+--       this yroot xroot fun i => by simp [parent_link, h, hr]
+
+-- nonrec theorem Equiv.rfl : Equiv self a a := rfl
+-- theorem Equiv.symm : Equiv self a b → Equiv self b a := .symm
+-- theorem Equiv.trans : Equiv self a b → Equiv self b c → Equiv self a c := .trans
+
+-- @[simp] theorem equiv_empty : Equiv empty a b ↔ a = b := by simp [Equiv]
+
+-- @[simp] theorem equiv_push : Equiv self.push a b ↔ Equiv self a b := by simp [Equiv]
+
+-- @[simp] theorem equiv_rootD : Equiv self (self.rootD a) a := by simp [Equiv, rootD_rootD]
+-- @[simp] theorem equiv_rootD_l : Equiv self (self.rootD a) b ↔ Equiv self a b := by
+--   simp [Equiv, rootD_rootD]
+-- @[simp] theorem equiv_rootD_r : Equiv self a (self.rootD b) ↔ Equiv self a b := by
+--   simp [Equiv, rootD_rootD]
+
+-- theorem equiv_find : Equiv (self.find x).1 a b ↔ Equiv self a b := by simp [Equiv, find_root_1]
+
+-- theorem equiv_link {self : UnionFind} {x y : Fin self.size}
+--     (xroot : self.parent x = x) (yroot : self.parent y = y) :
+--     Equiv (link self x y yroot) a b ↔
+--     Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
+--   have {m : UnionFind} {x y : Fin self.size}
+--       (xroot : self.rootD x = x) (yroot : self.rootD y = y)
+--       (hm : ∀ i, m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i) :
+--       Equiv m a b ↔
+--       Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
+--     simp [Equiv, hm, xroot, yroot]
+--     by_cases h1 : rootD self a = x <;> by_cases h2 : rootD self b = x <;>
+--       simp [h1, h2, imp_false, Decidable.not_not]
+--     · simp [h2, Ne.symm h2]; split <;> simp [@eq_comm _ _ (rootD self b), *]
+--     · by_cases h1 : rootD self a = y <;> by_cases h2 : rootD self b = y <;>
+--         simp [h1, h2, @eq_comm _ _ (rootD self b), *]
+--   obtain ⟨r, ha, hr⟩ := root_link xroot yroot; revert hr
+--   rw [← rootD_eq_self] at xroot yroot
+--   obtain rfl | rfl := ha
+--   · exact this xroot yroot
+--   · simpa [or_comm, and_comm] using this yroot xroot
+
+-- theorem equiv_union {self : UnionFind} {x y : Fin self.size} :
+--     Equiv (union self x y) a b ↔
+--     Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
+--   simp [union]; rw [equiv_link (by simp [← rootD_eq_self, rootD_rootD])]; simp [equiv_find]

From 9ba2e12ce6570b7fed7ad4d3675e5f6632949f2b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:52:31 +1100
Subject: [PATCH 15/18] .

---
 Batteries/Data/BinaryHeap.lean   |  2 +-
 Batteries/Data/Vector/Basic.lean |  2 +-
 Batteries/StdDeprecations.lean   | 26 ++++++++++++++------------
 3 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/Batteries/Data/BinaryHeap.lean b/Batteries/Data/BinaryHeap.lean
index 29a273a9d0..897cca1c2a 100644
--- a/Batteries/Data/BinaryHeap.lean
+++ b/Batteries/Data/BinaryHeap.lean
@@ -88,7 +88,7 @@ def size (self : BinaryHeap α lt) : Nat := self.1.size
 def vector (self : BinaryHeap α lt) : Vector α self.size := ⟨self.1, rfl⟩
 
 /-- `O(1)`. Get an element in the heap by index. -/
-def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i
+def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1[i]'(i.2)
 
 /-- `O(log n)`. Insert an element into a `BinaryHeap`, preserving the max-heap property. -/
 def insert (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 0ae5871356..d5989898eb 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -68,7 +68,7 @@ instance [Inhabited α] : Inhabited (Vector α n) where
 
 /-- Get an element of a vector using a `Fin` index. -/
 @[inline] def get (v : Vector α n) (i : Fin n) : α :=
-  v.toArray.get (i.cast v.size_toArray.symm)
+  v.toArray[i.cast v.size_toArray.symm]
 
 /-- Get an element of a vector using a `USize` index and a proof that the index is within bounds. -/
 @[inline] def uget (v : Vector α n) (i : USize) (h : i.toNat < n) : α :=
diff --git a/Batteries/StdDeprecations.lean b/Batteries/StdDeprecations.lean
index 74a00f4f5a..a17f235cee 100644
--- a/Batteries/StdDeprecations.lean
+++ b/Batteries/StdDeprecations.lean
@@ -48,16 +48,18 @@ alias Std.compareOfLessAndEq_eq_lt := Batteries.compareOfLessAndEq_eq_lt
 @[deprecated (since := "2024-05-07")] alias Std.mkRBMap := Batteries.mkRBMap
 @[deprecated (since := "2024-05-07")] alias Std.BinomialHeap := Batteries.BinomialHeap
 @[deprecated (since := "2024-05-07")] alias Std.mkBinomialHeap := Batteries.mkBinomialHeap
-@[deprecated (since := "2024-05-07")] alias Std.UFNode := Batteries.UFNode
-@[deprecated (since := "2024-05-07")] alias Std.UnionFind := Batteries.UnionFind
 
--- Check that these generate usable deprecated hints
--- when referring to names inside these namespaces.
-set_option warningAsError true in
-/--
-error: `Std.UnionFind` has been deprecated, use `Batteries.UnionFind` instead
----
-error: unknown constant 'Std.UnionFind.find'
--/
-#guard_msgs in
-#eval Std.UnionFind.find
+-- TODO: restore these when UnionFind is un-commented.
+-- @[deprecated (since := "2024-05-07")] alias Std.UFNode := Batteries.UFNode
+-- @[deprecated (since := "2024-05-07")] alias Std.UnionFind := Batteries.UnionFind
+
+-- -- Check that these generate usable deprecated hints
+-- -- when referring to names inside these namespaces.
+-- set_option warningAsError true in
+-- /--
+-- error: `Std.UnionFind` has been deprecated, use `Batteries.UnionFind` instead
+-- ---
+-- error: unknown constant 'Std.UnionFind.find'
+-- -/
+-- #guard_msgs in
+-- #eval Std.UnionFind.find

From d69cd4d3491ac8520b8fa6f8a2c61be56988b9ef Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:55:45 +1100
Subject: [PATCH 16/18] fix test

---
 BatteriesTest/array.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/BatteriesTest/array.lean b/BatteriesTest/array.lean
index 89f784293e..58bb65b713 100644
--- a/BatteriesTest/array.lean
+++ b/BatteriesTest/array.lean
@@ -9,7 +9,7 @@ variable (v d : α)
 variable (g : i < (a.set! i v).size)
 variable (j_lt : j < (a.set! i v).size)
 
-#check_simp (a.set! i v).get ⟨i, g⟩ ~> v
+#check_simp (a.set! i v).get i g ~> v
 #check_simp (a.set! i v).get! i ~> (a.setD i v)[i]!
 #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
 #check_simp (a.set! i v)[i] ~> v

From 6b3f8776b7d77ec5f69bfead5aadca354ef526fc Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 20:56:24 +1100
Subject: [PATCH 17/18] fix long lines

---
 Batteries/Data/UnionFind/Basic.lean | 1178 ++++++++++++++-------------
 1 file changed, 590 insertions(+), 588 deletions(-)

diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index d2386f122c..289fdc7d57 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -1,590 +1,592 @@
--- /-
--- Copyright (c) 2021 Mario Carneiro. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Mario Carneiro
--- -/
--- import Batteries.Tactic.Alias
--- import Batteries.Tactic.Lint.Misc
--- import Batteries.Tactic.SeqFocus
--- import Batteries.Util.Panic
--- import Batteries.Data.Array.Lemmas
-
--- @[deprecated (since := "2024-10-05")]
--- protected alias Batteries.UnionFind.panicWith := Batteries.panicWith
-
--- namespace Batteries
-
--- /-- Union-find node type -/
--- structure UFNode where
---   /-- Parent of node -/
---   parent : Nat
---   /-- Rank of node -/
---   rank : Nat
-
--- namespace UnionFind
-
--- /-- Parent of a union-find node, defaults to self when the node is a root -/
--- def parentD (arr : Array UFNode) (i : Nat) : Nat :=
---   if h : i < arr.size then arr[i].parent else i
-
--- /-- Rank of a union-find node, defaults to 0 when the node is a root -/
--- def rankD (arr : Array UFNode) (i : Nat) : Nat :=
---   if h : i < arr.size then arr[i].rank else 0
-
--- theorem parentD_eq {arr : Array UFNode} {i : Nat} {h} : parentD arr i = arr[i].parent := dif_pos _
+/- Commented out entire file on nightly-2024-11-12.
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Batteries.Tactic.Alias
+import Batteries.Tactic.Lint.Misc
+import Batteries.Tactic.SeqFocus
+import Batteries.Util.Panic
+import Batteries.Data.Array.Lemmas
+
+@[deprecated (since := "2024-10-05")]
+protected alias Batteries.UnionFind.panicWith := Batteries.panicWith
+
+namespace Batteries
+
+/-- Union-find node type -/
+structure UFNode where
+  /-- Parent of node -/
+  parent : Nat
+  /-- Rank of node -/
+  rank : Nat
+
+namespace UnionFind
+
+/-- Parent of a union-find node, defaults to self when the node is a root -/
+def parentD (arr : Array UFNode) (i : Nat) : Nat :=
+  if h : i < arr.size then arr[i].parent else i
+
+/-- Rank of a union-find node, defaults to 0 when the node is a root -/
+def rankD (arr : Array UFNode) (i : Nat) : Nat :=
+  if h : i < arr.size then arr[i].rank else 0
+
+theorem parentD_eq {arr : Array UFNode} {i : Nat} {h} : parentD arr i = arr[i].parent := dif_pos _
+
+theorem parentD_eq' {arr : Array UFNode} {i} (h) :
+    parentD arr i = arr[i].parent := dif_pos _
 
--- theorem parentD_eq' {arr : Array UFNode} {i} (h) :
---     parentD arr i = arr[i].parent := dif_pos _
+theorem rankD_eq {arr : Array UFNode} {i : Fin arr.size} : rankD arr i = arr[i].rank := dif_pos _
+
+theorem rankD_eq' {arr : Array UFNode} {i} (h) : rankD arr i = arr[i].rank := dif_pos _
 
--- theorem rankD_eq {arr : Array UFNode} {i : Fin arr.size} : rankD arr i = arr[i].rank := dif_pos _
-
--- theorem rankD_eq' {arr : Array UFNode} {i} (h) : rankD arr i = arr[i].rank := dif_pos _
-
--- theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·)
-
--- theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size :=
---   Decidable.not_imp_comm.1 parentD_of_not_lt
-
--- theorem parentD_set {arr : Array UFNode} {x v i h} :
---     parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
---   rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD]
---   split
---   · split <;> simp_all
---   · split <;> [(subst i; cases ‹¬_› h); rfl]
-
--- theorem rankD_set {arr : Array UFNode} {x v i h} :
---     rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by
---   rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD]
---   split
---   · split <;> simp_all
---   · split <;> [(subst i; cases ‹¬_› h); rfl]
-
--- end UnionFind
-
--- open UnionFind
-
--- /-- ### Union-find data structure
-
--- The `UnionFind` structure is an implementation of disjoint-set data structure
--- that uses path compression to make the primary operations run in amortized
--- nearly linear time. The nodes of a `UnionFind` structure `s` are natural
--- numbers smaller than `s.size`. The structure associates with a canonical
--- representative from its equivalence class. The structure can be extended
--- using the `push` operation and equivalence classes can be updated using the
--- `union` operation.
-
--- The main operations for `UnionFind` are:
-
--- * `empty`/`mkEmpty` are used to create a new empty structure.
--- * `size` returns the size of the data structure.
--- * `push` adds a new node to a structure, unlinked to any other node.
--- * `union` links two nodes of the data structure, joining their equivalence
---   classes, and performs path compression.
--- * `find` returns the canonical representative of a node and updates the data
---   structure using path compression.
--- * `root` returns the canonical representative of a node without altering the
---   data structure.
--- * `checkEquiv` checks whether two nodes have the same canonical representative
---   and updates the structure using path compression.
-
--- Most use cases should prefer `find` over `root` to benefit from the speedup from path-compression.
-
--- The main operations use `Fin s.size` to represent nodes of the union-find structure.
--- Some alternatives are provided:
-
--- * `unionN`, `findN`, `rootN`, `checkEquivN` use `Fin n` with a proof that `n = s.size`.
--- * `union!`, `find!`, `root!`, `checkEquiv!` use `Nat` and panic when the indices are out of bounds.
--- * `findD`, `rootD`, `checkEquivD` use `Nat` and treat out of bound indices as isolated nodes.
-
--- The noncomputable relation `UnionFind.Equiv` is provided to use the equivalence relation from a
--- `UnionFind` structure in the context of proofs.
--- -/
--- structure UnionFind where
---   /-- Array of union-find nodes -/
---   arr : Array UFNode
---   /-- Validity for parent nodes -/
---   parentD_lt : ∀ {i}, i < arr.size → parentD arr i < arr.size
---   /-- Validity for rank -/
---   rankD_lt : ∀ {i}, parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
-
--- namespace UnionFind
-
--- /-- Size of union-find structure. -/
--- @[inline] abbrev size (self : UnionFind) := self.arr.size
-
--- /-- Create an empty union-find structure with specific capacity -/
--- def mkEmpty (c : Nat) : UnionFind where
---   arr := Array.mkEmpty c
---   parentD_lt := nofun
---   rankD_lt := nofun
-
--- /-- Empty union-find structure -/
--- def empty := mkEmpty 0
-
--- instance : EmptyCollection UnionFind := ⟨.empty⟩
-
--- /-- Parent of union-find node -/
--- abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
-
--- theorem parent'_lt (self : UnionFind) (i : Nat) (h) :
---     self.arr[i].parent < self.size := by
---   simp [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList, h]
-
--- theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by
---   simp only [parentD]; split <;> simp only [*, parent'_lt]
-
--- /-- Rank of union-find node -/
--- abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
-
--- theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i →
---     self.rank i < self.rank (self.parent i) := by simpa only [rank] using self.rankD_lt
-
--- theorem rank'_lt (self : UnionFind) (i : Fin self.size) : (self.arr[i]).parent ≠ i →
---     self.rank i < self.rank (self.arr[i]).parent := by
---   simpa only [← parentD_eq] using self.rankD_lt
-
--- /-- Maximum rank of nodes in a union-find structure -/
--- noncomputable def rankMax (self : UnionFind) := self.arr.foldr (max ·.rank) 0 + 1
-
--- theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) :
---     (self.arr[i]).rank < self.rankMax := by
---   let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
---     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
---     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
---   simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList]
---   exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2)
-
--- theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
---     rankD self.arr i < self.rankMax := by
---   simp [rankD]; split <;> [apply rank'_lt_rankMax; apply Nat.succ_pos]
-
--- theorem lt_rankMax (self : UnionFind) (i : Nat) : self.rank i < self.rankMax := rankD_lt_rankMax ..
-
--- theorem push_rankD (arr : Array UFNode) : rankD (arr.push ⟨arr.size, 0⟩) i = rankD arr i := by
---   simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
---   split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
-
--- theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩) i = parentD arr i := by
---   simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
---   split <;> split <;> try simp
---   · exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
---   · cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
-
--- /-- Add a new node to a union-find structure, unlinked with any other nodes -/
--- def push (self : UnionFind) : UnionFind where
---   arr := self.arr.push ⟨self.arr.size, 0⟩
---   parentD_lt {i} := by
---     simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem]
---     split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt _); exact id]
---   rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt
-
--- /-- Root of a union-find node. -/
--- def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
---   let y := (self.arr[x]).parent
---   if h : y = x then
---     x
---   else
---     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
---     self.root ⟨y, self.parent'_lt x⟩
--- termination_by self.rankMax - self.rank x
-
--- @[inherit_doc root]
--- def rootN (self : UnionFind) (x : Fin n) (h : n = self.size) : Fin n :=
---   match n, h with | _, rfl => self.root x
-
--- /-- Root of a union-find node. Panics if index is out of bounds. -/
--- def root! (self : UnionFind) (x : Nat) : Nat :=
---   if h : x < self.size then self.root ⟨x, h⟩ else panicWith x "index out of bounds"
-
--- /-- Root of a union-find node. Returns input if index is out of bounds. -/
--- def rootD (self : UnionFind) (x : Nat) : Nat :=
---   if h : x < self.size then self.root ⟨x, h⟩ else x
-
--- @[nolint unusedHavesSuffices]
--- theorem parent_root (self : UnionFind) (x : Fin self.size) :
---     (self.arr[self.root x]).parent = self.root x := by
---   rw [root]; split <;> [assumption; skip]
---   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
---   apply parent_root
--- termination_by self.rankMax - self.rank x
-
--- theorem parent_rootD (self : UnionFind) (x : Nat) :
---     self.parent (self.rootD x) = self.rootD x := by
---   rw [rootD]
---   split
---   · simp [parentD, parent_root, -Array.get_eq_getElem]
---   · simp [parentD_of_not_lt, *]
-
--- @[nolint unusedHavesSuffices]
--- theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
---   simp only [rootD, Array.length_toList, parent_lt]
---   split
---   · simp only [parentD, ↓reduceDIte, *]
---     (conv => rhs; rw [root]); split
---     · rw [root, dif_pos] <;> simp_all
---     · simp
---   · simp only [not_false_eq_true, parentD_of_not_lt, *]
-
--- theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x < self.size := by
---   simp only [rootD, Array.length_toList]; split <;> simp [*]
-
--- @[nolint unusedHavesSuffices]
--- theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by
---   refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩
---   rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
-
--- theorem rootD_rootD {self : UnionFind} {x : Nat} : self.rootD (self.rootD x) = self.rootD x :=
---   rootD_eq_self.2 (parent_rootD ..)
-
--- theorem rootD_ext {m1 m2 : UnionFind}
---     (H : ∀ x, m1.parent x = m2.parent x) {x} : m1.rootD x = m2.rootD x := by
---   if h : m2.parent x = x then
---     rw [rootD_eq_self.2 h, rootD_eq_self.2 ((H _).trans h)]
---   else
---     have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
---     rw [← rootD_parent, H, rootD_ext H, rootD_parent]
--- termination_by m2.rankMax - m2.rank x
-
--- theorem le_rank_root {self : UnionFind} {x : Nat} : self.rank x ≤ self.rank (self.rootD x) := by
---   if h : self.parent x = x then
---     rw [rootD_eq_self.2 h]; exact Nat.le_refl ..
---   else
---     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
---     rw [← rootD_parent]
---     exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
--- termination_by self.rankMax - self.rank x
-
--- theorem lt_rank_root {self : UnionFind} {x : Nat} :
---     self.rank x < self.rank (self.rootD x) ↔ self.parent x ≠ x := by
---   refine ⟨fun h h' => Nat.ne_of_lt h (by rw [rootD_eq_self.2 h']), fun h => ?_⟩
---   rw [← rootD_parent]
---   exact Nat.lt_of_lt_of_le (self.rank_lt h) le_rank_root
-
--- /-- Auxiliary data structure for find operation -/
--- structure FindAux (n : Nat) where
---   /-- Array of nodes -/
---   s : Array UFNode
---   /-- Index of root node -/
---   root : Fin n
---   /-- Size requirement -/
---   size_eq : s.size = n
-
--- /-- Auxiliary function for find operation -/
--- def findAux (self : UnionFind) (x : Fin self.size) : FindAux self.size :=
---   let y := self.arr[x].parent
---   if h : y = x then
---     ⟨self.arr, x, rfl⟩
---   else
---     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
---     let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt x⟩
---     ⟨arr₁.modify x fun s => { s with parent := root }, root, by simp [H]⟩
--- termination_by self.rankMax - self.rank x
-
--- @[nolint unusedHavesSuffices]
--- theorem findAux_root {self : UnionFind} {x : Fin self.size} :
---     (findAux self x).root = self.root x := by
---   rw [findAux, root]
---   simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]
---   split <;> simp only
---   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
---   exact findAux_root
--- termination_by self.rankMax - self.rank x
-
--- @[nolint unusedHavesSuffices]
--- theorem findAux_s {self : UnionFind} {x : Fin self.size} :
---     (findAux self x).s = if self.arr[x].parent = x then self.arr else
---       (self.findAux ⟨_, self.parent'_lt x⟩).s.modify x fun s =>
---         { s with parent := self.rootD x } := by
---   rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
---   · rw [findAux]; split <;> rfl
---   · rw [← rootD_parent, parent, parentD_eq]
---     simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]
---     apply dif_pos
---     exact parent'_lt ..
-
--- set_option linter.deprecated false in
--- theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
---     rankD (findAux self x).s i = self.rank i := by
---   if h : i < self.size then
---     rw [findAux_s]; split <;> [rfl; skip]
---     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
---     have := lt_of_parentD (by rwa [parentD_eq])
---     rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify]
---     split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
---   else
---     simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
---     rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
--- termination_by self.rankMax - self.rank x
-
--- set_option linter.deprecated false in
--- theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
---     parentD (findAux self x).s i =
---     if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt x⟩).s i := by
---   rw [findAux_s]; split <;> [split; skip]
---   · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]
---   · rw [findAux_s]; simp [*, -Array.get_eq_getElem]
---   · next h =>
---     rw [parentD]; split <;> rename_i h'
---     · rw [Array.get_modify (by simpa using h')]
---       simp only [Array.data_length, @eq_comm _ i]
---       split <;> simp [← parentD_eq, -Array.get_eq_getElem]
---     · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
---       rw [parentD, dif_neg]; simpa using h'
-
--- theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} :
---     parentD (findAux self x).s (self.rootD x) = self.rootD x := by
---   rw [parentD_findAux]; split <;> [rfl; rename_i h]
---   rw [rootD_eq_self, parent, parentD_eq] at h
---   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
---   rw [← rootD_parent, parent, parentD_eq]
---   exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt x⟩)
--- termination_by self.rankMax - self.rank x
-
--- theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) :
---     parentD (findAux self x).s i < self.size := by
---   if h' : self.arr[x].parent = x then
---     rw [findAux_s, if_pos h']; apply self.parentD_lt h
---   else
---     rw [parentD_findAux]
---     split
---     · simp [rootD_lt]
---     · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
---       apply parentD_findAux_lt h
--- termination_by self.rankMax - self.rank x
-
--- theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
---     parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨
---     parentD (findAux self x).s i = self.parent i := by
---   if h' : self.arr[x].parent = x then
---     rw [findAux_s, if_pos h']; exact .inr rfl
---   else
---     rw [parentD_findAux]
---     split
---     · simp [*]
---     · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
---       exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
---         simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
--- termination_by self.rankMax - self.rank x
-
--- theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
---     parentD (findAux self x).s i ≠ i →
---     self.rank i < self.rank (parentD (findAux self x).s i) := by
---   if h' : self.arr[x].parent = x then
---     rw [findAux_s, if_pos h']; apply self.rank_lt
---   else
---     rw [parentD_findAux]; split <;> rename_i h <;> intro h'
---     · subst i; rwa [lt_rank_root, Ne, ← rootD_eq_self]
---     · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
---       apply lt_rankD_findAux h'
--- termination_by self.rankMax - self.rank x
-
--- /-- Find root of a union-find node, updating the structure using path compression. -/
--- def find (self : UnionFind) (x : Fin self.size) :
---     (s : UnionFind) × {_root : Fin s.size // s.size = self.size} :=
---   let r := self.findAux x
---   { 1.arr := r.s
---     2.1.val := r.root
---     1.parentD_lt := fun h => by
---       simp only [Array.length_toList, FindAux.size_eq] at *
---       exact parentD_findAux_lt h
---     1.rankD_lt := fun h => by rw [rankD_findAux, rankD_findAux]; exact lt_rankD_findAux h
---     2.1.isLt := show _ < r.s.size by rw [r.size_eq]; exact r.root.2
---     2.2 := by simp [size, r.size_eq] }
-
--- @[inherit_doc find]
--- def findN (self : UnionFind) (x : Fin n) (h : n = self.size) : UnionFind × Fin n :=
---   match n, h with | _, rfl => match self.find x with | ⟨s, r, h⟩ => (s, Fin.cast h r)
-
--- /-- Find root of a union-find node, updating the structure using path compression.
---   Panics if index is out of bounds. -/
--- def find! (self : UnionFind) (x : Nat) : UnionFind × Nat :=
---   if h : x < self.size then
---     match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
---   else
---     panicWith (self, x) "index out of bounds"
-
--- /-- Find root of a union-find node, updating the structure using path compression.
---   Returns inputs unchanged when index is out of bounds. -/
--- def findD (self : UnionFind) (x : Nat) : UnionFind × Nat :=
---   if h : x < self.size then
---     match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
---   else
---     (self, x)
-
--- @[simp] theorem find_size (self : UnionFind) (x : Fin self.size) :
---     (self.find x).1.size = self.size := by simp [find, size, FindAux.size_eq]
-
--- @[simp] theorem find_root_2 (self : UnionFind) (x : Fin self.size) :
---     (self.find x).2.1.1 = self.rootD x := by simp [find, findAux_root, rootD]
-
--- @[simp] theorem find_parent_1 (self : UnionFind) (x : Fin self.size) :
---     (self.find x).1.parent x = self.rootD x := by
---   simp only [parent, Array.length_toList, find]
---   rw [parentD_findAux, if_pos rfl]
-
--- theorem find_parent_or (self : UnionFind) (x : Fin self.size) (i) :
---     (self.find x).1.parent i = self.rootD i ∧ self.rootD i = self.rootD x ∨
---     (self.find x).1.parent i = self.parent i := parentD_findAux_or ..
-
--- @[simp] theorem find_root_1 (self : UnionFind) (x : Fin self.size) (i : Nat) :
---     (self.find x).1.rootD i = self.rootD i := by
---   if h : (self.find x).1.parent i = i then
---     rw [rootD_eq_self.2 h]
---     obtain ⟨h1, _⟩ | h1 := find_parent_or self x i <;> rw [h1] at h
---     · rw [h]
---     · rw [rootD_eq_self.2 h]
---   else
---     have := Nat.sub_lt_sub_left ((self.find x).1.lt_rankMax _) ((self.find x).1.rank_lt h)
---     rw [← rootD_parent, find_root_1 self x ((self.find x).1.parent i)]
---     obtain ⟨h1, _⟩ | h1 := find_parent_or self x i
---     · rw [h1, rootD_rootD]
---     · rw [h1, rootD_parent]
--- termination_by  (self.find x).1.rankMax - (self.find x).1.rank i
--- decreasing_by exact this -- why is this needed? It is way slower without it
-
--- /-- Link two union-find nodes -/
--- def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
---   if x.1 = y then
---     self
---   else
---     let nx := self[x]
---     let ny := self[y]
---     if ny.rank < nx.rank then
---       self.set y {ny with parent := x}
---     else
---       let arr₁ := self.set x {nx with parent := y}
---       if nx.rank = ny.rank then
---         arr₁.set y {ny with rank := ny.rank + 1} (by simp [arr₁])
---       else
---         arr₁
-
--- theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
---     (hroot : arr[x].rank < arr[y].rank ∨ arr[y].parent = y)
---     (H : arr[x].rank ≤ arr[y].rank) {i : Nat}
---     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
---     (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
---     (hR : ∀ {i}, rankD arr' i =
---       if y.1 = i ∧ arr[x].rank = arr[y].rank then
---         arr[y].rank + 1
---       else rankD arr i) :
---     ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by
---   simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
---     split <;> rename_i h₂ <;> intro h
---   · simp [h₂] at h
---   · simp only [rankD_eq, Array.get_eq_getElem]
---     split <;> rename_i h₃
---     · rw [← h₃]; apply Nat.lt_succ_self
---     · exact Nat.lt_of_le_of_ne H h₃
---   · cases h₂.1
---     simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot
---     simp only [hroot, parentD_eq, not_true_eq_false] at h
---   · have := rankD_lt h
---     split <;> rename_i h₃
---     · rw [← rankD_eq, h₃.1]; exact Nat.lt_succ_of_lt this
---     · exact this
-
--- theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
---     (h : arr[x].rank < arr[y].rank) {i : Nat}
---     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) :
---     let arr' := arr.set x ⟨y, arr[x].rank⟩
---     parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
---   setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set
---     (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem])
-
--- @[simp] theorem linkAux_size : (linkAux self x y).size = self.size := by
---   simp only [linkAux, Array.get_eq_getElem]
---   split <;> [rfl; split] <;> [skip; split] <;> simp
-
--- /-- Link a union-find node to a root node. -/
--- def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) : UnionFind where
---   arr := linkAux self.arr x y
---   parentD_lt h := by
---     simp only [Array.length_toList, linkAux_size] at *
---     simp only [linkAux, Array.get_eq_getElem]
---     split <;> [skip; split <;> [skip; split]]
---     · exact self.parentD_lt h
---     · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h]
---     · rw [parentD_set]; split
---       · exact self.parent'_lt _
---       · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
---     · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
---   rankD_lt := by
---     rw [parent, parentD_eq] at yroot
---     simp only [linkAux, Array.get_eq_getElem, ne_eq]
---     split <;> [skip; split <;> [skip; split]]
---     · exact self.rankD_lt
---     · exact setParent_rankD_lt ‹_› self.rankD_lt
---     · refine setParentBump_rankD_lt (.inr yroot) (Nat.le_of_eq ‹_›) self.rankD_lt (by
---         simp only [parentD_set, ite_eq_right_iff]
---         rintro rfl
---         simp [*, parentD_eq]) fun {i} => ?_
---       simp only [rankD_set, Fin.eta, Array.get_eq_getElem]
---       split
---       · simp_all
---       · simp_all only [Array.get_eq_getElem, Array.length_toList, Nat.lt_irrefl, not_false_eq_true,
---           and_true, ite_false, ite_eq_right_iff]
---         rintro rfl
---         simp [rankD_eq, *]
---     · exact setParent_rankD_lt (Nat.lt_of_le_of_ne (Nat.not_lt.1 ‹_›) ‹_›) self.rankD_lt
-
--- @[inherit_doc link]
--- def linkN (self : UnionFind) (x y : Fin n) (yroot : self.parent y = y) (h : n = self.size) :
---     UnionFind := match n, h with | _, rfl => self.link x y yroot
-
--- /-- Link a union-find node to a root node. Panics if either index is out of bounds. -/
--- def link! (self : UnionFind) (x y : Nat) (yroot : self.parent y = y) : UnionFind :=
---   if h : x < self.size ∧ y < self.size then
---     self.link ⟨x, h.1⟩ ⟨y, h.2⟩ yroot
---   else
---     panicWith self "index out of bounds"
-
--- /-- Link two union-find nodes, uniting their respective classes. -/
--- def union (self : UnionFind) (x y : Fin self.size) : UnionFind :=
---   let ⟨self₁, rx, ex⟩ := self.find x
---   have hy := by rw [ex]; exact y.2
---   match eq : self₁.find ⟨y, hy⟩ with
---   | ⟨self₂, ry, ey⟩ =>
---     self₂.link ⟨rx, by rw [ey]; exact rx.2⟩ ry <| by
---       have := find_root_1 self₁ ⟨y, hy⟩ (⟨y, hy⟩ : Fin _)
---       rw [← find_root_2, eq] at this; simp at this
---       rw [← this, parent_rootD]
-
--- @[inherit_doc union]
--- def unionN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind :=
---   match n, h with | _, rfl => self.union x y
-
--- /-- Link two union-find nodes, uniting their respective classes.
--- Panics if either index is out of bounds. -/
--- def union! (self : UnionFind) (x y : Nat) : UnionFind :=
---   if h : x < self.size ∧ y < self.size then
---     self.union ⟨x, h.1⟩ ⟨y, h.2⟩
---   else
---     panicWith self "index out of bounds"
-
--- /-- Check whether two union-find nodes are equivalent, updating structure using path compression. -/
--- def checkEquiv (self : UnionFind) (x y : Fin self.size) : UnionFind × Bool :=
---   let ⟨s, ⟨r₁, _⟩, h⟩ := self.find x
---   let ⟨s, ⟨r₂, _⟩, _⟩ := s.find (h ▸ y)
---   (s, r₁ == r₂)
-
--- @[inherit_doc checkEquiv]
--- def checkEquivN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind × Bool :=
---   match n, h with | _, rfl => self.checkEquiv x y
-
--- /-- Check whether two union-find nodes are equivalent, updating structure using path compression.
--- Panics if either index is out of bounds. -/
--- def checkEquiv! (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
---   if h : x < self.size ∧ y < self.size then
---     self.checkEquiv ⟨x, h.1⟩ ⟨y, h.2⟩
---   else
---     panicWith (self, false) "index out of bounds"
-
--- /-- Check whether two union-find nodes are equivalent with path compression,
--- returns `x == y` if either index is out of bounds -/
--- def checkEquivD (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
---   let (s, x) := self.findD x
---   let (s, y) := s.findD y
---   (s, x == y)
-
--- /-- Equivalence relation from a `UnionFind` structure -/
--- def Equiv (self : UnionFind) (a b : Nat) : Prop := self.rootD a = self.rootD b
+theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·)
+
+theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size :=
+  Decidable.not_imp_comm.1 parentD_of_not_lt
+
+theorem parentD_set {arr : Array UFNode} {x v i h} :
+    parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
+  rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD]
+  split
+  · split <;> simp_all
+  · split <;> [(subst i; cases ‹¬_› h); rfl]
+
+theorem rankD_set {arr : Array UFNode} {x v i h} :
+    rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by
+  rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD]
+  split
+  · split <;> simp_all
+  · split <;> [(subst i; cases ‹¬_› h); rfl]
+
+end UnionFind
+
+open UnionFind
+
+/-- ### Union-find data structure
+
+The `UnionFind` structure is an implementation of disjoint-set data structure
+that uses path compression to make the primary operations run in amortized
+nearly linear time. The nodes of a `UnionFind` structure `s` are natural
+numbers smaller than `s.size`. The structure associates with a canonical
+representative from its equivalence class. The structure can be extended
+using the `push` operation and equivalence classes can be updated using the
+`union` operation.
+
+The main operations for `UnionFind` are:
+
+* `empty`/`mkEmpty` are used to create a new empty structure.
+* `size` returns the size of the data structure.
+* `push` adds a new node to a structure, unlinked to any other node.
+* `union` links two nodes of the data structure, joining their equivalence
+  classes, and performs path compression.
+* `find` returns the canonical representative of a node and updates the data
+  structure using path compression.
+* `root` returns the canonical representative of a node without altering the
+  data structure.
+* `checkEquiv` checks whether two nodes have the same canonical representative
+  and updates the structure using path compression.
+
+Most use cases should prefer `find` over `root` to benefit from the speedup from path-compression.
+
+The main operations use `Fin s.size` to represent nodes of the union-find structure.
+Some alternatives are provided:
+
+* `unionN`, `findN`, `rootN`, `checkEquivN` use `Fin n` with a proof that `n = s.size`.
+* `union!`, `find!`, `root!`, `checkEquiv!` use `Nat` and panic when the indices are out of bounds.
+* `findD`, `rootD`, `checkEquivD` use `Nat` and treat out of bound indices as isolated nodes.
+
+The noncomputable relation `UnionFind.Equiv` is provided to use the equivalence relation from a
+`UnionFind` structure in the context of proofs.
+-/
+structure UnionFind where
+  /-- Array of union-find nodes -/
+  arr : Array UFNode
+  /-- Validity for parent nodes -/
+  parentD_lt : ∀ {i}, i < arr.size → parentD arr i < arr.size
+  /-- Validity for rank -/
+  rankD_lt : ∀ {i}, parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
+
+namespace UnionFind
+
+/-- Size of union-find structure. -/
+@[inline] abbrev size (self : UnionFind) := self.arr.size
+
+/-- Create an empty union-find structure with specific capacity -/
+def mkEmpty (c : Nat) : UnionFind where
+  arr := Array.mkEmpty c
+  parentD_lt := nofun
+  rankD_lt := nofun
+
+/-- Empty union-find structure -/
+def empty := mkEmpty 0
+
+instance : EmptyCollection UnionFind := ⟨.empty⟩
+
+/-- Parent of union-find node -/
+abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
+
+theorem parent'_lt (self : UnionFind) (i : Nat) (h) :
+    self.arr[i].parent < self.size := by
+  simp [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList, h]
+
+theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by
+  simp only [parentD]; split <;> simp only [*, parent'_lt]
+
+/-- Rank of union-find node -/
+abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
+
+theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i →
+    self.rank i < self.rank (self.parent i) := by simpa only [rank] using self.rankD_lt
+
+theorem rank'_lt (self : UnionFind) (i : Fin self.size) : (self.arr[i]).parent ≠ i →
+    self.rank i < self.rank (self.arr[i]).parent := by
+  simpa only [← parentD_eq] using self.rankD_lt
+
+/-- Maximum rank of nodes in a union-find structure -/
+noncomputable def rankMax (self : UnionFind) := self.arr.foldr (max ·.rank) 0 + 1
+
+theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) :
+    (self.arr[i]).rank < self.rankMax := by
+  let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
+    | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
+    | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
+  simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList]
+  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2)
+
+theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
+    rankD self.arr i < self.rankMax := by
+  simp [rankD]; split <;> [apply rank'_lt_rankMax; apply Nat.succ_pos]
+
+theorem lt_rankMax (self : UnionFind) (i : Nat) : self.rank i < self.rankMax := rankD_lt_rankMax ..
+
+theorem push_rankD (arr : Array UFNode) : rankD (arr.push ⟨arr.size, 0⟩) i = rankD arr i := by
+  simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
+  split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
+
+theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩) i = parentD arr i := by
+  simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
+  split <;> split <;> try simp
+  · exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
+  · cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
+
+/-- Add a new node to a union-find structure, unlinked with any other nodes -/
+def push (self : UnionFind) : UnionFind where
+  arr := self.arr.push ⟨self.arr.size, 0⟩
+  parentD_lt {i} := by
+    simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem]
+    split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt _); exact id]
+  rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt
+
+/-- Root of a union-find node. -/
+def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
+  let y := (self.arr[x]).parent
+  if h : y = x then
+    x
+  else
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
+    self.root ⟨y, self.parent'_lt x⟩
+termination_by self.rankMax - self.rank x
+
+@[inherit_doc root]
+def rootN (self : UnionFind) (x : Fin n) (h : n = self.size) : Fin n :=
+  match n, h with | _, rfl => self.root x
+
+/-- Root of a union-find node. Panics if index is out of bounds. -/
+def root! (self : UnionFind) (x : Nat) : Nat :=
+  if h : x < self.size then self.root ⟨x, h⟩ else panicWith x "index out of bounds"
+
+/-- Root of a union-find node. Returns input if index is out of bounds. -/
+def rootD (self : UnionFind) (x : Nat) : Nat :=
+  if h : x < self.size then self.root ⟨x, h⟩ else x
+
+@[nolint unusedHavesSuffices]
+theorem parent_root (self : UnionFind) (x : Fin self.size) :
+    (self.arr[self.root x]).parent = self.root x := by
+  rw [root]; split <;> [assumption; skip]
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+  apply parent_root
+termination_by self.rankMax - self.rank x
+
+theorem parent_rootD (self : UnionFind) (x : Nat) :
+    self.parent (self.rootD x) = self.rootD x := by
+  rw [rootD]
+  split
+  · simp [parentD, parent_root, -Array.get_eq_getElem]
+  · simp [parentD_of_not_lt, *]
+
+@[nolint unusedHavesSuffices]
+theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
+  simp only [rootD, Array.length_toList, parent_lt]
+  split
+  · simp only [parentD, ↓reduceDIte, *]
+    (conv => rhs; rw [root]); split
+    · rw [root, dif_pos] <;> simp_all
+    · simp
+  · simp only [not_false_eq_true, parentD_of_not_lt, *]
+
+theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x < self.size := by
+  simp only [rootD, Array.length_toList]; split <;> simp [*]
+
+@[nolint unusedHavesSuffices]
+theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by
+  refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩
+  rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
+
+theorem rootD_rootD {self : UnionFind} {x : Nat} : self.rootD (self.rootD x) = self.rootD x :=
+  rootD_eq_self.2 (parent_rootD ..)
+
+theorem rootD_ext {m1 m2 : UnionFind}
+    (H : ∀ x, m1.parent x = m2.parent x) {x} : m1.rootD x = m2.rootD x := by
+  if h : m2.parent x = x then
+    rw [rootD_eq_self.2 h, rootD_eq_self.2 ((H _).trans h)]
+  else
+    have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
+    rw [← rootD_parent, H, rootD_ext H, rootD_parent]
+termination_by m2.rankMax - m2.rank x
+
+theorem le_rank_root {self : UnionFind} {x : Nat} : self.rank x ≤ self.rank (self.rootD x) := by
+  if h : self.parent x = x then
+    rw [rootD_eq_self.2 h]; exact Nat.le_refl ..
+  else
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
+    rw [← rootD_parent]
+    exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
+termination_by self.rankMax - self.rank x
+
+theorem lt_rank_root {self : UnionFind} {x : Nat} :
+    self.rank x < self.rank (self.rootD x) ↔ self.parent x ≠ x := by
+  refine ⟨fun h h' => Nat.ne_of_lt h (by rw [rootD_eq_self.2 h']), fun h => ?_⟩
+  rw [← rootD_parent]
+  exact Nat.lt_of_lt_of_le (self.rank_lt h) le_rank_root
+
+/-- Auxiliary data structure for find operation -/
+structure FindAux (n : Nat) where
+  /-- Array of nodes -/
+  s : Array UFNode
+  /-- Index of root node -/
+  root : Fin n
+  /-- Size requirement -/
+  size_eq : s.size = n
+
+/-- Auxiliary function for find operation -/
+def findAux (self : UnionFind) (x : Fin self.size) : FindAux self.size :=
+  let y := self.arr[x].parent
+  if h : y = x then
+    ⟨self.arr, x, rfl⟩
+  else
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
+    let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt x⟩
+    ⟨arr₁.modify x fun s => { s with parent := root }, root, by simp [H]⟩
+termination_by self.rankMax - self.rank x
+
+@[nolint unusedHavesSuffices]
+theorem findAux_root {self : UnionFind} {x : Fin self.size} :
+    (findAux self x).root = self.root x := by
+  rw [findAux, root]
+  simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]
+  split <;> simp only
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+  exact findAux_root
+termination_by self.rankMax - self.rank x
+
+@[nolint unusedHavesSuffices]
+theorem findAux_s {self : UnionFind} {x : Fin self.size} :
+    (findAux self x).s = if self.arr[x].parent = x then self.arr else
+      (self.findAux ⟨_, self.parent'_lt x⟩).s.modify x fun s =>
+        { s with parent := self.rootD x } := by
+  rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
+  · rw [findAux]; split <;> rfl
+  · rw [← rootD_parent, parent, parentD_eq]
+    simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]
+    apply dif_pos
+    exact parent'_lt ..
+
+set_option linter.deprecated false in
+theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
+    rankD (findAux self x).s i = self.rank i := by
+  if h : i < self.size then
+    rw [findAux_s]; split <;> [rfl; skip]
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+    have := lt_of_parentD (by rwa [parentD_eq])
+    rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify]
+    split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
+  else
+    simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
+    rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
+termination_by self.rankMax - self.rank x
+
+set_option linter.deprecated false in
+theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
+    parentD (findAux self x).s i =
+    if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt x⟩).s i := by
+  rw [findAux_s]; split <;> [split; skip]
+  · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]
+  · rw [findAux_s]; simp [*, -Array.get_eq_getElem]
+  · next h =>
+    rw [parentD]; split <;> rename_i h'
+    · rw [Array.get_modify (by simpa using h')]
+      simp only [Array.data_length, @eq_comm _ i]
+      split <;> simp [← parentD_eq, -Array.get_eq_getElem]
+    · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
+      rw [parentD, dif_neg]; simpa using h'
+
+theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} :
+    parentD (findAux self x).s (self.rootD x) = self.rootD x := by
+  rw [parentD_findAux]; split <;> [rfl; rename_i h]
+  rw [rootD_eq_self, parent, parentD_eq] at h
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+  rw [← rootD_parent, parent, parentD_eq]
+  exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt x⟩)
+termination_by self.rankMax - self.rank x
+
+theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) :
+    parentD (findAux self x).s i < self.size := by
+  if h' : self.arr[x].parent = x then
+    rw [findAux_s, if_pos h']; apply self.parentD_lt h
+  else
+    rw [parentD_findAux]
+    split
+    · simp [rootD_lt]
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+      apply parentD_findAux_lt h
+termination_by self.rankMax - self.rank x
+
+theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
+    parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨
+    parentD (findAux self x).s i = self.parent i := by
+  if h' : self.arr[x].parent = x then
+    rw [findAux_s, if_pos h']; exact .inr rfl
+  else
+    rw [parentD_findAux]
+    split
+    · simp [*]
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+      exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
+        simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
+termination_by self.rankMax - self.rank x
+
+theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
+    parentD (findAux self x).s i ≠ i →
+    self.rank i < self.rank (parentD (findAux self x).s i) := by
+  if h' : self.arr[x].parent = x then
+    rw [findAux_s, if_pos h']; apply self.rank_lt
+  else
+    rw [parentD_findAux]; split <;> rename_i h <;> intro h'
+    · subst i; rwa [lt_rank_root, Ne, ← rootD_eq_self]
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+      apply lt_rankD_findAux h'
+termination_by self.rankMax - self.rank x
+
+/-- Find root of a union-find node, updating the structure using path compression. -/
+def find (self : UnionFind) (x : Fin self.size) :
+    (s : UnionFind) × {_root : Fin s.size // s.size = self.size} :=
+  let r := self.findAux x
+  { 1.arr := r.s
+    2.1.val := r.root
+    1.parentD_lt := fun h => by
+      simp only [Array.length_toList, FindAux.size_eq] at *
+      exact parentD_findAux_lt h
+    1.rankD_lt := fun h => by rw [rankD_findAux, rankD_findAux]; exact lt_rankD_findAux h
+    2.1.isLt := show _ < r.s.size by rw [r.size_eq]; exact r.root.2
+    2.2 := by simp [size, r.size_eq] }
+
+@[inherit_doc find]
+def findN (self : UnionFind) (x : Fin n) (h : n = self.size) : UnionFind × Fin n :=
+  match n, h with | _, rfl => match self.find x with | ⟨s, r, h⟩ => (s, Fin.cast h r)
+
+/-- Find root of a union-find node, updating the structure using path compression.
+  Panics if index is out of bounds. -/
+def find! (self : UnionFind) (x : Nat) : UnionFind × Nat :=
+  if h : x < self.size then
+    match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
+  else
+    panicWith (self, x) "index out of bounds"
+
+/-- Find root of a union-find node, updating the structure using path compression.
+  Returns inputs unchanged when index is out of bounds. -/
+def findD (self : UnionFind) (x : Nat) : UnionFind × Nat :=
+  if h : x < self.size then
+    match self.find ⟨x, h⟩ with | ⟨s, r, _⟩ => (s, r)
+  else
+    (self, x)
+
+@[simp] theorem find_size (self : UnionFind) (x : Fin self.size) :
+    (self.find x).1.size = self.size := by simp [find, size, FindAux.size_eq]
+
+@[simp] theorem find_root_2 (self : UnionFind) (x : Fin self.size) :
+    (self.find x).2.1.1 = self.rootD x := by simp [find, findAux_root, rootD]
+
+@[simp] theorem find_parent_1 (self : UnionFind) (x : Fin self.size) :
+    (self.find x).1.parent x = self.rootD x := by
+  simp only [parent, Array.length_toList, find]
+  rw [parentD_findAux, if_pos rfl]
+
+theorem find_parent_or (self : UnionFind) (x : Fin self.size) (i) :
+    (self.find x).1.parent i = self.rootD i ∧ self.rootD i = self.rootD x ∨
+    (self.find x).1.parent i = self.parent i := parentD_findAux_or ..
+
+@[simp] theorem find_root_1 (self : UnionFind) (x : Fin self.size) (i : Nat) :
+    (self.find x).1.rootD i = self.rootD i := by
+  if h : (self.find x).1.parent i = i then
+    rw [rootD_eq_self.2 h]
+    obtain ⟨h1, _⟩ | h1 := find_parent_or self x i <;> rw [h1] at h
+    · rw [h]
+    · rw [rootD_eq_self.2 h]
+  else
+    have := Nat.sub_lt_sub_left ((self.find x).1.lt_rankMax _) ((self.find x).1.rank_lt h)
+    rw [← rootD_parent, find_root_1 self x ((self.find x).1.parent i)]
+    obtain ⟨h1, _⟩ | h1 := find_parent_or self x i
+    · rw [h1, rootD_rootD]
+    · rw [h1, rootD_parent]
+termination_by  (self.find x).1.rankMax - (self.find x).1.rank i
+decreasing_by exact this -- why is this needed? It is way slower without it
+
+/-- Link two union-find nodes -/
+def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
+  if x.1 = y then
+    self
+  else
+    let nx := self[x]
+    let ny := self[y]
+    if ny.rank < nx.rank then
+      self.set y {ny with parent := x}
+    else
+      let arr₁ := self.set x {nx with parent := y}
+      if nx.rank = ny.rank then
+        arr₁.set y {ny with rank := ny.rank + 1} (by simp [arr₁])
+      else
+        arr₁
+
+theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
+    (hroot : arr[x].rank < arr[y].rank ∨ arr[y].parent = y)
+    (H : arr[x].rank ≤ arr[y].rank) {i : Nat}
+    (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
+    (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
+    (hR : ∀ {i}, rankD arr' i =
+      if y.1 = i ∧ arr[x].rank = arr[y].rank then
+        arr[y].rank + 1
+      else rankD arr i) :
+    ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by
+  simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
+    split <;> rename_i h₂ <;> intro h
+  · simp [h₂] at h
+  · simp only [rankD_eq, Array.get_eq_getElem]
+    split <;> rename_i h₃
+    · rw [← h₃]; apply Nat.lt_succ_self
+    · exact Nat.lt_of_le_of_ne H h₃
+  · cases h₂.1
+    simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot
+    simp only [hroot, parentD_eq, not_true_eq_false] at h
+  · have := rankD_lt h
+    split <;> rename_i h₃
+    · rw [← rankD_eq, h₃.1]; exact Nat.lt_succ_of_lt this
+    · exact this
+
+theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
+    (h : arr[x].rank < arr[y].rank) {i : Nat}
+    (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) :
+    let arr' := arr.set x ⟨y, arr[x].rank⟩
+    parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
+  setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set
+    (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem])
+
+@[simp] theorem linkAux_size : (linkAux self x y).size = self.size := by
+  simp only [linkAux, Array.get_eq_getElem]
+  split <;> [rfl; split] <;> [skip; split] <;> simp
+
+/-- Link a union-find node to a root node. -/
+def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) : UnionFind where
+  arr := linkAux self.arr x y
+  parentD_lt h := by
+    simp only [Array.length_toList, linkAux_size] at *
+    simp only [linkAux, Array.get_eq_getElem]
+    split <;> [skip; split <;> [skip; split]]
+    · exact self.parentD_lt h
+    · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h]
+    · rw [parentD_set]; split
+      · exact self.parent'_lt _
+      · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
+    · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
+  rankD_lt := by
+    rw [parent, parentD_eq] at yroot
+    simp only [linkAux, Array.get_eq_getElem, ne_eq]
+    split <;> [skip; split <;> [skip; split]]
+    · exact self.rankD_lt
+    · exact setParent_rankD_lt ‹_› self.rankD_lt
+    · refine setParentBump_rankD_lt (.inr yroot) (Nat.le_of_eq ‹_›) self.rankD_lt (by
+        simp only [parentD_set, ite_eq_right_iff]
+        rintro rfl
+        simp [*, parentD_eq]) fun {i} => ?_
+      simp only [rankD_set, Fin.eta, Array.get_eq_getElem]
+      split
+      · simp_all
+      · simp_all only [Array.get_eq_getElem, Array.length_toList, Nat.lt_irrefl, not_false_eq_true,
+          and_true, ite_false, ite_eq_right_iff]
+        rintro rfl
+        simp [rankD_eq, *]
+    · exact setParent_rankD_lt (Nat.lt_of_le_of_ne (Nat.not_lt.1 ‹_›) ‹_›) self.rankD_lt
+
+@[inherit_doc link]
+def linkN (self : UnionFind) (x y : Fin n) (yroot : self.parent y = y) (h : n = self.size) :
+    UnionFind := match n, h with | _, rfl => self.link x y yroot
+
+/-- Link a union-find node to a root node. Panics if either index is out of bounds. -/
+def link! (self : UnionFind) (x y : Nat) (yroot : self.parent y = y) : UnionFind :=
+  if h : x < self.size ∧ y < self.size then
+    self.link ⟨x, h.1⟩ ⟨y, h.2⟩ yroot
+  else
+    panicWith self "index out of bounds"
+
+/-- Link two union-find nodes, uniting their respective classes. -/
+def union (self : UnionFind) (x y : Fin self.size) : UnionFind :=
+  let ⟨self₁, rx, ex⟩ := self.find x
+  have hy := by rw [ex]; exact y.2
+  match eq : self₁.find ⟨y, hy⟩ with
+  | ⟨self₂, ry, ey⟩ =>
+    self₂.link ⟨rx, by rw [ey]; exact rx.2⟩ ry <| by
+      have := find_root_1 self₁ ⟨y, hy⟩ (⟨y, hy⟩ : Fin _)
+      rw [← find_root_2, eq] at this; simp at this
+      rw [← this, parent_rootD]
+
+@[inherit_doc union]
+def unionN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind :=
+  match n, h with | _, rfl => self.union x y
+
+/-- Link two union-find nodes, uniting their respective classes.
+Panics if either index is out of bounds. -/
+def union! (self : UnionFind) (x y : Nat) : UnionFind :=
+  if h : x < self.size ∧ y < self.size then
+    self.union ⟨x, h.1⟩ ⟨y, h.2⟩
+  else
+    panicWith self "index out of bounds"
+
+/-- Check whether two union-find nodes are equivalent, updating structure using path compression. -/
+def checkEquiv (self : UnionFind) (x y : Fin self.size) : UnionFind × Bool :=
+  let ⟨s, ⟨r₁, _⟩, h⟩ := self.find x
+  let ⟨s, ⟨r₂, _⟩, _⟩ := s.find (h ▸ y)
+  (s, r₁ == r₂)
+
+@[inherit_doc checkEquiv]
+def checkEquivN (self : UnionFind) (x y : Fin n) (h : n = self.size) : UnionFind × Bool :=
+  match n, h with | _, rfl => self.checkEquiv x y
+
+/-- Check whether two union-find nodes are equivalent, updating structure using path compression.
+Panics if either index is out of bounds. -/
+def checkEquiv! (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
+  if h : x < self.size ∧ y < self.size then
+    self.checkEquiv ⟨x, h.1⟩ ⟨y, h.2⟩
+  else
+    panicWith (self, false) "index out of bounds"
+
+/-- Check whether two union-find nodes are equivalent with path compression,
+returns `x == y` if either index is out of bounds -/
+def checkEquivD (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
+  let (s, x) := self.findD x
+  let (s, y) := s.findD y
+  (s, x == y)
+
+/-- Equivalence relation from a `UnionFind` structure -/
+def Equiv (self : UnionFind) (a b : Nat) : Prop := self.rootD a = self.rootD b
+-/

From 1459344add1fcda957624cd8cdc30951e9071a70 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 12 Nov 2024 15:25:56 +0100
Subject: [PATCH 18/18] uncomment UnionFind

---
 Batteries/Data/UnionFind/Basic.lean  | 104 +++++-----
 Batteries/Data/UnionFind/Lemmas.lean | 278 +++++++++++++--------------
 Batteries/Data/Vector/Basic.lean     |   2 +-
 Batteries/StdDeprecations.lean       |  26 ++-
 4 files changed, 201 insertions(+), 209 deletions(-)

diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index 289fdc7d57..a607dc2284 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -1,4 +1,3 @@
-/- Commented out entire file on nightly-2024-11-12.
 /-
 Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -32,14 +31,10 @@ def parentD (arr : Array UFNode) (i : Nat) : Nat :=
 def rankD (arr : Array UFNode) (i : Nat) : Nat :=
   if h : i < arr.size then arr[i].rank else 0
 
-theorem parentD_eq {arr : Array UFNode} {i : Nat} {h} : parentD arr i = arr[i].parent := dif_pos _
-
-theorem parentD_eq' {arr : Array UFNode} {i} (h) :
+theorem parentD_eq {arr : Array UFNode} {i} (h) :
     parentD arr i = arr[i].parent := dif_pos _
 
-theorem rankD_eq {arr : Array UFNode} {i : Fin arr.size} : rankD arr i = arr[i].rank := dif_pos _
-
-theorem rankD_eq' {arr : Array UFNode} {i} (h) : rankD arr i = arr[i].rank := dif_pos _
+theorem rankD_eq {arr : Array UFNode} {i} (h) : rankD arr i = arr[i].rank := dif_pos _
 
 theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·)
 
@@ -127,8 +122,7 @@ instance : EmptyCollection UnionFind := ⟨.empty⟩
 /-- Parent of union-find node -/
 abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
 
-theorem parent'_lt (self : UnionFind) (i : Nat) (h) :
-    self.arr[i].parent < self.size := by
+theorem parent'_lt (self : UnionFind) (i : Nat) (h) : self.arr[i].parent < self.size := by
   simp [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList, h]
 
 theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by
@@ -140,20 +134,19 @@ abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
 theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i →
     self.rank i < self.rank (self.parent i) := by simpa only [rank] using self.rankD_lt
 
-theorem rank'_lt (self : UnionFind) (i : Fin self.size) : (self.arr[i]).parent ≠ i →
+theorem rank'_lt (self : UnionFind) (i h) : self.arr[i].parent ≠ i →
     self.rank i < self.rank (self.arr[i]).parent := by
   simpa only [← parentD_eq] using self.rankD_lt
 
 /-- Maximum rank of nodes in a union-find structure -/
 noncomputable def rankMax (self : UnionFind) := self.arr.foldr (max ·.rank) 0 + 1
 
-theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) :
-    (self.arr[i]).rank < self.rankMax := by
+theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank < self.rankMax := by
   let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
   simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList]
-  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2)
+  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i h)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by
@@ -176,17 +169,17 @@ def push (self : UnionFind) : UnionFind where
   arr := self.arr.push ⟨self.arr.size, 0⟩
   parentD_lt {i} := by
     simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem]
-    split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt _); exact id]
+    split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt ..); exact id]
   rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt
 
 /-- Root of a union-find node. -/
 def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
-  let y := (self.arr[x]).parent
+  let y := self.arr[x.1].parent
   if h : y = x then
     x
   else
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
-    self.root ⟨y, self.parent'_lt x⟩
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ h)
+    self.root ⟨y, self.parent'_lt x _⟩
 termination_by self.rankMax - self.rank x
 
 @[inherit_doc root]
@@ -203,9 +196,9 @@ def rootD (self : UnionFind) (x : Nat) : Nat :=
 
 @[nolint unusedHavesSuffices]
 theorem parent_root (self : UnionFind) (x : Fin self.size) :
-    (self.arr[self.root x]).parent = self.root x := by
+    (self.arr[(self.root x).1]).parent = self.root x := by
   rw [root]; split <;> [assumption; skip]
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
   apply parent_root
 termination_by self.rankMax - self.rank x
 
@@ -232,7 +225,7 @@ theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x <
 @[nolint unusedHavesSuffices]
 theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by
   refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩
-  rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
+  rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq ‹_›] at h)]; rfl]
 
 theorem rootD_rootD {self : UnionFind} {x : Nat} : self.rootD (self.rootD x) = self.rootD x :=
   rootD_eq_self.2 (parent_rootD ..)
@@ -272,12 +265,12 @@ structure FindAux (n : Nat) where
 
 /-- Auxiliary function for find operation -/
 def findAux (self : UnionFind) (x : Fin self.size) : FindAux self.size :=
-  let y := self.arr[x].parent
+  let y := self.arr[x.1].parent
   if h : y = x then
     ⟨self.arr, x, rfl⟩
   else
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
-    let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt x⟩
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ h)
+    let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt _ x.2⟩
     ⟨arr₁.modify x fun s => { s with parent := root }, root, by simp [H]⟩
 termination_by self.rankMax - self.rank x
 
@@ -287,16 +280,16 @@ theorem findAux_root {self : UnionFind} {x : Fin self.size} :
   rw [findAux, root]
   simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]
   split <;> simp only
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
   exact findAux_root
 termination_by self.rankMax - self.rank x
 
 @[nolint unusedHavesSuffices]
 theorem findAux_s {self : UnionFind} {x : Fin self.size} :
-    (findAux self x).s = if self.arr[x].parent = x then self.arr else
-      (self.findAux ⟨_, self.parent'_lt x⟩).s.modify x fun s =>
+    (findAux self x).s = if self.arr[x.1].parent = x then self.arr else
+      (self.findAux ⟨_, self.parent'_lt x x.2⟩).s.modify x fun s =>
         { s with parent := self.rootD x } := by
-  rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
+  rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x x.2⟩).root from _]
   · rw [findAux]; split <;> rfl
   · rw [← rootD_parent, parent, parentD_eq]
     simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]
@@ -308,10 +301,11 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     rankD (findAux self x).s i = self.rank i := by
   if h : i < self.size then
     rw [findAux_s]; split <;> [rfl; skip]
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
     have := lt_of_parentD (by rwa [parentD_eq])
-    rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify]
-    split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
+    rw [rankD_eq (by simp [FindAux.size_eq, h]), Array.getElem_modify]
+    split <;>
+      simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem]
   else
     simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
     rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
@@ -320,13 +314,13 @@ termination_by self.rankMax - self.rank x
 set_option linter.deprecated false in
 theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s i =
-    if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt x⟩).s i := by
+    if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i := by
   rw [findAux_s]; split <;> [split; skip]
   · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]
   · rw [findAux_s]; simp [*, -Array.get_eq_getElem]
   · next h =>
     rw [parentD]; split <;> rename_i h'
-    · rw [Array.get_modify (by simpa using h')]
+    · rw [Array.getElem_modify (by simpa using h')]
       simp only [Array.data_length, @eq_comm _ i]
       split <;> simp [← parentD_eq, -Array.get_eq_getElem]
     · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
@@ -335,47 +329,48 @@ theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
 theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s (self.rootD x) = self.rootD x := by
   rw [parentD_findAux]; split <;> [rfl; rename_i h]
-  rw [rootD_eq_self, parent, parentD_eq] at h
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-  rw [← rootD_parent, parent, parentD_eq]
-  exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt x⟩)
+  rw [rootD_eq_self, parent, parentD_eq x.2] at h
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
+  rw [← rootD_parent, parent, parentD_eq x.2]
+  exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt _ x.2⟩)
 termination_by self.rankMax - self.rank x
 
 theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) :
     parentD (findAux self x).s i < self.size := by
-  if h' : self.arr[x].parent = x then
+  if h' : self.arr[x.1].parent = x then
     rw [findAux_s, if_pos h']; apply self.parentD_lt h
   else
     rw [parentD_findAux]
     split
     · simp [rootD_lt]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
       apply parentD_findAux_lt h
 termination_by self.rankMax - self.rank x
 
 theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
     parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨
     parentD (findAux self x).s i = self.parent i := by
-  if h' : self.arr[x].parent = x then
+  if h' : self.arr[x.1].parent = x then
     rw [findAux_s, if_pos h']; exact .inr rfl
   else
     rw [parentD_findAux]
     split
     · simp [*]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-      exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
-        simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
+      refine (parentD_findAux_or self ⟨_, self.parent'_lt _ x.2⟩ i)
+        |>.imp_left (.imp_right fun h => ?_)
+      simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
 termination_by self.rankMax - self.rank x
 
 theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s i ≠ i →
     self.rank i < self.rank (parentD (findAux self x).s i) := by
-  if h' : self.arr[x].parent = x then
+  if h' : self.arr[x.1].parent = x then
     rw [findAux_s, if_pos h']; apply self.rank_lt
   else
     rw [parentD_findAux]; split <;> rename_i h <;> intro h'
     · subst i; rwa [lt_rank_root, Ne, ← rootD_eq_self]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
       apply lt_rankD_findAux h'
 termination_by self.rankMax - self.rank x
 
@@ -448,8 +443,8 @@ def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
   if x.1 = y then
     self
   else
-    let nx := self[x]
-    let ny := self[y]
+    let nx := self[x.1]
+    let ny := self[y.1]
     if ny.rank < nx.rank then
       self.set y {ny with parent := x}
     else
@@ -460,32 +455,32 @@ def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
         arr₁
 
 theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
-    (hroot : arr[x].rank < arr[y].rank ∨ arr[y].parent = y)
-    (H : arr[x].rank ≤ arr[y].rank) {i : Nat}
+    (hroot : arr[x.1].rank < arr[y.1].rank ∨ arr[y.1].parent = y)
+    (H : arr[x.1].rank ≤ arr[y.1].rank) {i : Nat}
     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
     (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
     (hR : ∀ {i}, rankD arr' i =
-      if y.1 = i ∧ arr[x].rank = arr[y].rank then
-        arr[y].rank + 1
+      if y.1 = i ∧ arr[x.1].rank = arr[y.1].rank then
+        arr[y.1].rank + 1
       else rankD arr i) :
     ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by
   simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
     split <;> rename_i h₂ <;> intro h
   · simp [h₂] at h
-  · simp only [rankD_eq, Array.get_eq_getElem]
+  · simp only [rankD_eq, x.2, y.2, Array.get_eq_getElem]
     split <;> rename_i h₃
     · rw [← h₃]; apply Nat.lt_succ_self
     · exact Nat.lt_of_le_of_ne H h₃
   · cases h₂.1
     simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot
-    simp only [hroot, parentD_eq, not_true_eq_false] at h
+    simp only [hroot, parentD_eq y.2, not_true_eq_false] at h
   · have := rankD_lt h
     split <;> rename_i h₃
     · rw [← rankD_eq, h₃.1]; exact Nat.lt_succ_of_lt this
     · exact this
 
 theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
-    (h : arr[x].rank < arr[y].rank) {i : Nat}
+    (h : arr[x.1].rank < arr[y.1].rank) {i : Nat}
     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) :
     let arr' := arr.set x ⟨y, arr[x].rank⟩
     parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
@@ -506,7 +501,7 @@ def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) :
     · exact self.parentD_lt h
     · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h]
     · rw [parentD_set]; split
-      · exact self.parent'_lt _
+      · exact self.parent'_lt ..
       · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
     · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
   rankD_lt := by
@@ -589,4 +584,3 @@ def checkEquivD (self : UnionFind) (x y : Nat) : UnionFind × Bool :=
 
 /-- Equivalence relation from a `UnionFind` structure -/
 def Equiv (self : UnionFind) (a b : Nat) : Prop := self.rootD a = self.rootD b
--/
diff --git a/Batteries/Data/UnionFind/Lemmas.lean b/Batteries/Data/UnionFind/Lemmas.lean
index d94c75568c..f070a6d4f1 100644
--- a/Batteries/Data/UnionFind/Lemmas.lean
+++ b/Batteries/Data/UnionFind/Lemmas.lean
@@ -1,139 +1,139 @@
--- /-
--- Copyright (c) 2021 Mario Carneiro. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Mario Carneiro
--- -/
--- import Batteries.Data.UnionFind.Basic
-
--- namespace Batteries.UnionFind
-
--- @[simp] theorem arr_empty : empty.arr = #[] := rfl
--- @[simp] theorem parent_empty : empty.parent a = a := rfl
--- @[simp] theorem rank_empty : empty.rank a = 0 := rfl
--- @[simp] theorem rootD_empty : empty.rootD a = a := rfl
-
--- @[simp] theorem arr_push {m : UnionFind} : m.push.arr = m.arr.push ⟨m.arr.size, 0⟩ := rfl
-
--- @[simp] theorem parentD_push {arr : Array UFNode} :
---     parentD (arr.push ⟨arr.size, 0⟩) a = parentD arr a := by
---   simp [parentD]; split <;> split <;> try simp [Array.getElem_push, *]
---   · next h1 h2 =>
---     simp [Nat.lt_succ] at h1 h2
---     exact Nat.le_antisymm h2 h1
---   · next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
-
--- @[simp] theorem parent_push {m : UnionFind} : m.push.parent a = m.parent a := by simp [parent]
-
--- @[simp] theorem rankD_push {arr : Array UFNode} :
---     rankD (arr.push ⟨arr.size, 0⟩) a = rankD arr a := by
---   simp [rankD]; split <;> split <;> try simp [Array.getElem_push, *]
---   next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
-
--- @[simp] theorem rank_push {m : UnionFind} : m.push.rank a = m.rank a := by simp [rank]
-
--- @[simp] theorem rankMax_push {m : UnionFind} : m.push.rankMax = m.rankMax := by simp [rankMax]
-
--- @[simp] theorem root_push {self : UnionFind} : self.push.rootD x = self.rootD x :=
---   rootD_ext fun _ => parent_push
-
--- @[simp] theorem arr_link : (link self x y yroot).arr = linkAux self.arr x y := rfl
-
--- theorem parentD_linkAux {self} {x y : Fin self.size} :
---     parentD (linkAux self x y) i =
---     if x.1 = y then
---       parentD self i
---     else
---       if (self.get y).rank < (self.get x).rank then
---         if y = i then x else parentD self i
---       else
---         if x = i then y else parentD self i := by
---   dsimp only [linkAux]; split <;> [rfl; split] <;> [rw [parentD_set]; split] <;> rw [parentD_set]
---   split <;> [(subst i; rwa [if_neg, parentD_eq]); rw [parentD_set]]
-
--- theorem parent_link {self} {x y : Fin self.size} (yroot) {i} :
---     (link self x y yroot).parent i =
---     if x.1 = y then
---       self.parent i
---     else
---       if self.rank y < self.rank x then
---         if y = i then x else self.parent i
---       else
---         if x = i then y else self.parent i := by
---   simp [rankD_eq]; exact parentD_linkAux
-
--- theorem root_link {self : UnionFind} {x y : Fin self.size}
---     (xroot : self.parent x = x) (yroot : self.parent y = y) :
---     ∃ r, (r = x ∨ r = y) ∧ ∀ i,
---       (link self x y yroot).rootD i =
---       if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
---   if h : x.1 = y then
---     refine ⟨x, .inl rfl, fun i => ?_⟩
---     rw [rootD_ext (m2 := self) (fun _ => by rw [parent_link, if_pos h])]
---     split <;> [obtain _ | _ := ‹_› <;> simp [*]; rfl]
---   else
---   have {x y : Fin self.size}
---       (xroot : self.parent x = x) (yroot : self.parent y = y) {m : UnionFind}
---       (hm : ∀ i, m.parent i = if y = i then x.1 else self.parent i) :
---       ∃ r, (r = x ∨ r = y) ∧ ∀ i,
---         m.rootD i = if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
---     let rec go (i) :
---         m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i := by
---       if h : m.parent i = i then
---         rw [rootD_eq_self.2 h]; rw [hm i] at h; split at h
---         · rw [if_pos, h]; simp [← h, rootD_eq_self, xroot]
---         · rw [rootD_eq_self.2 ‹_›]; split <;> [skip; rfl]
---           next h' => exact h'.resolve_right (Ne.symm ‹_›)
---       else
---         have _ := Nat.sub_lt_sub_left (m.lt_rankMax i) (m.rank_lt h)
---         rw [← rootD_parent, go (m.parent i)]
---         rw [hm i]; split <;> [subst i; rw [rootD_parent]]
---         simp [rootD_eq_self.2 xroot, rootD_eq_self.2 yroot]
---     termination_by m.rankMax - m.rank i
---     exact ⟨x, .inl rfl, go⟩
---   if hr : self.rank y < self.rank x then
---     exact this xroot yroot fun i => by simp [parent_link, h, hr]
---   else
---     simpa (config := {singlePass := true}) [or_comm] using
---       this yroot xroot fun i => by simp [parent_link, h, hr]
-
--- nonrec theorem Equiv.rfl : Equiv self a a := rfl
--- theorem Equiv.symm : Equiv self a b → Equiv self b a := .symm
--- theorem Equiv.trans : Equiv self a b → Equiv self b c → Equiv self a c := .trans
-
--- @[simp] theorem equiv_empty : Equiv empty a b ↔ a = b := by simp [Equiv]
-
--- @[simp] theorem equiv_push : Equiv self.push a b ↔ Equiv self a b := by simp [Equiv]
-
--- @[simp] theorem equiv_rootD : Equiv self (self.rootD a) a := by simp [Equiv, rootD_rootD]
--- @[simp] theorem equiv_rootD_l : Equiv self (self.rootD a) b ↔ Equiv self a b := by
---   simp [Equiv, rootD_rootD]
--- @[simp] theorem equiv_rootD_r : Equiv self a (self.rootD b) ↔ Equiv self a b := by
---   simp [Equiv, rootD_rootD]
-
--- theorem equiv_find : Equiv (self.find x).1 a b ↔ Equiv self a b := by simp [Equiv, find_root_1]
-
--- theorem equiv_link {self : UnionFind} {x y : Fin self.size}
---     (xroot : self.parent x = x) (yroot : self.parent y = y) :
---     Equiv (link self x y yroot) a b ↔
---     Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
---   have {m : UnionFind} {x y : Fin self.size}
---       (xroot : self.rootD x = x) (yroot : self.rootD y = y)
---       (hm : ∀ i, m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i) :
---       Equiv m a b ↔
---       Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
---     simp [Equiv, hm, xroot, yroot]
---     by_cases h1 : rootD self a = x <;> by_cases h2 : rootD self b = x <;>
---       simp [h1, h2, imp_false, Decidable.not_not]
---     · simp [h2, Ne.symm h2]; split <;> simp [@eq_comm _ _ (rootD self b), *]
---     · by_cases h1 : rootD self a = y <;> by_cases h2 : rootD self b = y <;>
---         simp [h1, h2, @eq_comm _ _ (rootD self b), *]
---   obtain ⟨r, ha, hr⟩ := root_link xroot yroot; revert hr
---   rw [← rootD_eq_self] at xroot yroot
---   obtain rfl | rfl := ha
---   · exact this xroot yroot
---   · simpa [or_comm, and_comm] using this yroot xroot
-
--- theorem equiv_union {self : UnionFind} {x y : Fin self.size} :
---     Equiv (union self x y) a b ↔
---     Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
---   simp [union]; rw [equiv_link (by simp [← rootD_eq_self, rootD_rootD])]; simp [equiv_find]
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Batteries.Data.UnionFind.Basic
+
+namespace Batteries.UnionFind
+
+@[simp] theorem arr_empty : empty.arr = #[] := rfl
+@[simp] theorem parent_empty : empty.parent a = a := rfl
+@[simp] theorem rank_empty : empty.rank a = 0 := rfl
+@[simp] theorem rootD_empty : empty.rootD a = a := rfl
+
+@[simp] theorem arr_push {m : UnionFind} : m.push.arr = m.arr.push ⟨m.arr.size, 0⟩ := rfl
+
+@[simp] theorem parentD_push {arr : Array UFNode} :
+    parentD (arr.push ⟨arr.size, 0⟩) a = parentD arr a := by
+  simp [parentD]; split <;> split <;> try simp [Array.getElem_push, *]
+  · next h1 h2 =>
+    simp [Nat.lt_succ] at h1 h2
+    exact Nat.le_antisymm h2 h1
+  · next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
+
+@[simp] theorem parent_push {m : UnionFind} : m.push.parent a = m.parent a := by simp [parent]
+
+@[simp] theorem rankD_push {arr : Array UFNode} :
+    rankD (arr.push ⟨arr.size, 0⟩) a = rankD arr a := by
+  simp [rankD]; split <;> split <;> try simp [Array.getElem_push, *]
+  next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
+
+@[simp] theorem rank_push {m : UnionFind} : m.push.rank a = m.rank a := by simp [rank]
+
+@[simp] theorem rankMax_push {m : UnionFind} : m.push.rankMax = m.rankMax := by simp [rankMax]
+
+@[simp] theorem root_push {self : UnionFind} : self.push.rootD x = self.rootD x :=
+  rootD_ext fun _ => parent_push
+
+@[simp] theorem arr_link : (link self x y yroot).arr = linkAux self.arr x y := rfl
+
+theorem parentD_linkAux {self} {x y : Fin self.size} :
+    parentD (linkAux self x y) i =
+    if x.1 = y then
+      parentD self i
+    else
+      if self[y.1].rank < self[x.1].rank then
+        if y = i then x else parentD self i
+      else
+        if x = i then y else parentD self i := by
+  dsimp only [linkAux]; split <;> [rfl; split] <;> [rw [parentD_set]; split] <;> rw [parentD_set]
+  split <;> [(subst i; rwa [if_neg, parentD_eq]); rw [parentD_set]]
+
+theorem parent_link {self} {x y : Fin self.size} (yroot) {i} :
+    (link self x y yroot).parent i =
+    if x.1 = y then
+      self.parent i
+    else
+      if self.rank y < self.rank x then
+        if y = i then x else self.parent i
+      else
+        if x = i then y else self.parent i := by
+  simp [rankD_eq]; exact parentD_linkAux
+
+theorem root_link {self : UnionFind} {x y : Fin self.size}
+    (xroot : self.parent x = x) (yroot : self.parent y = y) :
+    ∃ r, (r = x ∨ r = y) ∧ ∀ i,
+      (link self x y yroot).rootD i =
+      if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
+  if h : x.1 = y then
+    refine ⟨x, .inl rfl, fun i => ?_⟩
+    rw [rootD_ext (m2 := self) (fun _ => by rw [parent_link, if_pos h])]
+    split <;> [obtain _ | _ := ‹_› <;> simp [*]; rfl]
+  else
+  have {x y : Fin self.size}
+      (xroot : self.parent x = x) (yroot : self.parent y = y) {m : UnionFind}
+      (hm : ∀ i, m.parent i = if y = i then x.1 else self.parent i) :
+      ∃ r, (r = x ∨ r = y) ∧ ∀ i,
+        m.rootD i = if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i := by
+    let rec go (i) :
+        m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i := by
+      if h : m.parent i = i then
+        rw [rootD_eq_self.2 h]; rw [hm i] at h; split at h
+        · rw [if_pos, h]; simp [← h, rootD_eq_self, xroot]
+        · rw [rootD_eq_self.2 ‹_›]; split <;> [skip; rfl]
+          next h' => exact h'.resolve_right (Ne.symm ‹_›)
+      else
+        have _ := Nat.sub_lt_sub_left (m.lt_rankMax i) (m.rank_lt h)
+        rw [← rootD_parent, go (m.parent i)]
+        rw [hm i]; split <;> [subst i; rw [rootD_parent]]
+        simp [rootD_eq_self.2 xroot, rootD_eq_self.2 yroot]
+    termination_by m.rankMax - m.rank i
+    exact ⟨x, .inl rfl, go⟩
+  if hr : self.rank y < self.rank x then
+    exact this xroot yroot fun i => by simp [parent_link, h, hr]
+  else
+    simpa (config := {singlePass := true}) [or_comm] using
+      this yroot xroot fun i => by simp [parent_link, h, hr]
+
+nonrec theorem Equiv.rfl : Equiv self a a := rfl
+theorem Equiv.symm : Equiv self a b → Equiv self b a := .symm
+theorem Equiv.trans : Equiv self a b → Equiv self b c → Equiv self a c := .trans
+
+@[simp] theorem equiv_empty : Equiv empty a b ↔ a = b := by simp [Equiv]
+
+@[simp] theorem equiv_push : Equiv self.push a b ↔ Equiv self a b := by simp [Equiv]
+
+@[simp] theorem equiv_rootD : Equiv self (self.rootD a) a := by simp [Equiv, rootD_rootD]
+@[simp] theorem equiv_rootD_l : Equiv self (self.rootD a) b ↔ Equiv self a b := by
+  simp [Equiv, rootD_rootD]
+@[simp] theorem equiv_rootD_r : Equiv self a (self.rootD b) ↔ Equiv self a b := by
+  simp [Equiv, rootD_rootD]
+
+theorem equiv_find : Equiv (self.find x).1 a b ↔ Equiv self a b := by simp [Equiv, find_root_1]
+
+theorem equiv_link {self : UnionFind} {x y : Fin self.size}
+    (xroot : self.parent x = x) (yroot : self.parent y = y) :
+    Equiv (link self x y yroot) a b ↔
+    Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
+  have {m : UnionFind} {x y : Fin self.size}
+      (xroot : self.rootD x = x) (yroot : self.rootD y = y)
+      (hm : ∀ i, m.rootD i = if self.rootD i = x ∨ self.rootD i = y then x.1 else self.rootD i) :
+      Equiv m a b ↔
+      Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
+    simp [Equiv, hm, xroot, yroot]
+    by_cases h1 : rootD self a = x <;> by_cases h2 : rootD self b = x <;>
+      simp [h1, h2, imp_false, Decidable.not_not]
+    · simp [h2, Ne.symm h2]; split <;> simp [@eq_comm _ _ (rootD self b), *]
+    · by_cases h1 : rootD self a = y <;> by_cases h2 : rootD self b = y <;>
+        simp [h1, h2, @eq_comm _ _ (rootD self b), *]
+  obtain ⟨r, ha, hr⟩ := root_link xroot yroot; revert hr
+  rw [← rootD_eq_self] at xroot yroot
+  obtain rfl | rfl := ha
+  · exact this xroot yroot
+  · simpa [or_comm, and_comm] using this yroot xroot
+
+theorem equiv_union {self : UnionFind} {x y : Fin self.size} :
+    Equiv (union self x y) a b ↔
+    Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b := by
+  simp [union]; rw [equiv_link (by simp [← rootD_eq_self, rootD_rootD])]; simp [equiv_find]
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index d5989898eb..73a4a41aee 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -68,7 +68,7 @@ instance [Inhabited α] : Inhabited (Vector α n) where
 
 /-- Get an element of a vector using a `Fin` index. -/
 @[inline] def get (v : Vector α n) (i : Fin n) : α :=
-  v.toArray[i.cast v.size_toArray.symm]
+  v.toArray[(i.cast v.size_toArray.symm).1]
 
 /-- Get an element of a vector using a `USize` index and a proof that the index is within bounds. -/
 @[inline] def uget (v : Vector α n) (i : USize) (h : i.toNat < n) : α :=
diff --git a/Batteries/StdDeprecations.lean b/Batteries/StdDeprecations.lean
index a17f235cee..74a00f4f5a 100644
--- a/Batteries/StdDeprecations.lean
+++ b/Batteries/StdDeprecations.lean
@@ -48,18 +48,16 @@ alias Std.compareOfLessAndEq_eq_lt := Batteries.compareOfLessAndEq_eq_lt
 @[deprecated (since := "2024-05-07")] alias Std.mkRBMap := Batteries.mkRBMap
 @[deprecated (since := "2024-05-07")] alias Std.BinomialHeap := Batteries.BinomialHeap
 @[deprecated (since := "2024-05-07")] alias Std.mkBinomialHeap := Batteries.mkBinomialHeap
+@[deprecated (since := "2024-05-07")] alias Std.UFNode := Batteries.UFNode
+@[deprecated (since := "2024-05-07")] alias Std.UnionFind := Batteries.UnionFind
 
--- TODO: restore these when UnionFind is un-commented.
--- @[deprecated (since := "2024-05-07")] alias Std.UFNode := Batteries.UFNode
--- @[deprecated (since := "2024-05-07")] alias Std.UnionFind := Batteries.UnionFind
-
--- -- Check that these generate usable deprecated hints
--- -- when referring to names inside these namespaces.
--- set_option warningAsError true in
--- /--
--- error: `Std.UnionFind` has been deprecated, use `Batteries.UnionFind` instead
--- ---
--- error: unknown constant 'Std.UnionFind.find'
--- -/
--- #guard_msgs in
--- #eval Std.UnionFind.find
+-- Check that these generate usable deprecated hints
+-- when referring to names inside these namespaces.
+set_option warningAsError true in
+/--
+error: `Std.UnionFind` has been deprecated, use `Batteries.UnionFind` instead
+---
+error: unknown constant 'Std.UnionFind.find'
+-/
+#guard_msgs in
+#eval Std.UnionFind.find