Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib/Data/List/EditDistance/Bounds.lean

@@ -79,7 +79,7 @@ theorem le_suffixLevenshtein_append_minimum (xs : List α) (ys₁ ys₂) :
 theorem suffixLevenshtein_minimum_le_levenshtein_append (xs ys₁ ys₂) :
     (suffixLevenshtein C xs ys₂).1.minimum ≤ levenshtein C xs (ys₁ ++ ys₂) := by
   cases ys₁ with
-  | nil => exact List.minimum_le_of_mem' (List.get_mem _ _ _)
+  | nil => exact List.minimum_le_of_mem' (List.getElem_mem _)
   | cons y ys₁ =>
       exact (le_suffixLevenshtein_append_minimum _ _ _).trans
         (suffixLevenshtein_minimum_le_levenshtein_cons _ _ _)

Mathlib/Data/List/MinMax.lean

@@ -427,7 +427,7 @@ theorem minimum_of_length_pos_le_of_mem (h : a ∈ l) (w : 0 < l.length) :
 theorem getElem_le_maximum_of_length_pos {i : ℕ} (w : i < l.length) (h := (Nat.zero_lt_of_lt w)) :
     l[i] ≤ l.maximum_of_length_pos h := by
   apply le_maximum_of_length_pos_of_mem
-  exact get_mem l i w
+  exact getElem_mem _
 
 theorem minimum_of_length_pos_le_getElem {i : ℕ} (w : i < l.length) (h := (Nat.zero_lt_of_lt w)) :
     l.minimum_of_length_pos h ≤ l[i] :=

Mathlib/Data/List/Nodup.lean

@@ -122,7 +122,7 @@ theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length)
 
 theorem indexOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) :
     indexOf l[i] l = i :=
-  suffices (⟨indexOf l[i] l, indexOf_lt_length.2 (get_mem _ _ _)⟩ : Fin l.length) = ⟨i, h⟩
+  suffices (⟨indexOf l[i] l, indexOf_lt_length.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩
     from Fin.val_eq_of_eq this
   nodup_iff_injective_get.1 H (by simp)
 

Mathlib/Data/List/NodupEquivFin.lean

@@ -127,7 +127,7 @@ theorem sublist_of_orderEmbedding_get?_eq {l l' : List α} (f : ℕ ↪o ℕ)
   rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
   apply List.Sublist.append _ (IH _ this)
   rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]
-  apply List.get_mem
+  exact List.getElem_mem _
 
 /-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
 there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that

Mathlib/SetTheory/Nimber/Basic.lean

@@ -44,16 +44,16 @@ noncomputable section
 
 /-! ### Basic casts between `Ordinal` and `Nimber` -/
 
-/-- A type synonym for ordinals with natural addition and multiplication. -/
+/-- A type synonym for ordinals with nimber addition and multiplication. -/
 def Nimber : Type _ :=
   Ordinal deriving Zero, Inhabited, One, Nontrivial, WellFoundedRelation
 
-instance Nimber.linearOrder : LinearOrder Nimber := {Ordinal.linearOrder with}
-instance Nimber.succOrder : SuccOrder Nimber := {Ordinal.instSuccOrder with}
-instance Nimber.orderBot : OrderBot Nimber := {Ordinal.orderBot with}
-instance Nimber.noMaxOrder : NoMaxOrder Nimber := {Ordinal.noMaxOrder with}
-instance Nimber.zeroLEOneClass : ZeroLEOneClass Nimber := {Ordinal.zeroLEOneClass with}
-instance Nimber.instNeZeroOne : NeZero (1 : Nimber) := Ordinal.NeZero.one
+instance Nimber.instLinearOrder : LinearOrder Nimber := Ordinal.instLinearOrder
+instance Nimber.instSuccOrder : SuccOrder Nimber := Ordinal.instSuccOrder
+instance Nimber.instOrderBot : OrderBot Nimber := Ordinal.instOrderBot
+instance Nimber.instNoMaxOrder : NoMaxOrder Nimber := Ordinal.instNoMaxOrder
+instance Nimber.instZeroLEOneClass : ZeroLEOneClass Nimber := Ordinal.instZeroLEOneClass
+instance Nimber.instNeZeroOne : NeZero (1 : Nimber) := Ordinal.instNeZeroOne
 
 /-- The identity function between `Ordinal` and `Nimber`. -/
 @[match_pattern]

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -287,7 +287,7 @@ instance partialOrder : PartialOrder Ordinal where
     Quotient.inductionOn₂ a b fun _ _ ⟨h₁⟩ ⟨h₂⟩ =>
       Quot.sound ⟨InitialSeg.antisymm h₁ h₂⟩
 
-instance linearOrder : LinearOrder Ordinal :=
+instance : LinearOrder Ordinal :=
   {inferInstanceAs (PartialOrder Ordinal) with
     le_total := fun a b => Quotient.inductionOn₂ a b fun ⟨_, r, _⟩ ⟨_, s, _⟩ =>
       (InitialSeg.total r s).recOn (fun f => Or.inl ⟨f⟩) fun f => Or.inr ⟨f⟩
@@ -309,7 +309,7 @@ theorem _root_.PrincipalSeg.ordinal_type_lt {α β} {r : α → α → Prop} {s
 protected theorem zero_le (o : Ordinal) : 0 ≤ o :=
   inductionOn o fun _ r _ => (InitialSeg.ofIsEmpty _ r).ordinal_type_le
 
-instance orderBot : OrderBot Ordinal where
+instance : OrderBot Ordinal where
   bot := 0
   bot_le := Ordinal.zero_le
 
@@ -330,10 +330,10 @@ protected theorem not_lt_zero (o : Ordinal) : ¬o < 0 :=
 theorem eq_zero_or_pos : ∀ a : Ordinal, a = 0 ∨ 0 < a :=
   eq_bot_or_bot_lt
 
-instance zeroLEOneClass : ZeroLEOneClass Ordinal :=
+instance : ZeroLEOneClass Ordinal :=
   ⟨Ordinal.zero_le _⟩
 
-instance NeZero.one : NeZero (1 : Ordinal) :=
+instance instNeZeroOne : NeZero (1 : Ordinal) :=
   ⟨Ordinal.one_ne_zero⟩
 
 theorem type_le_iff {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r]
@@ -875,13 +875,13 @@ private theorem succ_le_iff' {a b : Ordinal} : a + 1 ≤ b ↔ a < b := by
   · apply (RelEmbedding.ofMonotone (Sum.recOn · f fun _ ↦ f.top) ?_).ordinal_type_le
     simpa [f.map_rel_iff] using f.lt_top
 
-instance noMaxOrder : NoMaxOrder Ordinal :=
+instance : NoMaxOrder Ordinal :=
   ⟨fun _ => ⟨_, succ_le_iff'.1 le_rfl⟩⟩
 
-instance instSuccOrder : SuccOrder Ordinal.{u} :=
+instance : SuccOrder Ordinal.{u} :=
   SuccOrder.ofSuccLeIff (fun o => o + 1) succ_le_iff'
 
-instance instSuccAddOrder : SuccAddOrder Ordinal := ⟨fun _ => rfl⟩
+instance : SuccAddOrder Ordinal := ⟨fun _ => rfl⟩
 
 @[simp]
 theorem add_one_eq_succ (o : Ordinal) : o + 1 = succ o :=

Mathlib/SetTheory/Ordinal/NaturalOps.lean

@@ -53,10 +53,12 @@ def NatOrdinal : Type _ :=
   -- Porting note: used to derive LinearOrder & SuccOrder but need to manually define
   Ordinal deriving Zero, Inhabited, One, WellFoundedRelation
 
-instance NatOrdinal.linearOrder : LinearOrder NatOrdinal := {Ordinal.linearOrder with}
-instance NatOrdinal.instSuccOrder : SuccOrder NatOrdinal := {Ordinal.instSuccOrder with}
-instance NatOrdinal.orderBot : OrderBot NatOrdinal := {Ordinal.orderBot with}
-instance NatOrdinal.noMaxOrder : NoMaxOrder NatOrdinal := {Ordinal.noMaxOrder with}
+instance NatOrdinal.instLinearOrder : LinearOrder NatOrdinal := Ordinal.instLinearOrder
+instance NatOrdinal.instSuccOrder : SuccOrder NatOrdinal := Ordinal.instSuccOrder
+instance NatOrdinal.instOrderBot : OrderBot NatOrdinal := Ordinal.instOrderBot
+instance NatOrdinal.instNoMaxOrder : NoMaxOrder NatOrdinal := Ordinal.instNoMaxOrder
+instance NatOrdinal.instZeroLEOneClass : ZeroLEOneClass NatOrdinal := Ordinal.instZeroLEOneClass
+instance NatOrdinal.instNeZeroOne : NeZero (1 : NatOrdinal) := Ordinal.instNeZeroOne
 
 /-- The identity function between `Ordinal` and `NatOrdinal`. -/
 @[match_pattern]
@@ -316,19 +318,19 @@ open Ordinal NaturalOps
 instance : Add NatOrdinal := ⟨nadd⟩
 instance : SuccAddOrder NatOrdinal := ⟨fun x => (nadd_one x).symm⟩
 
-instance addLeftStrictMono : AddLeftStrictMono NatOrdinal.{u} :=
+instance : AddLeftStrictMono NatOrdinal.{u} :=
   ⟨fun a _ _ h => nadd_lt_nadd_left h a⟩
 
-instance addLeftMono : AddLeftMono NatOrdinal.{u} :=
+instance : AddLeftMono NatOrdinal.{u} :=
   ⟨fun a _ _ h => nadd_le_nadd_left h a⟩
 
-instance addLeftReflectLE : AddLeftReflectLE NatOrdinal.{u} :=
+instance : AddLeftReflectLE NatOrdinal.{u} :=
   ⟨fun a b c h => by
     by_contra! h'
     exact h.not_lt (add_lt_add_left h' a)⟩
 
-instance orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid NatOrdinal :=
-  { NatOrdinal.linearOrder with
+instance : OrderedCancelAddCommMonoid NatOrdinal :=
+  { NatOrdinal.instLinearOrder with
     add := (· + ·)
     add_assoc := nadd_assoc
     add_le_add_left := fun _ _ => add_le_add_left
@@ -339,7 +341,7 @@ instance orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid NatOrdinal :=
     add_comm := nadd_comm
     nsmul := nsmulRec }
 
-instance addMonoidWithOne : AddMonoidWithOne NatOrdinal :=
+instance : AddMonoidWithOne NatOrdinal :=
   AddMonoidWithOne.unary
 
 @[deprecated Order.succ_eq_add_one (since := "2024-09-04")]
@@ -674,8 +676,8 @@ instance : Mul NatOrdinal :=
 -- Porting note: had to add universe annotations to ensure that the
 -- two sources lived in the same universe.
 instance : OrderedCommSemiring NatOrdinal.{u} :=
-  { NatOrdinal.orderedCancelAddCommMonoid.{u},
-    NatOrdinal.linearOrder.{u} with
+  { NatOrdinal.instOrderedCancelAddCommMonoid.{u},
+    NatOrdinal.instLinearOrder.{u} with
     mul := (· * ·)
     left_distrib := nmul_nadd
     right_distrib := nadd_nmul

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23b4216d1e3a2064058bb415c11e5f6df0417c99",
+   "rev": "922825a3fa019deafbf4f61ed7c70fbdeebc9206",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",