Lemmas reproduced from Batteries.

These are the Batteries lemmas the Mathlib-free hex libraries (HexMatrix, HexRowReduce, HexDeterminant, HexGramSchmidt, HexBerlekamp) relied on but which are not (yet) in the Lean core library. They are reproduced here, with names and signatures identical to the Batteries originals, so the Mathlib-free libraries no longer need to depend on Batteries. Remove each one if it is migrated up to lean4.

Keeping the signatures identical to Batteries is deliberate: the *Mathlib bridge libraries pull Batteries in via Mathlib, so both copies coexist there. Lean accepts duplicate declarations from different modules when their signatures match (the proofs may differ), so there is no clash. If you change a signature here it will collide with Batteries in the bridge libraries.

theorem List.pairwise_lt_finRange (n : Nat) : Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (finRange n)

Reproduced from Batteries.Data.List.Lemmas; remove if migrated up to lean4.

theorem List.nodup_finRange (n : Nat) : (finRange n).Nodup

Reproduced from Batteries.Data.List.Lemmas; remove if migrated up to lean4.

theorem List.perm_ext_iff_of_nodup {α : Type u_1} {l₁ l₂ : List α} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : l₁.Perm l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂

Reproduced from Batteries.Data.List.Perm; remove if migrated up to lean4. The Batteries original has no [DecidableEq α]; we match that signature and use classical in the proof, since core lacks the Subperm API Batteries uses.

@[simp]

theorem List.getElem_idxOf {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {xs : List α} (h : idxOf x xs < xs.length) : xs[idxOf x xs] = x

Reproduced from Batteries.Data.List.Lemmas; remove if migrated up to lean4.

@[simp]

theorem List.Nodup.idxOf_getElem {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} (H : xs.Nodup) (i : Nat) (h : i < xs.length) : idxOf xs[i] xs = i

Reproduced from Batteries.Data.List.Lemmas; remove if migrated up to lean4.

theorem List.nodup_subset_length_le {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} (h₁ : l₁.Nodup) (hsub : l₁ ⊆ l₂) : l₁.length ≤ l₂.length

A Nodup list contained in another list is no longer than it. Replaces uses of Batteries' Subperm API (subperm_of_subset/Subperm.length_le), which core lacks; this name is not from Batteries. Remove in favour of a core lemma if one is migrated up to lean4.