From 8de4e6c1b56f8b7b84da8da29a9179d495e54737 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 19 Nov 2024 21:00:18 +1100 Subject: [PATCH] chore: use List.getElem rather than List.get --- Mathlib/Analysis/Calculus/FDeriv/Mul.lean | 2 +- Mathlib/Combinatorics/Enumerative/Composition.lean | 4 ++-- Mathlib/Data/Finset/Sort.lean | 4 ++-- Mathlib/Data/List/Cycle.lean | 10 +++++----- Mathlib/Data/List/NodupEquivFin.lean | 2 +- Mathlib/Data/Vector/Mem.lean | 2 +- .../ClassNumber/AdmissibleAbsoluteValue.lean | 2 +- 7 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean index e8073446374b3..6b5f7dc3f86f0 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean @@ -690,7 +690,7 @@ theorem HasFDerivWithinAt.list_prod' {l : List ι} {x : E} smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) s x := by simp only [← List.finRange_map_get l, List.map_map] refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x - (hasFDerivWithinAt_pi.mpr fun i ↦ h l[i] (l.get_mem i i.isLt))) ?_ + (hasFDerivWithinAt_pi.mpr fun i ↦ h l[i] (l.getElem_mem i.isLt))) ?_ ext m simp [← List.map_map] diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean index 986e40eed5b1b..20b7c32701611 100644 --- a/Mathlib/Combinatorics/Enumerative/Composition.lean +++ b/Mathlib/Combinatorics/Enumerative/Composition.lean @@ -150,7 +150,7 @@ theorem sum_blocksFun : ∑ i, c.blocksFun i = n := by conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn] theorem blocksFun_mem_blocks (i : Fin c.length) : c.blocksFun i ∈ c.blocks := - get_mem _ _ _ + getElem_mem _ @[simp] theorem one_le_blocks {i : ℕ} (h : i ∈ c.blocks) : 1 ≤ i := @@ -158,7 +158,7 @@ theorem one_le_blocks {i : ℕ} (h : i ∈ c.blocks) : 1 ≤ i := @[simp] theorem one_le_blocks' {i : ℕ} (h : i < c.length) : 1 ≤ c.blocks[i] := - c.one_le_blocks (get_mem (blocks c) i h) + c.one_le_blocks (getElem_mem h) @[simp] theorem blocks_pos' (i : ℕ) (h : i < c.length) : 0 < c.blocks[i] := diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean index 7e7f3fc62d674..486acd9c00f1b 100644 --- a/Mathlib/Data/Finset/Sort.lean +++ b/Mathlib/Data/Finset/Sort.lean @@ -113,7 +113,7 @@ theorem sorted_zero_eq_min'_aux (s : Finset α) (h : 0 < (s.sort (· ≤ ·)).le obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this rw [← hi] exact (s.sort_sorted (· ≤ ·)).rel_get_of_le (Nat.zero_le i) - · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l 0 h) + · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.getElem_mem h) exact s.min'_le _ this theorem sorted_zero_eq_min' {s : Finset α} {h : 0 < (s.sort (· ≤ ·)).length} : @@ -130,7 +130,7 @@ theorem sorted_last_eq_max'_aux (s : Finset α) let l := s.sort (· ≤ ·) apply le_antisymm · have : l.get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ ∈ s := - (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _ h) + (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.getElem_mem h) exact s.le_max' _ this · have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H) obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this diff --git a/Mathlib/Data/List/Cycle.lean b/Mathlib/Data/List/Cycle.lean index 167f0c1116671..876e1a2130482 100644 --- a/Mathlib/Data/List/Cycle.lean +++ b/Mathlib/Data/List/Cycle.lean @@ -217,7 +217,7 @@ theorem prev_ne_cons_cons (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz · rw [prev, dif_neg hy, if_neg hz] theorem next_mem (h : x ∈ l) : l.next x h ∈ l := - nextOr_mem (get_mem _ _ _) + nextOr_mem (getElem_mem _) theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by cases' l with hd tl @@ -233,7 +233,7 @@ theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by · exact mem_cons_of_mem _ (hl _ _) theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) : - next l (l.get i) (get_mem _ _ _) = + next l (l.get i) (getElem_mem _) = l.get ⟨(i + 1) % l.length, Nat.mod_lt _ (i.1.zero_le.trans_lt i.2)⟩ := match l, h, i with | [], _, i => by simpa using i.2 @@ -254,7 +254,7 @@ theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) : · subst hi' rw [next_getLast_cons] · simp [hi', get] - · rw [get_cons_succ]; exact get_mem _ _ _ + · rw [get_cons_succ]; exact getElem_mem _ · exact hx' · simp [getLast_eq_getElem] · exact hn.of_cons @@ -271,12 +271,12 @@ theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) : intro h have := nodup_iff_injective_get.1 hn h simp at this; simp [this] at hi' - · rw [get_cons_succ]; exact get_mem _ _ _ + · rw [get_cons_succ]; exact getElem_mem _ -- Unused variable linter incorrectly reports that `h` is unused here. set_option linter.unusedVariables false in theorem prev_get (l : List α) (h : Nodup l) (i : Fin l.length) : - prev l (l.get i) (get_mem _ _ _) = + prev l (l.get i) (getElem_mem _) = l.get ⟨(i + (l.length - 1)) % l.length, Nat.mod_lt _ i.pos⟩ := match l with | [] => by simpa using i.2 diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean index 65a48a57e4574..fbcf74a9eec72 100644 --- a/Mathlib/Data/List/NodupEquivFin.lean +++ b/Mathlib/Data/List/NodupEquivFin.lean @@ -49,7 +49,7 @@ variable [DecidableEq α] the set of elements of `l`. -/ @[simps] def getEquiv (l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l } where - toFun i := ⟨get l i, get_mem l i i.2⟩ + toFun i := ⟨get l i, getElem_mem i.2⟩ invFun x := ⟨indexOf (↑x) l, indexOf_lt_length.2 x.2⟩ left_inv i := by simp only [List.get_indexOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H] right_inv x := by simp diff --git a/Mathlib/Data/Vector/Mem.lean b/Mathlib/Data/Vector/Mem.lean index 3eb0fe6678d82..bd52e003d0ed4 100644 --- a/Mathlib/Data/Vector/Mem.lean +++ b/Mathlib/Data/Vector/Mem.lean @@ -24,7 +24,7 @@ variable {α β : Type*} {n : ℕ} (a a' : α) @[simp] theorem get_mem (i : Fin n) (v : Vector α n) : v.get i ∈ v.toList := by rw [get_eq_get] - exact List.get_mem _ _ _ + exact List.getElem_mem _ theorem mem_iff_get (v : Vector α n) : a ∈ v.toList ↔ ∃ i, v.get i = a := by simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get] diff --git a/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean b/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean index bdc2a13623ee7..22fc2f2d46e5e 100644 --- a/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean +++ b/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean @@ -102,7 +102,7 @@ theorem exists_approx_aux (n : ℕ) (h : abv.IsAdmissible) : /-- This proof was nicer prior to https://github.com/leanprover/lean4/pull/4400. Please feel welcome to improve it, by avoiding use of `List.get` in favour of `GetElem`. -/ have : ∀ i h, t ((Finset.univ.filter fun x ↦ t x = s).toList.get ⟨i, h⟩) = s := fun i h ↦ - (Finset.mem_filter.mp (Finset.mem_toList.mp (List.get_mem _ i h))).2 + (Finset.mem_filter.mp (Finset.mem_toList.mp (List.getElem_mem h))).2 simp only [Nat.succ_eq_add_one, Finset.length_toList, List.get_eq_getElem] at this simp only [Nat.succ_eq_add_one, List.get_eq_getElem, Fin.coe_castLE] rw [this _ (Nat.lt_of_le_of_lt (Nat.le_of_lt_succ i₁.2) hs),