From 0c99c08c3b6fd18160eeb6eace019adeaf593761 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 17 Apr 2024 12:51:10 -0500 Subject: [PATCH] chore(FinEnum): `List.nthLe` -> `List.get` --- Mathlib/Data/FinEnum.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/Data/FinEnum.lean b/Mathlib/Data/FinEnum.lean index 7654b41d4cb1e..26cc839e3db9f 100644 --- a/Mathlib/Data/FinEnum.lean +++ b/Mathlib/Data/FinEnum.lean @@ -48,13 +48,12 @@ def ofEquiv (α) {β} [FinEnum α] (h : β ≃ α) : FinEnum β #align fin_enum.of_equiv FinEnum.ofEquiv /-- create a `FinEnum` instance from an exhaustive list without duplicates -/ -def ofNodupList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) (h' : List.Nodup xs) : FinEnum α - where +def ofNodupList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) (h' : List.Nodup xs) : + FinEnum α where card := xs.length equiv := - ⟨fun x => ⟨xs.indexOf x, by rw [List.indexOf_lt_length]; apply h⟩, fun ⟨i, h⟩ => - xs.nthLe _ h, fun x => by simp, fun ⟨i, h⟩ => by - simp [*]⟩ + ⟨fun x => ⟨xs.indexOf x, by rw [List.indexOf_lt_length]; apply h⟩, xs.get, fun x => by simp, + fun i => by ext; simp [List.get_indexOf h']⟩ #align fin_enum.of_nodup_list FinEnum.ofNodupList /-- create a `FinEnum` instance from an exhaustive list; duplicates are removed -/