copy across some Find API to Array

src/Init/Data/Option/Basic.lean

@@ -101,12 +101,6 @@ This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
   | some x,   some y => r x y
   | _, _             => False
 
-@[inline] protected def le (r : α → β → Prop) : Option α → Option β → Prop
-  | none,   some _ => True
-  | none,   none   => True
-  | some _, none   => False
-  | some x, some y => r x y
-
 instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
   | none,   some _ => isTrue  trivial
   | some x, some y => s x y
@@ -223,24 +217,18 @@ instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
 @[simp] theorem any_none : Option.any p none = false := rfl
 @[simp] theorem any_some : Option.any p (some x) = p x := rfl
 
-/--
-The minimum of two optional values.
-
-Note this treats `none` as the least element,
-so `min none x = min x none = none` for all `x : Option α`.
-Prior to nightly-2025-02-27, we instead had `min none (some x) = min (some x) none = some x`.
--/
+/-- The minimum of two optional values. -/
 protected def min [Min α] : Option α → Option α → Option α
   | some x, some y => some (Min.min x y)
-  | some _, none => none
-  | none, some _ => none
+  | some x, none => some x
+  | none, some y => some y
   | none, none => none
 
 instance [Min α] : Min (Option α) where min := Option.min
 
 @[simp] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl
-@[simp] theorem min_some_none [Min α] {a : α} : min (some a) none = none := rfl
-@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = none := rfl
+@[simp] theorem min_some_none [Min α] {a : α} : min (some a) none = some a := rfl
+@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = some b := rfl
 @[simp] theorem min_none_none [Min α] : min (none : Option α) none = none := rfl
 
 /-- The maximum of two optional values. -/
@@ -263,9 +251,6 @@ end Option
 instance [LT α] : LT (Option α) where
   lt := Option.lt (· < ·)
 
-instance [LE α] : LE (Option α) where
-  le := Option.le (· ≤ ·)
-
 @[always_inline]
 instance : Functor Option where
   map := Option.map

src/Init/Data/Option/Lemmas.lean

@@ -673,80 +673,4 @@ theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p
        o.pelim g (fun a h => g' (f a (H a h))) := by
   cases o <;> simp
 
-/-! ### LT and LE -/
-
-@[simp] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
-@[simp] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
-@[simp] theorem some_lt_some [LT α] {a b : α} : some a < some b ↔ a < b := by simp [LT.lt, Option.lt]
-
-@[simp] theorem none_le [LE α] {a : Option α} : none ≤ a := by cases a <;> simp [LE.le, Option.le]
-@[simp] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le]
-@[simp] theorem some_le_some [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le]
-
-/-! ### min and max -/
-
-theorem min_eq_left [LE α] [Min α] (min_eq_left : ∀ x y : α, x ≤ y → min x y = x)
-    {a b : Option α} (h : a ≤ b) : min a b = a := by
-  cases a <;> cases b <;> simp_all
-
-theorem min_eq_right [LE α] [Min α] (min_eq_right : ∀ x y : α, y ≤ x → min x y = y)
-    {a b : Option α} (h : b ≤ a) : min a b = b := by
-  cases a <;> cases b <;> simp_all
-
-theorem min_eq_left_of_lt [LT α] [Min α] (min_eq_left : ∀ x y : α, x < y → min x y = x)
-    {a b : Option α} (h : a < b) : min a b = a := by
-  cases a <;> cases b <;> simp_all
-
-theorem min_eq_right_of_lt [LT α] [Min α] (min_eq_right : ∀ x y : α, y < x → min x y = y)
-    {a b : Option α} (h : b < a) : min a b = b := by
-  cases a <;> cases b <;> simp_all
-
-theorem min_eq_or [LE α] [Min α] (min_eq_or : ∀ x y : α, min x y = x ∨ min x y = y)
-    {a b : Option α} : min a b = a ∨ min a b = b := by
-  cases a <;> cases b <;> simp_all
-
-theorem min_le_left [LE α] [Min α] (min_le_left : ∀ x y : α, min x y ≤ x)
-    {a b : Option α} : min a b ≤ a := by
-  cases a <;> cases b <;> simp_all
-
-theorem min_le_right [LE α] [Min α] (min_le_right : ∀ x y : α, min x y ≤ y)
-    {a b : Option α} : min a b ≤ b := by
-  cases a <;> cases b <;> simp_all
-
-theorem le_min [LE α] [Min α] (le_min : ∀ x y z : α, x ≤ min y z ↔ x ≤ y ∧ x ≤ z)
-    {a b c : Option α} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c := by
-  cases a <;> cases b <;> cases c <;> simp_all
-
-theorem max_eq_left [LE α] [Max α] (max_eq_left : ∀ x y : α, x ≤ y → max x y = y)
-    {a b : Option α} (h : a ≤ b) : max a b = b := by
-  cases a <;> cases b <;> simp_all
-
-theorem max_eq_right [LE α] [Max α] (max_eq_right : ∀ x y : α, y ≤ x → max x y = x)
-    {a b : Option α} (h : b ≤ a) : max a b = a := by
-  cases a <;> cases b <;> simp_all
-
-theorem max_eq_left_of_lt [LT α] [Max α] (max_eq_left : ∀ x y : α, x < y → max x y = y)
-    {a b : Option α} (h : a < b) : max a b = b := by
-  cases a <;> cases b <;> simp_all
-
-theorem max_eq_right_of_lt [LT α] [Max α] (max_eq_right : ∀ x y : α, y < x → max x y = x)
-    {a b : Option α} (h : b < a) : max a b = a := by
-  cases a <;> cases b <;> simp_all
-
-theorem max_eq_or [LE α] [Max α] (max_eq_or : ∀ x y : α, max x y = x ∨ max x y = y)
-    {a b : Option α} : max a b = a ∨ max a b = b := by
-  cases a <;> cases b <;> simp_all
-
-theorem left_le_max [LE α] [Max α] (le_refl : ∀ x : α, x ≤ x) (left_le_max : ∀ x y : α, x ≤ max x y)
-    {a b : Option α} : a ≤ max a b := by
-  cases a <;> cases b <;> simp_all
-
-theorem right_le_max [LE α] [Max α] (le_refl : ∀ x : α, x ≤ x) (right_le_max : ∀ x y : α, y ≤ max x y)
-    {a b : Option α} : b ≤ max a b := by
-  cases a <;> cases b <;> simp_all
-
-theorem max_le [LE α] [Max α] (max_le : ∀ x y z : α, max x y ≤ z ↔ x ≤ z ∧ y ≤ z)
-    {a b c : Option α} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c := by
-  cases a <;> cases b <;> cases c <;> simp_all
-
 end Option

src/Init/Data/SInt/Lemmas.lean

@@ -11,15 +11,3 @@ import Init.Data.SInt.Basic
 @[simp] theorem UInt32.toBitVec_toInt32 (x : UInt32) : x.toInt32.toBitVec = x.toBitVec := rfl
 @[simp] theorem UInt64.toBitVec_toInt64 (x : UInt64) : x.toInt64.toBitVec = x.toBitVec := rfl
 @[simp] theorem USize.toBitVec_toISize (x : USize) : x.toISize.toBitVec = x.toBitVec := rfl
-
-@[simp] theorem Int8.ofBitVec_uInt8ToBitVec (x : UInt8) : Int8.ofBitVec x.toBitVec = x.toInt8 := rfl
-@[simp] theorem Int16.ofBitVec_uInt16ToBitVec (x : UInt16) : Int16.ofBitVec x.toBitVec = x.toInt16 := rfl
-@[simp] theorem Int32.ofBitVec_uInt32ToBitVec (x : UInt32) : Int32.ofBitVec x.toBitVec = x.toInt32 := rfl
-@[simp] theorem Int64.ofBitVec_uInt64ToBitVec (x : UInt64) : Int64.ofBitVec x.toBitVec = x.toInt64 := rfl
-@[simp] theorem ISize.ofBitVec_uSize8ToBitVec (x : USize) : ISize.ofBitVec x.toBitVec = x.toISize := rfl
-
-@[simp] theorem UInt8.toUInt8_toInt8 (x : UInt8) : x.toInt8.toUInt8 = x := rfl
-@[simp] theorem UInt16.toUInt16_toInt16 (x : UInt16) : x.toInt16.toUInt16 = x := rfl
-@[simp] theorem UInt32.toUInt32_toInt32 (x : UInt32) : x.toInt32.toUInt32 = x := rfl
-@[simp] theorem UInt64.toUInt64_toInt64 (x : UInt64) : x.toInt64.toUInt64 = x := rfl
-@[simp] theorem USize.toUSize_toISize (x : USize) : x.toISize.toUSize = x := rfl

src/Init/Data/UInt/Lemmas.lean

@@ -295,51 +295,6 @@ theorem UInt16.toNat_lt_usizeSize (n : UInt16) : n.toNat < USize.size :=
 theorem UInt32.toNat_lt_usizeSize (n : UInt32) : n.toNat < USize.size :=
   Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
 
-theorem UInt8.size_dvd_usizeSize : UInt8.size ∣ USize.size := by cases USize.size_eq <;> simp_all +decide
-theorem UInt16.size_dvd_usizeSize : UInt16.size ∣ USize.size := by cases USize.size_eq <;> simp_all +decide
-theorem UInt32.size_dvd_usizeSize : UInt32.size ∣ USize.size := by cases USize.size_eq <;> simp_all +decide
-theorem USize.size_dvd_uInt64Size : USize.size ∣ UInt64.size := by cases USize.size_eq <;> simp_all +decide
-
-@[simp] theorem mod_usizeSize_uInt8Size (n : Nat) : n % USize.size % UInt8.size = n % UInt8.size :=
-  Nat.mod_mod_of_dvd _ UInt8.size_dvd_usizeSize
-@[simp] theorem mod_usizeSize_uInt16Size (n : Nat) : n % USize.size % UInt16.size = n % UInt16.size :=
-  Nat.mod_mod_of_dvd _ UInt16.size_dvd_usizeSize
-@[simp] theorem mod_usizeSize_uInt32Size (n : Nat) : n % USize.size % UInt32.size = n % UInt32.size :=
-  Nat.mod_mod_of_dvd _ UInt32.size_dvd_usizeSize
-@[simp] theorem mod_uInt64Size_uSizeSize (n : Nat) : n % UInt64.size % USize.size = n % USize.size :=
-  Nat.mod_mod_of_dvd _ USize.size_dvd_uInt64Size
-
-@[simp] theorem UInt8.toNat_mod_size (n : UInt8) : n.toNat % UInt8.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt
-@[simp] theorem UInt8.toNat_mod_uInt16Size (n : UInt8) : n.toNat % UInt16.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
-@[simp] theorem UInt8.toNat_mod_uInt32Size (n : UInt8) : n.toNat % UInt32.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
-@[simp] theorem UInt8.toNat_mod_uInt64Size (n : UInt8) : n.toNat % UInt64.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
-@[simp] theorem UInt8.toNat_mod_uSizeSize (n : UInt8) : n.toNat % USize.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt_usizeSize
-
-@[simp] theorem UInt16.toNat_mod_size (n : UInt16) : n.toNat % UInt16.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt
-@[simp] theorem UInt16.toNat_mod_uInt32Size (n : UInt16) : n.toNat % UInt32.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
-@[simp] theorem UInt16.toNat_mod_uInt64Size (n : UInt16) : n.toNat % UInt64.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
-@[simp] theorem UInt16.toNat_mod_uSizeSize (n : UInt16) : n.toNat % USize.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt_usizeSize
-
-@[simp] theorem UInt32.toNat_mod_size (n : UInt32) : n.toNat % UInt32.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt
-@[simp] theorem UInt32.toNat_mod_uInt64Size (n : UInt32) : n.toNat % UInt64.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
-@[simp] theorem UInt32.toNat_mod_uSizeSize (n : UInt32) : n.toNat % USize.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt_usizeSize
-
-@[simp] theorem UInt64.toNat_mod_size (n : UInt64) : n.toNat % UInt64.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt
-
-@[simp] theorem USize.toNat_mod_size (n : USize) : n.toNat % USize.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt_size
-@[simp] theorem USize.toNat_mod_uInt64Size (n : USize) : n.toNat % UInt64.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt
-
-@[simp] theorem UInt8.toUInt16_mod_256 (n : UInt8) : n.toUInt16 % 256 = n.toUInt16 := UInt16.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt32_mod_256 (n : UInt8) : n.toUInt32 % 256 = n.toUInt32 := UInt32.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt64_mod_256 (n : UInt8) : n.toUInt64 % 256 = n.toUInt64 := UInt64.toNat.inj (by simp)
-@[simp] theorem UInt8.toUSize_mod_256 (n : UInt8) : n.toUSize % 256 = n.toUSize := USize.toNat.inj (by simp)
-
-@[simp] theorem UInt16.toUInt32_mod_65536 (n : UInt16) : n.toUInt32 % 65536 = n.toUInt32 := UInt32.toNat.inj (by simp)
-@[simp] theorem UInt16.toUInt64_mod_65536 (n : UInt16) : n.toUInt64 % 65536 = n.toUInt64 := UInt64.toNat.inj (by simp)
-@[simp] theorem UInt16.toUSize_mod_65536 (n : UInt16) : n.toUSize % 65536 = n.toUSize := USize.toNat.inj (by simp)
-
-@[simp] theorem UInt32.toUInt64_mod_4294967296 (n : UInt32) : n.toUInt64 % 4294967296 = n.toUInt64 := UInt64.toNat.inj (by simp)
-
 @[simp] theorem Fin.mk_uInt8ToNat (n : UInt8) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
 @[simp] theorem Fin.mk_uInt16ToNat (n : UInt16) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
 @[simp] theorem Fin.mk_uInt32ToNat (n : UInt32) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
@@ -394,14 +349,14 @@ theorem USize.size_dvd_uInt64Size : USize.size ∣ UInt64.size := by cases USize
 @[simp] theorem UInt16.toBitVec_toUInt64 (n : UInt16) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
 @[simp] theorem UInt32.toBitVec_toUInt64 (n : UInt32) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
 @[simp] theorem USize.toBitVec_toUInt64 (n : USize) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 :=
-  BitVec.eq_of_toNat_eq (by simp)
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt (USize.toNat_lt _)])
 
 @[simp] theorem UInt8.toBitVec_toUSize (n : UInt8) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
-  BitVec.eq_of_toNat_eq (by simp)
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
 @[simp] theorem UInt16.toBitVec_toUSize (n : UInt16) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
-  BitVec.eq_of_toNat_eq (by simp)
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
 @[simp] theorem UInt32.toBitVec_toUSize (n : UInt32) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
-  BitVec.eq_of_toNat_eq (by simp)
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
 @[simp] theorem UInt64.toBitVec_toUSize (n : UInt64) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
   BitVec.eq_of_toNat_eq (by simp)
 
@@ -465,321 +420,3 @@ theorem USize.ofNatLT_uInt64ToNat (n : UInt64) (h) : USize.ofNatLT n.toNat h = n
 @[simp] theorem USize.ofFin_uint8ToFin (n : UInt8) : USize.ofFin (n.toFin.castLE UInt8.size_le_usizeSize) = n.toUSize := rfl
 @[simp] theorem USize.ofFin_uint16ToFin (n : UInt16) : USize.ofFin (n.toFin.castLE UInt16.size_le_usizeSize) = n.toUSize := rfl
 @[simp] theorem USize.ofFin_uint32ToFin (n : UInt32) : USize.ofFin (n.toFin.castLE UInt32.size_le_usizeSize) = n.toUSize := rfl
-
-@[simp] theorem Nat.toUInt8_eq {n : Nat} : n.toUInt8 = UInt8.ofNat n := rfl
-@[simp] theorem Nat.toUInt16_eq {n : Nat} : n.toUInt16 = UInt16.ofNat n := rfl
-@[simp] theorem Nat.toUInt32_eq {n : Nat} : n.toUInt32 = UInt32.ofNat n := rfl
-@[simp] theorem Nat.toUInt64_eq {n : Nat} : n.toUInt64 = UInt64.ofNat n := rfl
-@[simp] theorem Nat.toUSize_eq {n : Nat} : n.toUSize = USize.ofNat n := rfl
-
-@[simp] theorem UInt8.ofBitVec_uInt16ToBitVec (n : UInt16) :
-    UInt8.ofBitVec (n.toBitVec.setWidth 8) = n.toUInt8 := rfl
-@[simp] theorem UInt8.ofBitVec_uInt32ToBitVec (n : UInt32) :
-    UInt8.ofBitVec (n.toBitVec.setWidth 8) = n.toUInt8 := rfl
-@[simp] theorem UInt8.ofBitVec_uInt64ToBitVec (n : UInt64) :
-    UInt8.ofBitVec (n.toBitVec.setWidth 8) = n.toUInt8 := rfl
-@[simp] theorem UInt8.ofBitVec_uSizeToBitVec (n : USize) :
-    UInt8.ofBitVec (n.toBitVec.setWidth 8) = n.toUInt8 := UInt8.toNat.inj (by simp)
-
-@[simp] theorem UInt16.ofBitVec_uInt8ToBitVec (n : UInt8) :
-    UInt16.ofBitVec (n.toBitVec.setWidth 16) = n.toUInt16 := rfl
-@[simp] theorem UInt16.ofBitVec_uInt32ToBitVec (n : UInt32) :
-    UInt16.ofBitVec (n.toBitVec.setWidth 16) = n.toUInt16 := rfl
-@[simp] theorem UInt16.ofBitVec_uInt64ToBitVec (n : UInt64) :
-    UInt16.ofBitVec (n.toBitVec.setWidth 16) = n.toUInt16 := rfl
-@[simp] theorem UInt16.ofBitVec_uSizeToBitVec (n : USize) :
-    UInt16.ofBitVec (n.toBitVec.setWidth 16) = n.toUInt16 := UInt16.toNat.inj (by simp)
-
-@[simp] theorem UInt32.ofBitVec_uInt8ToBitVec (n : UInt8) :
-    UInt32.ofBitVec (n.toBitVec.setWidth 32) = n.toUInt32 := rfl
-@[simp] theorem UInt32.ofBitVec_uInt16ToBitVec (n : UInt16) :
-    UInt32.ofBitVec (n.toBitVec.setWidth 32) = n.toUInt32 := rfl
-@[simp] theorem UInt32.ofBitVec_uInt64ToBitVec (n : UInt64) :
-    UInt32.ofBitVec (n.toBitVec.setWidth 32) = n.toUInt32 := rfl
-@[simp] theorem UInt32.ofBitVec_uSizeToBitVec (n : USize) :
-    UInt32.ofBitVec (n.toBitVec.setWidth 32) = n.toUInt32 := UInt32.toNat.inj (by simp)
-
-@[simp] theorem UInt64.ofBitVec_uInt8ToBitVec (n : UInt8) :
-    UInt64.ofBitVec (n.toBitVec.setWidth 64) = n.toUInt64 := rfl
-@[simp] theorem UInt64.ofBitVec_uInt16ToBitVec (n : UInt16) :
-    UInt64.ofBitVec (n.toBitVec.setWidth 64) = n.toUInt64 := rfl
-@[simp] theorem UInt64.ofBitVec_uInt32ToBitVec (n : UInt32) :
-    UInt64.ofBitVec (n.toBitVec.setWidth 64) = n.toUInt64 := rfl
-@[simp] theorem UInt64.ofBitVec_uSizeToBitVec (n : USize) :
-    UInt64.ofBitVec (n.toBitVec.setWidth 64) = n.toUInt64 :=
-  UInt64.toNat.inj (by simp)
-
-@[simp] theorem USize.ofBitVec_uInt8ToBitVec (n : UInt8) :
-    USize.ofBitVec (n.toBitVec.setWidth System.Platform.numBits) = n.toUSize :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.ofBitVec_uInt16ToBitVec (n : UInt16) :
-    USize.ofBitVec (n.toBitVec.setWidth System.Platform.numBits) = n.toUSize :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.ofBitVec_uInt32ToBitVec (n : UInt32) :
-    USize.ofBitVec (n.toBitVec.setWidth System.Platform.numBits) = n.toUSize :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.ofBitVec_uInt64ToBitVec (n : UInt64) :
-    USize.ofBitVec (n.toBitVec.setWidth System.Platform.numBits) = n.toUSize :=
-  USize.toNat.inj (by simp)
-
-@[simp] theorem UInt8.ofNat_uInt16ToNat (n : UInt16) : UInt8.ofNat n.toNat = n.toUInt8 := rfl
-@[simp] theorem UInt8.ofNat_uInt32ToNat (n : UInt32) : UInt8.ofNat n.toNat = n.toUInt8 := rfl
-@[simp] theorem UInt8.ofNat_uInt64ToNat (n : UInt64) : UInt8.ofNat n.toNat = n.toUInt8 := rfl
-@[simp] theorem UInt8.ofNat_uSizeToNat (n : USize) : UInt8.ofNat n.toNat = n.toUInt8 := rfl
-
-@[simp] theorem UInt16.ofNat_uInt8ToNat (n : UInt8) : UInt16.ofNat n.toNat = n.toUInt16 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt16.ofNat_uInt32ToNat (n : UInt32) : UInt16.ofNat n.toNat = n.toUInt16 := rfl
-@[simp] theorem UInt16.ofNat_uInt64ToNat (n : UInt64) : UInt16.ofNat n.toNat = n.toUInt16 := rfl
-@[simp] theorem UInt16.ofNat_uSizeToNat (n : USize) : UInt16.ofNat n.toNat = n.toUInt16 := rfl
-
-@[simp] theorem UInt32.ofNat_uInt8ToNat (n : UInt8) : UInt32.ofNat n.toNat = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem UInt32.ofNat_uInt16ToNat (n : UInt16) : UInt32.ofNat n.toNat = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem UInt32.ofNat_uInt64ToNat (n : UInt64) : UInt32.ofNat n.toNat = n.toUInt32 := rfl
-@[simp] theorem UInt32.ofNat_uSizeToNat (n : USize) : UInt32.ofNat n.toNat = n.toUInt32 := rfl
-
-@[simp] theorem UInt64.ofNat_uInt8ToNat (n : UInt8) : UInt64.ofNat n.toNat = n.toUInt64 :=
-  UInt64.toNat.inj (by simp)
-@[simp] theorem UInt64.ofNat_uInt16ToNat (n : UInt16) : UInt64.ofNat n.toNat = n.toUInt64 :=
-  UInt64.toNat.inj (by simp)
-@[simp] theorem UInt64.ofNat_uInt32ToNat (n : UInt32) : UInt64.ofNat n.toNat = n.toUInt64 :=
-  UInt64.toNat.inj (by simp)
-@[simp] theorem UInt64.ofNat_uSizeToNat (n : USize) : UInt64.ofNat n.toNat = n.toUInt64 :=
-  UInt64.toNat.inj (by simp)
-
-@[simp] theorem USize.ofNat_uInt8ToNat (n : UInt8) : USize.ofNat n.toNat = n.toUSize :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.ofNat_uInt16ToNat (n : UInt16) : USize.ofNat n.toNat = n.toUSize :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.ofNat_uInt32ToNat (n : UInt32) : USize.ofNat n.toNat = n.toUSize :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.ofNat_uInt64ToNat (n : UInt64) : USize.ofNat n.toNat = n.toUSize :=
-  USize.toNat.inj (by simp)
-
-theorem UInt8.ofNatLT_eq_ofNat (n : Nat) {h} : UInt8.ofNatLT n h = UInt8.ofNat n :=
-  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt16.ofNatLT_eq_ofNat (n : Nat) {h} : UInt16.ofNatLT n h = UInt16.ofNat n :=
-  UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt32.ofNatLT_eq_ofNat (n : Nat) {h} : UInt32.ofNatLT n h = UInt32.ofNat n :=
-  UInt32.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt64.ofNatLT_eq_ofNat (n : Nat) {h} : UInt64.ofNatLT n h = UInt64.ofNat n :=
-  UInt64.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem USize.ofNatLT_eq_ofNat (n : Nat) {h} : USize.ofNatLT n h = USize.ofNat n :=
-  USize.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-
-theorem UInt8.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < UInt8.size) :
-    UInt8.ofNatTruncate n = UInt8.ofNat n := by
-  simp [ofNatTruncate, hn, UInt8.ofNatLT_eq_ofNat]
-theorem UInt16.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < UInt16.size) :
-    UInt16.ofNatTruncate n = UInt16.ofNat n := by
-  simp [ofNatTruncate, hn, UInt16.ofNatLT_eq_ofNat]
-theorem UInt32.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < UInt32.size) :
-    UInt32.ofNatTruncate n = UInt32.ofNat n := by
-  simp [ofNatTruncate, hn, UInt32.ofNatLT_eq_ofNat]
-theorem UInt64.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < UInt64.size) :
-    UInt64.ofNatTruncate n = UInt64.ofNat n := by
-  simp [ofNatTruncate, hn, UInt64.ofNatLT_eq_ofNat]
-theorem USize.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < USize.size) :
-    USize.ofNatTruncate n = USize.ofNat n := by
-  simp [ofNatTruncate, hn, USize.ofNatLT_eq_ofNat]
-
-@[simp] theorem UInt8.ofNatTruncate_toNat (n : UInt8) : UInt8.ofNatTruncate n.toNat = n := by
-  rw [UInt8.ofNatTruncate_eq_ofNat] <;> simp [n.toNat_lt]
-
-@[simp] theorem UInt16.ofNatTruncate_uInt8ToNat (n : UInt8) : UInt16.ofNatTruncate n.toNat = n.toUInt16 := by
-  rw [UInt16.ofNatTruncate_eq_ofNat, ofNat_uInt8ToNat]
-  exact Nat.lt_trans (n.toNat_lt) (by decide)
-@[simp] theorem UInt16.ofNatTruncate_toNat (n : UInt16) : UInt16.ofNatTruncate n.toNat = n := by
-  rw [UInt16.ofNatTruncate_eq_ofNat] <;> simp [n.toNat_lt]
-
-@[simp] theorem UInt32.ofNatTruncate_uInt8ToNat (n : UInt8) : UInt32.ofNatTruncate n.toNat = n.toUInt32 := by
-  rw [UInt32.ofNatTruncate_eq_ofNat, ofNat_uInt8ToNat]
-  exact Nat.lt_trans (n.toNat_lt) (by decide)
-@[simp] theorem UInt32.ofNatTruncate_uInt16ToNat (n : UInt16) : UInt32.ofNatTruncate n.toNat = n.toUInt32 := by
-  rw [UInt32.ofNatTruncate_eq_ofNat, ofNat_uInt16ToNat]
-  exact Nat.lt_trans (n.toNat_lt) (by decide)
-@[simp] theorem UInt32.ofNatTruncate_toNat (n : UInt32) : UInt32.ofNatTruncate n.toNat = n := by
-  rw [UInt32.ofNatTruncate_eq_ofNat] <;> simp [n.toNat_lt]
-
-@[simp] theorem UInt64.ofNatTruncate_uInt8ToNat (n : UInt8) : UInt64.ofNatTruncate n.toNat = n.toUInt64 := by
-  rw [UInt64.ofNatTruncate_eq_ofNat, ofNat_uInt8ToNat]
-  exact Nat.lt_trans (n.toNat_lt) (by decide)
-@[simp] theorem UInt64.ofNatTruncate_uInt16ToNat (n : UInt16) : UInt64.ofNatTruncate n.toNat = n.toUInt64 := by
-  rw [UInt64.ofNatTruncate_eq_ofNat, ofNat_uInt16ToNat]
-  exact Nat.lt_trans (n.toNat_lt) (by decide)
-@[simp] theorem UInt64.ofNatTruncate_uInt32ToNat (n : UInt32) : UInt64.ofNatTruncate n.toNat = n.toUInt64 := by
-  rw [UInt64.ofNatTruncate_eq_ofNat, ofNat_uInt32ToNat]
-  exact Nat.lt_trans (n.toNat_lt) (by decide)
-@[simp] theorem UInt64.ofNatTruncate_toNat (n : UInt64) : UInt64.ofNatTruncate n.toNat = n := by
-  rw [UInt64.ofNatTruncate_eq_ofNat] <;> simp [n.toNat_lt]
-@[simp] theorem UInt64.ofNatTruncate_uSizeToNat (n : USize) : UInt64.ofNatTruncate n.toNat = n.toUInt64 := by
-  rw [UInt64.ofNatTruncate_eq_ofNat, ofNat_uSizeToNat]
-  exact n.toNat_lt
-
-@[simp] theorem USize.ofNatTruncate_uInt8ToNat (n : UInt8) : USize.ofNatTruncate n.toNat = n.toUSize := by
-  rw [USize.ofNatTruncate_eq_ofNat, ofNat_uInt8ToNat]
-  exact n.toNat_lt_usizeSize
-@[simp] theorem USize.ofNatTruncate_uInt16ToNat (n : UInt16) : USize.ofNatTruncate n.toNat = n.toUSize := by
-  rw [USize.ofNatTruncate_eq_ofNat, ofNat_uInt16ToNat]
-  exact n.toNat_lt_usizeSize
-@[simp] theorem USize.ofNatTruncate_uInt32ToNat (n : UInt32) : USize.ofNatTruncate n.toNat = n.toUSize := by
-  rw [USize.ofNatTruncate_eq_ofNat, ofNat_uInt32ToNat]
-  exact n.toNat_lt_usizeSize
-@[simp] theorem USize.ofNatTruncate_toNat (n : USize) : USize.ofNatTruncate n.toNat = n := by
-  rw [USize.ofNatTruncate_eq_ofNat] <;> simp [n.toNat_lt_size]
-
-@[simp] theorem UInt8.toUInt8_toUInt16 (n : UInt8) : n.toUInt16.toUInt8 = n :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt8_toUInt32 (n : UInt8) : n.toUInt32.toUInt8 = n :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt8_toUInt64 (n : UInt8) : n.toUInt64.toUInt8 = n :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt8_toUSize (n : UInt8) : n.toUSize.toUInt8 = n :=
-  UInt8.toNat.inj (by simp)
-
-@[simp] theorem UInt8.toUInt16_toUInt32 (n : UInt8) : n.toUInt32.toUInt16 = n.toUInt16 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt16_toUInt64 (n : UInt8) : n.toUInt64.toUInt16 = n.toUInt16 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt16_toUSize (n : UInt8) : n.toUSize.toUInt16 = n.toUInt16 :=
-  UInt16.toNat.inj (by simp)
-
-@[simp] theorem UInt8.toUInt32_toUInt16 (n : UInt8) : n.toUInt16.toUInt32 = n.toUInt32 := rfl
-@[simp] theorem UInt8.toUInt32_toUInt64 (n : UInt8) : n.toUInt64.toUInt32 = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem UInt8.toUInt32_toUSize (n : UInt8) : n.toUSize.toUInt32 = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-
-@[simp] theorem UInt8.toUInt64_toUInt16 (n : UInt8) : n.toUInt16.toUInt64 = n.toUInt64 := rfl
-@[simp] theorem UInt8.toUInt64_toUInt32 (n : UInt8) : n.toUInt32.toUInt64 = n.toUInt64 := rfl
-@[simp] theorem UInt8.toUInt64_toUSize (n : UInt8) : n.toUSize.toUInt64 = n.toUInt64 := rfl
-
-@[simp] theorem UInt8.toUSize_toUInt16 (n : UInt8) : n.toUInt16.toUSize = n.toUSize := rfl
-@[simp] theorem UInt8.toUSize_toUInt32 (n : UInt8) : n.toUInt32.toUSize = n.toUSize := rfl
-@[simp] theorem UInt8.toUSize_toUInt64 (n : UInt8) : n.toUInt64.toUSize = n.toUSize :=
-  USize.toNat.inj (by simp)
-
-@[simp] theorem UInt16.toUInt8_toUInt32 (n : UInt16) : n.toUInt32.toUInt8 = n.toUInt8 := rfl
-@[simp] theorem UInt16.toUInt8_toUInt64 (n : UInt16) : n.toUInt64.toUInt8 = n.toUInt8 := rfl
-@[simp] theorem UInt16.toUInt8_toUSize (n : UInt16) : n.toUSize.toUInt8 = n.toUInt8 := rfl
-
-@[simp] theorem UInt16.toUInt16_toUInt8 (n : UInt16) : n.toUInt8.toUInt16 = n % 256 := rfl
-@[simp] theorem UInt16.toUInt16_toUInt32 (n : UInt16) : n.toUInt32.toUInt16 = n :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt16.toUInt16_toUInt64 (n : UInt16) : n.toUInt64.toUInt16 = n :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt16.toUInt16_toUSize (n : UInt16) : n.toUSize.toUInt16 = n :=
-  UInt16.toNat.inj (by simp)
-
-@[simp] theorem UInt16.toUInt32_toUInt8 (n : UInt16) : n.toUInt8.toUInt32 = n.toUInt32 % 256 := rfl
-@[simp] theorem UInt16.toUInt32_toUInt64 (n : UInt16) : n.toUInt64.toUInt32 = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem UInt16.toUInt32_toUSize (n : UInt16) : n.toUSize.toUInt32 = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-
-@[simp] theorem UInt16.toUInt64_toUInt8 (n : UInt16) : n.toUInt8.toUInt64 = n.toUInt64 % 256 := rfl
-@[simp] theorem UInt16.toUInt64_toUInt32 (n : UInt16) : n.toUInt32.toUInt64 = n.toUInt64 := rfl
-@[simp] theorem UInt16.toUInt64_toUSize (n : UInt16) : n.toUSize.toUInt64 = n.toUInt64 := rfl
-
-@[simp] theorem UInt16.toUSize_toUInt8 (n : UInt16) : n.toUInt8.toUSize = n.toUSize % 256 :=
-  USize.toNat.inj (by simp)
-@[simp] theorem UInt16.toUSize_toUInt32 (n : UInt16) : n.toUInt32.toUSize = n.toUSize :=
-  USize.toNat.inj (by simp)
-@[simp] theorem UInt16.toUSize_toUInt64 (n : UInt16) : n.toUInt64.toUSize = n.toUSize :=
-  USize.toNat.inj (by simp)
-
-@[simp] theorem UInt32.toUInt8_toUInt16 (n : UInt32) : n.toUInt16.toUInt8 = n.toUInt8 :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem UInt32.toUInt8_toUInt64 (n : UInt32) : n.toUInt64.toUInt8 = n.toUInt8 := rfl
-@[simp] theorem UInt32.toUInt8_toUSize (n : UInt32) : n.toUSize.toUInt8 = n.toUInt8 := rfl
-
-@[simp] theorem UInt32.toUInt16_toUInt8 (n : UInt32) : n.toUInt8.toUInt16 = n.toUInt16 % 256 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt32.toUInt16_toUInt64 (n : UInt32) : n.toUInt64.toUInt16 = n.toUInt16 := rfl
-@[simp] theorem UInt32.toUInt16_toUSize (n : UInt32) : n.toUSize.toUInt16 = n.toUInt16 := rfl
-
-@[simp] theorem UInt32.toUInt32_toUInt8 (n : UInt32) : n.toUInt8.toUInt32 = n % 256 := rfl
-@[simp] theorem UInt32.toUInt32_toUInt16 (n : UInt32) : n.toUInt16.toUInt32 = n % 65536 := rfl
-@[simp] theorem UInt32.toUInt32_toUInt64 (n : UInt32) : n.toUInt64.toUInt32 = n :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem UInt32.toUInt32_toUSize (n : UInt32) : n.toUSize.toUInt32 = n :=
-  UInt32.toNat.inj (by simp)
-
-@[simp] theorem UInt32.toUInt64_toUInt8 (n : UInt32) : n.toUInt8.toUInt64 = n.toUInt64 % 256 := rfl
-@[simp] theorem UInt32.toUInt64_toUInt16 (n : UInt32) : n.toUInt16.toUInt64 = n.toUInt64 % 65536 := rfl
-@[simp] theorem UInt32.toUInt64_toUSize (n : UInt32) : n.toUSize.toUInt64 = n.toUInt64 := rfl
-
-@[simp] theorem UInt32.toUSize_toUInt8 (n : UInt32) : n.toUInt8.toUSize = n.toUSize % 256 :=
-  USize.toNat.inj (by simp)
-@[simp] theorem UInt32.toUSize_toUInt16 (n : UInt32) : n.toUInt16.toUSize = n.toUSize % 65536 :=
-  USize.toNat.inj (by simp)
-@[simp] theorem UInt32.toUSize_toUInt64 (n : UInt32) : n.toUInt64.toUSize = n.toUSize :=
-  USize.toNat.inj (by simp)
-
-@[simp] theorem UInt64.toUInt8_toUInt16 (n : UInt64) : n.toUInt16.toUInt8 = n.toUInt8 :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem UInt64.toUInt8_toUInt32 (n : UInt64) : n.toUInt32.toUInt8 = n.toUInt8 :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem UInt64.toUInt8_toUSize (n : UInt64) : n.toUSize.toUInt8 = n.toUInt8 :=
-  UInt8.toNat.inj (by simp)
-
-@[simp] theorem UInt64.toUInt16_toUInt8 (n : UInt64) : n.toUInt8.toUInt16 = n.toUInt16 % 256 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt64.toUInt16_toUInt32 (n : UInt64) : n.toUInt32.toUInt16 = n.toUInt16 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem UInt64.toUInt16_toUSize (n : UInt64) : n.toUSize.toUInt16 = n.toUInt16 :=
-  UInt16.toNat.inj (by simp)
-
-@[simp] theorem UInt64.toUInt32_toUInt8 (n : UInt64) : n.toUInt8.toUInt32 = n.toUInt32 % 256 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem UInt64.toUInt32_toUInt16 (n : UInt64) : n.toUInt16.toUInt32 = n.toUInt32 % 65536 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem UInt64.toUInt32_toUSize (n : UInt64) : n.toUSize.toUInt32 = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-
-@[simp] theorem UInt64.toUInt64_toUInt8 (n : UInt64) : n.toUInt8.toUInt64 = n % 256 := rfl
-@[simp] theorem UInt64.toUInt64_toUInt16 (n : UInt64) : n.toUInt16.toUInt64 = n % 65536 := rfl
-@[simp] theorem UInt64.toUInt64_toUInt32 (n : UInt64) : n.toUInt32.toUInt64 = n % 4294967296 := rfl
-
-@[simp] theorem UInt64.toUSize_toUInt8 (n : UInt64) : n.toUInt8.toUSize = n.toUSize % 256 :=
-  USize.toNat.inj (by simp)
-@[simp] theorem UInt64.toUSize_toUInt16 (n : UInt64) : n.toUInt16.toUSize = n.toUSize % 65536 :=
-  USize.toNat.inj (by simp)
-
-@[simp] theorem USize.toUInt8_toUInt16 (n : USize) : n.toUInt16.toUInt8 = n.toUInt8 :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem USize.toUInt8_toUInt32 (n : USize) : n.toUInt32.toUInt8 = n.toUInt8 :=
-  UInt8.toNat.inj (by simp)
-@[simp] theorem USize.toUInt8_toUInt64 (n : USize) : n.toUInt64.toUInt8 = n.toUInt8 := rfl
-
-@[simp] theorem USize.toUInt16_toUInt8 (n : USize) : n.toUInt8.toUInt16 = n.toUInt16 % 256 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem USize.toUInt16_toUInt32 (n : USize) : n.toUInt32.toUInt16 = n.toUInt16 :=
-  UInt16.toNat.inj (by simp)
-@[simp] theorem USize.toUInt16_toUInt64 (n : USize) : n.toUInt64.toUInt16 = n.toUInt16 := rfl
-
-@[simp] theorem USize.toUInt64_toUInt8 (n : USize) : n.toUInt8.toUInt64 = n.toUInt64 % 256 := rfl
-@[simp] theorem USize.toUInt64_toUInt16 (n : USize) : n.toUInt16.toUInt64 = n.toUInt64 % 65536 := rfl
-
-@[simp] theorem USize.toUInt32_toUInt8 (n : USize) : n.toUInt8.toUInt32 = n.toUInt32 % 256 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem USize.toUInt32_toUInt16 (n : USize) : n.toUInt16.toUInt32 = n.toUInt32 % 65536 :=
-  UInt32.toNat.inj (by simp)
-@[simp] theorem USize.toUInt32_toUInt64 (n : USize) : n.toUInt64.toUInt32 = n.toUInt32 :=
-  UInt32.toNat.inj (by simp)
-
-@[simp] theorem USize.toUSize_toUInt8 (n : USize) : n.toUInt8.toUSize = n % 256 :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.toUSize_toUInt16 (n : USize) : n.toUInt16.toUSize = n % 65536 :=
-  USize.toNat.inj (by simp)
-@[simp] theorem USize.toUSize_toUInt64 (n : USize) : n.toUInt64.toUSize = n :=
-  USize.toNat.inj (by simp)
-
--- Note: we are currently missing the following four results for which there does not seem to
--- be a good candidate for the RHS:
--- @[simp] theorem UInt64.toUInt64_toUSize (n : UInt64) : n.toUSize.toUInt64 = ? :=
--- @[simp] theorem UInt64.toUSize_toUInt32 (n : UInt64) : n.toUInt32.toUSize = ? :=
--- @[simp] theorem USize.toUInt64_toUInt32 (n : USize) : n.toUInt32.toUInt64 = ? :=
--- @[simp] theorem USize.toUSize_toUInt32 (n : USize) : n.toInt32.toUSize = ? :=

src/Init/Grind/Lemmas.lean

@@ -69,11 +69,6 @@ theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by s
 theorem eq_congr  {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*]
 theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)]
 
-/-! Ne -/
-
-theorem ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := by simp [*]
-theorem ne_of_ne_of_eq_right {α : Sort u} {a b c : α} (h₁ : a = c) (h₂ : b ≠ c) : b ≠ a := by simp [*]
-
 /-! Bool.and -/
 
 theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h]

src/Init/Omega/Constraint.lean

@@ -181,13 +181,13 @@ theorem combo_sat (a) (w₁ : c₁.sat x₁) (b) (w₂ : c₂.sat x₂) :
 
 /-- The conjunction of two constraints. -/
 def combine (x y : Constraint) : Constraint where
-  lowerBound := Option.merge max x.lowerBound y.lowerBound
-  upperBound := Option.merge min x.upperBound y.upperBound
+  lowerBound := max x.lowerBound y.lowerBound
+  upperBound := min x.upperBound y.upperBound
 
 theorem combine_sat : (c : Constraint) → (c' : Constraint) → (t : Int) →
     (c.combine c').sat t = (c.sat t ∧ c'.sat t) := by
   rintro ⟨_ | l₁, _ | u₁⟩ <;> rintro ⟨_ | l₂, _ | u₂⟩ t
-    <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le, Option.merge] at *
+    <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le] at *
   · rw [And.comm]
   · rw [← and_assoc, And.comm (a := l₂ ≤ t), and_assoc]
   · rw [and_assoc]

src/Lean/Elab/Tactic/Induction.lean

@@ -173,10 +173,6 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
           addNewArg arg
       loop
     | _ =>
-      let s ← get
-      let ctx ← read
-      unless s.targetPos = ctx.targets.size do
-        throwError "unexpected number of targets for '{elimInfo.elimExpr}'"
       pure ()
   let (_, s) ← (loop).run { elimInfo := elimInfo, targets := targets }
     |>.run { f := elimInfo.elimExpr, fType := elimInfo.elimType, motive := none }

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -24,70 +24,28 @@ Implementation of the `exact?` tactic.
 def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
     TacticM Unit := do
   let mvar ← getMainGoal
-  let initialState ← saveState
   let (_, goal) ← (← getMainGoal).intros
   goal.withContext do
     let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
     let tactic := fun exfalso =>
-      solveByElim required (exfalso := exfalso) (maxDepth := 6)
+          solveByElim required (exfalso := exfalso) (maxDepth := 6)
     let allowFailure := fun g => do
       let g ← g.withContext (instantiateMVars (.mvar g))
       return required.all fun e => e.occurs g
-    match (← librarySearch goal tactic allowFailure) with
+    match ← librarySearch goal tactic allowFailure with
     -- Found goal that closed problem
     | none =>
-      addSuggestionIfValid ref mvar initialState
+      addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
     -- Found suggestions
     | some suggestions =>
-      if requireClose then
-        let hint := if suggestions.isEmpty then "" else " Try `apply?` to see partial suggestions."
-        throwError "`exact?` could not close the goal.{hint}"
+      if requireClose then throwError
+        "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
       reportOutOfHeartbeats `apply? ref
       for (_, suggestionMCtx) in suggestions do
         withMCtx suggestionMCtx do
-          addSuggestionIfValid ref mvar initialState (addSubgoalsMsg := true) (errorOnInvalid := false)
+          addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
       if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
       admitGoal goal
-where
-  /--
-  Executes `tac` in `savedState` (then restores the current state). Used to ensure that a suggested
-  tactic is valid.
-
-  Remark: we don't merely elaborate the proof term's syntax because it may successfully round-trip
-  (d)elaboration but still produce an invalid tactic (see the example in #5407).
-  -/
-  evalTacticWithState (savedState : Tactic.SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
-    let currState ← saveState
-    savedState.restore
-    try
-      Term.withoutErrToSorry <| withoutRecover <| evalTactic tac
-    finally
-      currState.restore
-
-  /--
-  Suggests using the value of `goal` as a proof term if the corresponding tactic is valid at
-  `origGoal`, or else informs the user that a proof exists but is not syntactically valid.
-  -/
-  addSuggestionIfValid (ref : Syntax) (goal : MVarId) (initialState : Tactic.SavedState)
-                       (addSubgoalsMsg := false) (errorOnInvalid := true) : TacticM Unit := do
-    let proofExpr := (← instantiateMVars (mkMVar goal)).headBeta
-    let proofMVars ← getMVars proofExpr
-    let hasMVars := !proofMVars.isEmpty
-    let suggestion ← mkExactSuggestionSyntax proofExpr (useRefine := hasMVars) (exposeNames := false)
-    let mut exposeNames := false
-    try evalTacticWithState initialState suggestion
-    catch _ =>
-      exposeNames := true
-      let suggestion' ← mkExactSuggestionSyntax proofExpr (useRefine := hasMVars) (exposeNames := true)
-      try evalTacticWithState initialState suggestion'
-      catch _ =>
-        let suggestionStr ← SuggestionText.prettyExtra suggestion
-        -- Pretty-print the version without `expose_names` so variable names match the Infoview
-        let msg := m!"found a {if hasMVars then "partial " else ""}proof, \
-                      but the corresponding tactic failed:{indentD suggestionStr}"
-        if errorOnInvalid then throwError msg else logInfo msg
-        return
-    addExactSuggestion ref proofExpr (addSubgoalsMsg := addSubgoalsMsg) (exposeNames := exposeNames)
 
 @[builtin_tactic Lean.Parser.Tactic.exact?]
 def evalExact : Tactic := fun stx => do
@@ -111,7 +69,7 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     introdGoal.withContext do
       if let some suggestions ← librarySearch introdGoal then
         if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
-        else logError "`exact?%` could not close the goal. Try `by apply?` to see partial suggestions."
+        else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
         mkLabeledSorry expectedType (synthetic := true) (unique := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta

src/Lean/Elab/Tactic/Try.lean

@@ -48,6 +48,14 @@ private def isExprAccessible (e : Expr) : MetaM Bool := do
   let (_, s) ← e.collectFVars |>.run {}
   s.fvarIds.allM isAccessible
 
+/-- Creates a temporary local context where all names are exposed, and executes `k`-/
+private def withExposedNames (k : MetaM α) : MetaM α := do
+  withNewMCtxDepth do
+    -- Create a helper goal to apply
+    let mvarId := (← mkFreshExprMVar (mkConst ``True)).mvarId!
+    let mvarId ← mvarId.exposeNames
+    mvarId.withContext do k
+
 /-- Executes `tac` in the saved state. This function is used to validate a tactic before suggesting it. -/
 def checkTactic (savedState : SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
   let currState ← saveState

src/Lean/Message.lean

@@ -241,11 +241,6 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
   | nCtx, ctx,       compose d₁ d₂            => return (← formatAux nCtx ctx d₁) ++ (← formatAux nCtx ctx d₂)
   | nCtx, ctx,       group d                  => Format.group <$> formatAux nCtx ctx d
   | nCtx, ctx,       trace data header children => do
-    let childFmts ← children.mapM (formatAux nCtx ctx)
-    if data.cls.isAnonymous then
-      -- Sequence of top-level traces collected by `addTraceAsMessages`, do not indent.
-      return .joinSep childFmts.toList "\n"
-
     let mut msg := f!"[{data.cls}]"
     if data.startTime != 0 then
       msg := f!"{msg} [{data.stopTime - data.startTime}]"
@@ -255,6 +250,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
       if maxNum > 0 && children.size > maxNum then
         children := children.take maxNum |>.push <|
           ofFormat f!"{children.size - maxNum} more entries... (increase `maxTraceChildren` to see more)"
+    let childFmts ← children.mapM (formatAux nCtx ctx)
     return .nest 2 (.joinSep (msg::childFmts.toList) "\n")
   | nCtx, ctx?,      ofLazy pp _             => do
     let dyn ← pp (ctx?.map (mkPPContext nCtx))

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -120,8 +120,6 @@ where
       else
         collect (b.instantiate1 (← mkFreshExprMVar d)) (argIdx+1) targetIdx implicits targets'
     | _ =>
-      unless targetIdx = targets.size do
-        throwError "extra targets for '{elimInfo.elimExpr}'"
       return (implicits, targets')
 
 structure CustomEliminator where

src/Lean/Meta/Tactic/ExposeNames.lean

@@ -7,13 +7,15 @@ prelude
 import Lean.Meta.Tactic.Util
 
 namespace Lean.Meta
-
-/-- Returns a copy of the local context in which all declarations have clear, accessible names. -/
-private def getLCtxWithExposedNames : MetaM LocalContext := do
+/--
+Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
+If no local declarations require renaming, the original goal is returned unchanged.
+-/
+def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  mvarId.checkNotAssigned `expose_names
   let mut map : Std.HashMap Name FVarId := {}
   let mut toRename := #[]
-  let mut lctx ← getLCtx
-  for localDecl in lctx do
+  for localDecl in (← getLCtx) do
     let userName := localDecl.userName
     if userName.hasMacroScopes then
       toRename := toRename.push localDecl.fvarId
@@ -23,8 +25,9 @@ private def getLCtxWithExposedNames : MetaM LocalContext := do
         toRename := toRename.push fvarId
       map := map.insert userName localDecl.fvarId
   if toRename.isEmpty then
-    return lctx
+    return mvarId
   let mut next : Std.HashMap Name Nat := {}
+  let mut lctx ← getLCtx
   -- Remark: Shadowed variables may be inserted later.
   toRename := toRename.qsort fun fvarId₁ fvarId₂ =>
     (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index
@@ -46,21 +49,8 @@ private def getLCtxWithExposedNames : MetaM LocalContext := do
     next := next.insert baseName i
     map := map.insert userName fvarId
     lctx := lctx.modifyLocalDecl fvarId (·.setUserName userName)
-  return lctx
-
-/--
-Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
-If no local declarations require renaming, the original goal is returned unchanged.
--/
-def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
-  mvarId.checkNotAssigned `expose_names
-  let lctx ← getLCtxWithExposedNames
   let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) (← mvarId.getType) .syntheticOpaque (← mvarId.getTag)
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
-/-- Creates a temporary local context where all names are exposed, and executes `k` -/
-def withExposedNames (k : MetaM α) : MetaM α := do
-  withNewMCtxDepth <| withLCtx (← getLCtxWithExposedNames) (← getLocalInstances) k
-
 end Lean.Meta

src/Lean/Meta/Tactic/Grind.lean

@@ -28,7 +28,6 @@ import Lean.Meta.Tactic.Grind.Arith
 import Lean.Meta.Tactic.Grind.Ext
 import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
-import Lean.Meta.Tactic.Grind.Diseq
 
 namespace Lean
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean

@@ -43,7 +43,4 @@ builtin_initialize registerTraceClass `grind.cutsat.le.upper (inherited := true)
 builtin_initialize registerTraceClass `grind.cutsat.assign
 builtin_initialize registerTraceClass `grind.cutsat.conflict
 
-builtin_initialize registerTraceClass `grind.debug.cutsat.eq
-builtin_initialize registerTraceClass `grind.debug.cutsat.diseq
-
 end Lean

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -151,16 +151,14 @@ private def exprAsPoly (a : Expr) : GoalM Poly := do
 
 @[export lean_process_cutsat_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
-  trace[grind.debug.cutsat.eq] "{a} = {b}"
   let p₁ ← exprAsPoly a
   let p₂ ← exprAsPoly b
   let p := p₁.combine (p₂.mul (-1))
   let c ← mkEqCnstr p (.core p₁ p₂ (← mkEqProof a b))
   c.assert
 
-@[export lean_process_cutsat_eq_lit]
+@[export lean_process_new_cutsat_lit]
 def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
-  trace[grind.debug.cutsat.eq] "{a} = {ke}"
   let some k ← getIntValue? ke | return ()
   let p₁ ← exprAsPoly a
   let h ← mkEqProof a ke
@@ -172,11 +170,6 @@ def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
     mkEqCnstr p (.core p₁ p₂ h)
   c.assert
 
-@[export lean_process_cutsat_diseq]
-def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
-  trace[grind.debug.cutsat.diseq] "{a} ≠ {b}"
-  -- TODO
-
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where
   | add | mul | num

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -124,13 +124,10 @@ private def propagateCutsatEq (rhsRoot lhsRoot : ENode) : GoalM Unit := do
       -- We have to retrieve the node because other fields have been updated
       let rhsRoot ← getENode rhsRoot.self
       setENode rhsRoot.self { rhsRoot with cutsat? := lhsCutsat }
-      propagateCutsatDiseqs rhsRoot.self
   | none =>
+    if isIntNum lhsRoot.self then
     if let some rhsCutsat := rhsRoot.cutsat? then
-      if isIntNum lhsRoot.self then
-        Arith.Cutsat.processNewEqLit rhsCutsat lhsRoot.self
-      else
-        propagateCutsatDiseqs lhsRoot.self
+      Arith.Cutsat.processNewEqLit rhsCutsat lhsRoot.self
 
 /--
 Tries to apply beta-reductiong using the parent applications of the functions in `fns` with
@@ -228,12 +225,12 @@ where
     }
     propagateBeta lams₁ fns₁
     propagateBeta lams₂ fns₂
-    propagateOffsetEq rhsRoot lhsRoot
-    propagateCutsatEq rhsRoot lhsRoot
     resetParentsOf lhsRoot.self
     copyParentsTo parents rhsNode.root
     unless (← isInconsistent) do
       updateMT rhsRoot.self
+    propagateOffsetEq rhsRoot lhsRoot
+    propagateCutsatEq rhsRoot lhsRoot
     unless (← isInconsistent) do
       for parent in parents do
         propagateUp parent

src/Lean/Meta/Tactic/Grind/Diseq.lean

@@ -1,81 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind.Lemmas
-import Lean.Meta.Tactic.Grind.Types
-
-namespace Lean.Meta.Grind
-
-/--
-Returns `some (c = d)` if
-- `c = d` and `False` are in the same equivalence class, and
-- `a` (`b`) and `c` are in the same equivalence class, and
-- `b` (`a`) and `d` are in the same equivalence class.
-Otherwise return `none`.
-
-Remark `a` and `b` are assumed to have the same type.
--/
-private def getDiseqFor? (a b : Expr) : GoalM (Option Expr) := do
-  /-
-  In Z3, we use the congruence table to find equalities more efficiently,
-  but this optimization would be more complicated here because equalities have
-  the type as an implicit argument, and `grind`s congruence table assumes it is
-  hash-consed and canonicalized. So, we use the "slower" approach of visiting
-  parents.
-  -/
-  let aRoot ← getRoot a
-  let bRoot ← getRoot b
-  let aParents ← getParents aRoot
-  let bParents ← getParents bRoot
-  if aParents.size ≤ bParents.size then
-    go aParents
-  else
-    go bParents
-where
-  go (parents : ParentSet) : GoalM (Option Expr) := do
-    for parent in parents do
-      let_expr Eq α c d := parent | continue
-      if (← isEqFalse parent) then
-        -- Remark: we expect `hasType` test to seldom fail, but it can happen because of
-        -- heterogeneous equalities
-        if (← isEqv a c <&&> isEqv b d <&&> hasType a α) then
-          return some parent
-        if (← isEqv a d <&&> isEqv b c <&&> hasType a α) then
-          return some parent
-    return none
-
-/--
-Returns `true` if `a` and `b` are known to be disequal.
-See `getDiseqFor?`
--/
-def isDiseq (a b : Expr) : GoalM Bool := do
-  return (← getDiseqFor? a b).isSome
-
-/--
-Returns a proof for `true` if `a` and `b` are known to be disequal.
-See `getDiseqFor?`
--/
-def mkDiseqProof? (a b : Expr) : GoalM (Option Expr) := do
-  let some eq ← getDiseqFor? a b | return none
-  let_expr f@Eq α c d := eq | unreachable!
-  let u := f.constLevels!
-  let h ← mkOfEqFalse (← mkEqFalseProof eq)
-  let (c, d, h) ← if (← isEqv a c <&&> isEqv b d) then
-    pure (c, d, h)
-  else
-    pure (d, c, mkApp4 (mkConst ``Ne.symm u) α c d h)
-  -- We have `a = c` and `b = d`
-  let h ← if isSameExpr a c then
-    pure h
-  else
-    pure <| mkApp6 (mkConst ``Grind.ne_of_ne_of_eq_left u) α a c d (← mkEqProof a c) h
-  -- `h : a ≠ d
-  if isSameExpr b d then
-    return h
-  else
-    return mkApp6 (mkConst ``Grind.ne_of_ne_of_eq_right u) α b a d (← mkEqProof b d) h
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Propagate.lean

@@ -146,7 +146,6 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
     pushEq a b <| mkOfEqTrueCore e (← mkEqTrueProof e)
   else if (← isEqFalse e) then
     let_expr Eq α lhs rhs := e | return ()
-    propagateCutsatDiseq lhs rhs
     let thms ← getExtTheorems α
     if !thms.isEmpty then
       /-

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Tactics
 import Init.Data.Queue
-import Std.Data.TreeSet
 import Lean.Util.ShareCommon
 import Lean.HeadIndex
 import Lean.Meta.Basic
@@ -397,7 +396,7 @@ instance : BEq (CongrKey enodes) where
 abbrev CongrTable (enodes : ENodeMap) := PHashSet (CongrKey enodes)
 
 -- Remark: we cannot use pointer addresses here because we have to traverse the tree.
-abbrev ParentSet := Std.TreeSet Expr Expr.quickComp
+abbrev ParentSet := RBTree Expr Expr.quickComp
 abbrev ParentMap := PHashMap ENodeKey ParentSet
 
 /--
@@ -866,16 +865,9 @@ opaque Arith.Cutsat.processNewEq (a b : Expr) : GoalM Unit
 Notifies the cutsat module that `a = k` where
 `a` is term that has been internalized by this module, and `k` is a numeral.
 -/
-@[extern "lean_process_cutsat_eq_lit"] -- forward definition
+@[extern "lean_process_new_cutsat_lit"] -- forward definition
 opaque Arith.Cutsat.processNewEqLit (a k : Expr) : GoalM Unit
 
-/--
-Notifies the cutsat module that `a ≠ b` where
-`a` and `b` are terms that have been internalized by this module.
--/
-@[extern "lean_process_cutsat_diseq"] -- forward definition
-opaque Arith.Cutsat.processNewDiseq (a b : Expr) : GoalM Unit
-
 /-- Returns `true` if `e` is a nonegative numeral and has type `Int`. -/
 def isNonnegIntNum (e : Expr) : Bool := Id.run do
   let_expr OfNat.ofNat _ _ inst := e | false
@@ -890,52 +882,6 @@ def isIntNum (e : Expr) : Bool :=
     isNonnegIntNum e
   | _ => isNonnegIntNum e
 
-/--
-Returns `true` if type of `t` is definitionally equal to `α`
--/
-def hasType (t α : Expr) : MetaM Bool :=
-  withDefault do isDefEq (← inferType t) α
-
-/--
-For each equality `b = c` in `parents`, executes `k b c` IF
-- `b = c` is equal to `False`, and
-- `a` is the equivalence class of `b` or `c`, and
-- type of `a` is definitionally equal to types of `b` and `c`.
--/
-@[inline] def forEachDiseqOfCore (a : Expr) (parents : ParentSet) (k : (lhs : Expr) → (rhs : Expr) → GoalM Unit) : GoalM Unit := do
-  for parent in parents do
-    let_expr Eq α b c := parent | continue
-    if (← isEqFalse parent) then
-    if (← isEqv a b <||> isEqv a c) then
-    if (← hasType a α) then
-      k b c
-
-/--
-For each equality `b = c` in `(← getParents a)`, executes `k b c` IF
-- `b = c` is equal to `False`, and
-- `a` is the equivalence class of `b` or `c`, and
-- type of `a` is definitionally equal to types of `b` and `c`.
--/
-@[inline] def forEachDiseqOf (a : Expr) (k : (lhs : Expr) → (rhs : Expr) → GoalM Unit) : GoalM Unit := do
-  forEachDiseqOfCore a (← getParents a) k
-
-/--
-Given `lhs` and `rhs` that are known to be disequal, checks whether
-`lhs` and `rhs` have cutsat terms `e₁` and `e₂` attached to them,
-and invokes process `Arith.Cutsat.processNewDiseq e₁ e₂`
--/
-def propagateCutsatDiseq (lhs rhs : Expr) : GoalM Unit := do
-  let { cutsat? := some e₁, .. } ← getRootENode lhs | return ()
-  let { cutsat? := some e₂, .. } ← getRootENode rhs | return ()
-  Arith.Cutsat.processNewDiseq e₁ e₂
-
-/--
-Traverses all known disequalities about `e`, and propagate the ones relevant to the
-cutsat module.
--/
-def propagateCutsatDiseqs (e : Expr) : GoalM Unit := do
-  forEachDiseqOf e propagateCutsatDiseq
-
 /--
 Marks `e` as a term of interest to the cutsat module.
 If the root of `e`s equivalence class has already a term of interest,
@@ -949,7 +895,6 @@ def markAsCutsatTerm (e : Expr) : GoalM Unit := do
     Arith.Cutsat.processNewEqLit e root.self
   else
     setENode root.self { root with cutsat? := some e }
-    propagateCutsatDiseqs root.self
 
 /-- Returns `true` is `e` is the root of its congruence class. -/
 def isCongrRoot (e : Expr) : GoalM Bool := do

src/Lean/Meta/Tactic/TryThis.lean

@@ -8,7 +8,6 @@ import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Lean.Data.Json.Elab
 import Lean.Data.Lsp.Utf16
-import Lean.Meta.Tactic.ExposeNames
 
 /-!
 # "Try this" support
@@ -427,27 +426,17 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
     (codeActionPrefix? : Option String := none) : MetaM Unit := do
   if suggestions.isEmpty then throwErrorAt ref "no suggestions available"
   let msgs := suggestions.map toMessageData
-  let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ .nest 2 m)
+  let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ m)
   logInfoAt ref m!"{header}{msgs}"
   addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
 
-/--
-Returns the syntax for an `exact` or `refine` (as indicated by `useRefine`) tactic corresponding to
-`e`. If `exposeNames` is `true`, prepends the tactic with `expose_names.`
--/
-def mkExactSuggestionSyntax (e : Expr) (useRefine : Bool) (exposeNames : Bool) : MetaM (TSyntax `tactic) :=
-  withOptions (pp.mvars.set · false) do
-  let exprStx ← (if exposeNames then withExposedNames else id) <| delabToRefinableSyntax e
-  let tac ← if useRefine then `(tactic| refine $exprStx) else `(tactic| exact $exprStx)
-  let tacSeq ← if exposeNames then `(tactic| (expose_names; $tac)) else pure tac
-  return tacSeq
-
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (exposeNames : Bool) (e : Expr) :
-    MetaM Suggestion :=
+private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion :=
   withOptions (pp.mvars.set · false) do
+  let stx ← delabToRefinableSyntax e
   let mvars ← getMVars e
-  let mut suggestion ← mkExactSuggestionSyntax e (useRefine := !mvars.isEmpty) exposeNames
-  let messageData? ← SuggestionText.prettyExtra suggestion
+  let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
+  let pp ← ppExpr e
+  let messageData? := if mvars.isEmpty then m!"exact {pp}" else m!"refine {pp}"
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in mvars do
@@ -468,12 +457,11 @@ The parameters are:
   `Remaining subgoals:`
 * `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
   suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
-* `exposeNames`: if true (default false), will insert `expose_names` prior to the generated tactic
 -/
 def addExactSuggestion (ref : Syntax) (e : Expr)
     (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none) (exposeNames := false) : MetaM Unit := do
-  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg exposeNames e)
+    (codeActionPrefix? : Option String := none): MetaM Unit := do
+  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e)
     (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add `exact e` or `refine e` suggestions.
@@ -491,8 +479,8 @@ The parameters are:
 -/
 def addExactSuggestions (ref : Syntax) (es : Array Expr)
     (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none) (exposeNames := false) : MetaM Unit := do
-  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg exposeNames
+    (codeActionPrefix? : Option String := none) : MetaM Unit := do
+  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg
   addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add a term suggestion.

src/Lean/Util/Trace.lean

@@ -380,9 +380,7 @@ def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Un
     pos2traces := pos2traces.insert (pos, endPos) <| pos2traces.getD (pos, endPos) #[] |>.push traceElem.msg
   let traces' := pos2traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    -- cmdline and info view differ in how they insert newlines in between trace nodes so we just
-    -- put them in a synthetic root node for now and let the rendering functions handle this case
-    let data := .tagged `trace <| .trace { cls := .anonymous } .nil traceMsg
+    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
     logMessage <| Elab.mkMessageCore (← getFileName) (← getFileMap) data .information pos endPos
 
 end Lean

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -149,12 +149,6 @@ where
   | ctx,      compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
   | ctx,      group d                  => Format.group <$> go nCtx ctx d
   | ctx,      .trace data header children => do
-    if data.cls.isAnonymous then
-      -- Sequence of top-level traces collected by `addTraceAsMessages`, do not indent.
-      -- As with nested sibling nodes, we do not separate them with newlines but rely on the client
-      -- to never put trace nodes on the same line.
-      return .join (← children.mapM (go nCtx ctx)).toList
-
     let mut header := (← go nCtx ctx header).nest 4
     if data.startTime != 0 then
       header := f!"[{data.stopTime - data.startTime}] {header}"

src/Std/Classes/Ord.lean

@@ -28,14 +28,12 @@ class ReflCmp {α : Type u} (cmp : α → α → Ordering) : Prop where
   /-- Comparison is reflexive. -/
   compare_self {a : α} : cmp a a = .eq
 
+export ReflCmp (compare_self)
+
 /-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
 abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering)
 
-@[simp]
-theorem ReflOrd.compare_self {α : Type u} [Ord α] [ReflOrd α] {a : α} : compare a a = .eq :=
-    ReflCmp.compare_self
-
-export ReflOrd (compare_self)
+attribute [simp] compare_self
 
 end Refl
 
@@ -268,7 +266,7 @@ variable {α : Type u} {cmp : α → α → Ordering} [LawfulEqCmp cmp]
 
 @[simp]
 theorem compare_eq_iff_eq {a b : α} : cmp a b = .eq ↔ a = b :=
-  ⟨LawfulEqCmp.eq_of_compare, by rintro rfl; exact ReflCmp.compare_self⟩
+  ⟨LawfulEqCmp.eq_of_compare, by rintro rfl; simp⟩
 
 @[simp]
 theorem compare_beq_iff_eq {a b : α} : cmp a b == .eq ↔ a = b :=
@@ -295,7 +293,7 @@ theorem beq_eq [Ord α] {a b : α} : (a == b) = (compare a b == .eq) :=
 theorem equivBEq_of_transOrd [Ord α] [TransOrd α] : EquivBEq α where
   symm {a b} h := by simp_all [OrientedCmp.eq_comm]
   trans h₁ h₂ := by simp_all only [beq_eq, beq_iff_eq]; exact TransCmp.eq_trans h₁ h₂
-  refl := by simp only [beq_eq, beq_iff_eq]; exact compare_self
+  refl := by simp
 
 theorem lawfulBEq_of_lawfulEqOrd [Ord α] [LawfulEqOrd α] : LawfulBEq α where
   eq_of_beq hbeq := by simp_all

src/Std/Data/DTreeMap/Basic.lean

@@ -634,7 +634,7 @@ def getThenInsertIfNew? (t : DTreeMap α β cmp) (a : α) (b : β) :
 
 @[inline, inherit_doc DTreeMap.get?]
 def get? (t : DTreeMap α β cmp) (a : α) : Option β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.get? t.inner a
+  letI : Ord α := ⟨cmp⟩; Impl.Const.get? a t.inner
 
 @[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
 def find? (t : DTreeMap α β cmp) (a : α) : Option β :=
@@ -642,11 +642,11 @@ def find? (t : DTreeMap α β cmp) (a : α) : Option β :=
 
 @[inline, inherit_doc DTreeMap.get]
 def get (t : DTreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.get t.inner a h
+  letI : Ord α := ⟨cmp⟩; Impl.Const.get a t.inner h
 
 @[inline, inherit_doc DTreeMap.get!]
 def get! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.get! t.inner a
+  letI : Ord α := ⟨cmp⟩; Impl.Const.get! a t.inner
 
 @[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
 def find! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
@@ -654,7 +654,7 @@ def find! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
 
 @[inline, inherit_doc DTreeMap.getD]
 def getD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.getD t.inner a fallback
+  letI : Ord α := ⟨cmp⟩; Impl.Const.getD a t.inner fallback
 
 @[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
 def findD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=

src/Std/Data/DTreeMap/Internal/Balancing.lean

@@ -763,13 +763,13 @@ theorem balance_eq_inner [Ord α] {sz k v} {l r : Impl α β}
     balance k v l r hl.left hl.right h = inner sz k v l r := by
   rw [balance_eq_balance!, balance!_eq_balanceₘ hl.left hl.right h, balanceₘ]
   have hl' := balanced_inner_iff.mp hl
-  fun_cases balanceₘ k v l r <;> tree_tac
+  cases k, v, l, r, hl.left, hl.right, h using balanceₘ.fun_cases <;> tree_tac
 
 theorem balance!_desc {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced)
     (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :
     (balance! k v l r).size = l.size + 1 + r.size ∧ (balance! k v l r).Balanced := by
   rw [balance!_eq_balanceₘ hlb hrb hlr, balanceₘ]
-  fun_cases balanceₘ k v l r
+  cases k, v, l, r, hlb, hrb, hlr using balanceₘ.fun_cases
   · rw [if_pos ‹_›, bin, balanced_inner_iff]
     exact ⟨rfl, hlb, hrb, Or.inl ‹_›, rfl⟩
   · rw [if_neg ‹_›, dif_pos ‹_›]

src/Std/Data/DTreeMap/Internal/Cell.lean

@@ -43,7 +43,7 @@ def ofEq [Ord α] {k : α → Ordering} (k' : α) (v' : β k') (hcmp : ∀ [Orie
 
 /-- Create a cell with a matching key. Internal implementation detail of the tree map -/
 def of [Ord α] (k : α) (v : β k) : Cell α β (compare k) :=
-  .ofEq k v compare_self
+  .ofEq k v (by intro; simp)
 
 @[simp]
 theorem ofEq_inner [Ord α] {k : α → Ordering} {k' : α} {v' : β k'} {h} :

src/Std/Data/DTreeMap/Internal/Lemmas.lean

@@ -61,10 +61,7 @@ private def helperLemmaNames : Array Name :=
 
 private def queryNames : Array Name :=
   #[``isEmpty_eq_isEmpty, ``contains_eq_containsKey, ``size_eq_length,
-    ``get?_eq_getValueCast?, ``Const.get?_eq_getValue?,
-    ``get_eq_getValueCast, ``Const.get_eq_getValue,
-    ``get!_eq_getValueCast!, ``Const.get!_eq_getValue!,
-    ``getD_eq_getValueCastD, ``Const.getD_eq_getValueD]
+    ``get?_eq_getValueCast?, ``Const.get?_eq_getValue?]
 
 private def modifyMap : Std.HashMap Name Name :=
   .ofList
@@ -490,461 +487,71 @@ namespace Const
 
 variable {β : Type v} {t : Impl α β}
 
-theorem get?_empty [TransOrd α] {a : α} : get? (empty : Impl α β) a = none := by
+theorem get?_empty [TransOrd α] {a : α} : get? a (empty : Impl α β) = none := by
   simp_to_model using List.getValue?_nil
 
 theorem get?_of_isEmpty [TransOrd α] (h : t.WF) {a : α} :
-    t.isEmpty = true → get? t a = none := by
+    t.isEmpty = true → get? a t = none := by
   simp_to_model; empty
 
 theorem get?_insert [TransOrd α] (h : t.WF) {a k : α} {v : β} :
-    get? (t.insert k v h.balanced).impl a =
-      if compare k a = .eq then some v else get? t a := by
+    get? a (t.insert k v h.balanced).impl =
+      if compare k a = .eq then some v else get? a t := by
   simp_to_model [insert] using List.getValue?_insertEntry
 
 theorem get?_insert! [TransOrd α] (h : t.WF) {a k : α} {v : β} :
-    get? (t.insert! k v) a =
-      if compare k a = .eq then some v else get? t a := by
+    get? a (t.insert! k v) =
+      if compare k a = .eq then some v else get? a t := by
   simp_to_model [insert!] using List.getValue?_insertEntry
 
 theorem get?_insert_self [TransOrd α] (h : t.WF) {k : α} {v : β} :
-    get? (t.insert k v h.balanced).impl k = some v := by
+    get? k (t.insert k v h.balanced).impl = some v := by
   simp_to_model [insert] using List.getValue?_insertEntry_self
 
 theorem get?_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β} :
-    get? (t.insert! k v) k = some v := by
+    get? k (t.insert! k v) = some v := by
   simp_to_model [insert!] using List.getValue?_insertEntry_self
 
 theorem contains_eq_isSome_get? [TransOrd α] (h : t.WF) {a : α} :
-    t.contains a = (get? t a).isSome := by
+    t.contains a = (get? a t).isSome := by
   simp_to_model using List.containsKey_eq_isSome_getValue?
 
 theorem mem_iff_isSome_get? [TransOrd α] (h : t.WF) {a : α} :
-    a ∈ t ↔ (get? t a).isSome := by
+    a ∈ t ↔ (get? a t).isSome := by
   simpa [mem_iff_contains] using contains_eq_isSome_get? h
 
 theorem get?_eq_none_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} :
-    t.contains a = false → get? t a = none := by
+    t.contains a = false → get? a t = none := by
   simp_to_model using List.getValue?_eq_none.mpr
 
 theorem get?_eq_none [TransOrd α] (h : t.WF) {a : α} :
-    ¬ a ∈ t → get? t a = none := by
+    ¬ a ∈ t → get? a t = none := by
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
 
 theorem get?_erase [TransOrd α] (h : t.WF) {k a : α} :
-    get? (t.erase k h.balanced).impl a = if compare k a = .eq then none else get? t a := by
+    get? a (t.erase k h.balanced).impl = if compare k a = .eq then none else get? a t := by
   simp_to_model [erase] using List.getValue?_eraseKey
 
 theorem get?_erase! [TransOrd α] (h : t.WF) {k a : α} :
-    get? (t.erase! k) a = if compare k a = .eq then none else get? t a := by
+    get? a (t.erase! k) = if compare k a = .eq then none else get? a t := by
   simp_to_model [erase!] using List.getValue?_eraseKey
 
 theorem get?_erase_self [TransOrd α] (h : t.WF) {k : α} :
-    get? (t.erase k h.balanced).impl k = none := by
+    get? k (t.erase k h.balanced).impl = none := by
   simp_to_model [erase] using List.getValue?_eraseKey_self
 
 theorem get?_erase!_self [TransOrd α] (h : t.WF) {k : α} :
-    get? (t.erase! k) k = none := by
+    get? k (t.erase! k) = none := by
   simp_to_model [erase!] using List.getValue?_eraseKey_self
 
-theorem get?_eq_get? [LawfulEqOrd α] [TransOrd α] (h : t.WF) {a : α} : get? t a = t.get? a := by
+theorem get?_eq_get? [LawfulEqOrd α] [TransOrd α] (h : t.WF) {a : α} : get? a t = t.get? a := by
   simp_to_model using List.getValue?_eq_getValueCast?
 
 theorem get?_congr [TransOrd α] (h : t.WF) {a b : α} (hab : compare a b = .eq) :
-    get? t a = get? t b := by
+    get? a t = get? b t := by
   revert hab
   simp_to_model using List.getValue?_congr
 
 end Const
 
-theorem get_insert [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
-    (t.insert k v h.balanced).impl.get a h₁ =
-      if h₂ : compare k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂)) v
-      else
-        t.get a (contains_of_contains_insert h h₁ h₂) := by
-  simp_to_model [insert] using List.getValueCast_insertEntry
-
-theorem get_insert! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
-    (t.insert! k v).get a h₁ =
-      if h₂ : compare k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂)) v
-      else
-        t.get a (contains_of_contains_insert! h h₁ h₂) := by
-  simp_to_model [insert!] using List.getValueCast_insertEntry
-
-theorem get_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
-    (t.insert k v h.balanced).impl.get k (contains_insert_self h) = v := by
-  simp_to_model [insert] using List.getValueCast_insertEntry_self
-
-theorem get_insert!_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
-    (t.insert! k v).get k (contains_insert!_self h) = v := by
-  simp_to_model [insert!] using List.getValueCast_insertEntry_self
-
-@[simp]
-theorem get_erase [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {h'} :
-    (t.erase k h.balanced).impl.get a h' = t.get a (contains_of_contains_erase h h') := by
-  simp_to_model [erase] using List.getValueCast_eraseKey
-
-theorem get_erase! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {h'} :
-    (t.erase! k).get a h' = t.get a (contains_of_contains_erase! h h') := by
-  simp_to_model [erase!] using List.getValueCast_eraseKey
-
-theorem get?_eq_some_get [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {h'} : t.get? a = some (t.get a h') := by
-  simp_to_model using List.getValueCast?_eq_some_getValueCast
-
-namespace Const
-
-variable {β : Type v} {t : Impl α β} (h : t.WF)
-
-theorem get_insert [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} :
-    get (t.insert k v h.balanced).impl a h₁ =
-      if h₂ : compare k a = .eq then v
-      else get t a (contains_of_contains_insert h h₁ h₂) := by
-  simp_to_model [insert] using List.getValue_insertEntry
-
-theorem get_insert! [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} :
-    get (t.insert! k v) a h₁ =
-      if h₂ : compare k a = .eq then v
-      else get t a (contains_of_contains_insert! h h₁ h₂) := by
-  simp_to_model [insert!] using List.getValue_insertEntry
-
-theorem get_insert_self [TransOrd α] (h : t.WF) {k : α} {v : β} :
-    get (t.insert k v h.balanced).impl k (contains_insert_self h) = v := by
-  simp_to_model [insert] using List.getValue_insertEntry_self
-
-theorem get_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β} :
-    get (t.insert! k v) k (contains_insert!_self h) = v := by
-  simp_to_model [insert!] using List.getValue_insertEntry_self
-
-@[simp]
-theorem get_erase [TransOrd α] (h : t.WF) {k a : α} {h'} :
-    get (t.erase k h.balanced).impl a h' = get t a (contains_of_contains_erase h h') := by
-  simp_to_model [erase] using List.getValue_eraseKey
-
-theorem get_erase! [TransOrd α] (h : t.WF) {k a : α} {h'} :
-    get (t.erase! k) a h' = get t a (contains_of_contains_erase! h h') := by
-  simp_to_model [erase!] using List.getValue_eraseKey
-
-theorem get?_eq_some_get [TransOrd α] (h : t.WF) {a : α} {h} :
-    get? t a = some (get t a h) := by
-  simp_to_model using List.getValue?_eq_some_getValue
-
-theorem get_eq_get [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {h} : get t a h = t.get a h := by
-  simp_to_model using List.getValue_eq_getValueCast
-
-theorem get_congr [TransOrd α] (h : t.WF) {a b : α} (hab : compare a b = .eq) {h'} :
-    get t a h' = get t b ((contains_congr h hab).symm.trans h') := by
-  revert hab h'
-  simp_to_model using List.getValue_congr
-
-end Const
-
-theorem get!_empty [TransOrd α] [LawfulEqOrd α] {a : α} [Inhabited (β a)] :
-    get! (empty : Impl α β) a = default := by
-  simp_to_model using List.getValueCast!_nil
-
-theorem get!_of_isEmpty [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] :
-    t.isEmpty = true → t.get! a = default := by
-  simp_to_model; empty
-
-theorem get!_insert [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} :
-    (t.insert k v h.balanced).impl.get! a =
-      if h : compare k a = .eq then cast (congrArg β (compare_eq_iff_eq.mp h)) v else t.get! a := by
-  simp_to_model [insert] using List.getValueCast!_insertEntry
-
-theorem get!_insert! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} :
-    (t.insert! k v).get! a =
-      if h : compare k a = .eq then cast (congrArg β (compare_eq_iff_eq.mp h)) v else t.get! a := by
-  simp_to_model [insert!] using List.getValueCast!_insertEntry
-
-theorem get!_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] {b : β a} :
-    (t.insert a b h.balanced).impl.get! a = b := by
-  simp_to_model [insert] using List.getValueCast!_insertEntry_self
-
-theorem get!_insert!_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] {b : β a} :
-    (t.insert! a b).get! a = b := by
-  simp_to_model [insert!] using List.getValueCast!_insertEntry_self
-
-theorem get!_eq_default_of_contains_eq_false [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α}
-    [Inhabited (β a)] : t.contains a = false → t.get! a = default := by
-  simp_to_model using List.getValueCast!_eq_default
-
-theorem get!_eq_default [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] :
-    ¬ a ∈ t → t.get! a = default := by
-  simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
-
-theorem get!_erase [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] :
-    (t.erase k h.balanced).impl.get! a = if compare k a = .eq then default else t.get! a := by
-  simp_to_model [erase] using List.getValueCast!_eraseKey
-
-theorem get!_erase! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] :
-    (t.erase! k).get! a = if compare k a = .eq then default else t.get! a := by
-  simp_to_model [erase!] using List.getValueCast!_eraseKey
-
-theorem get!_erase_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} [Inhabited (β k)] :
-    (t.erase k h.balanced).impl.get! k = default := by
-  simp_to_model [erase] using List.getValueCast!_eraseKey_self
-
-theorem get!_erase!_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} [Inhabited (β k)] :
-    (t.erase! k).get! k = default := by
-  simp_to_model [erase!] using List.getValueCast!_eraseKey_self
-
-theorem get?_eq_some_get!_of_contains [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] :
-    t.contains a = true → t.get? a = some (t.get! a) := by
-  simp_to_model using List.getValueCast?_eq_some_getValueCast!
-
-theorem get?_eq_some_get! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] :
-    a ∈ t → t.get? a = some (t.get! a) := by
-  simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
-
-theorem get!_eq_get!_get? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] :
-    t.get! a = (t.get? a).get! := by
-  simp_to_model using List.getValueCast!_eq_getValueCast?
-
-theorem get_eq_get! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] {h} :
-    t.get a h = t.get! a := by
-  simp_to_model using List.getValueCast_eq_getValueCast!
-
-namespace Const
-
-variable {β : Type v} {t : Impl α β} (h : t.WF)
-
-theorem get!_empty [TransOrd α] [Inhabited β] {a : α} :
-    get! (empty : Impl α β) a = default := by
-  simp_to_model using List.getValue!_nil
-
-theorem get!_of_isEmpty [TransOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    t.isEmpty = true → get! t a = default := by
-  simp_to_model; empty
-
-theorem get!_insert [TransOrd α] [Inhabited β] (h : t.WF) {k a : α} {v : β} :
-    get! (t.insert k v h.balanced).impl a = if compare k a = .eq then v else get! t a := by
-  simp_to_model [insert] using List.getValue!_insertEntry
-
-theorem get!_insert! [TransOrd α] [Inhabited β] (h : t.WF) {k a : α} {v : β} :
-    get! (t.insert! k v) a = if compare k a = .eq then v else get! t a := by
-  simp_to_model [insert!] using List.getValue!_insertEntry
-
-theorem get!_insert_self [TransOrd α] [Inhabited β] (h : t.WF) {k : α}
-    {v : β} : get! (t.insert k v h.balanced).impl k = v := by
-  simp_to_model [insert] using List.getValue!_insertEntry_self
-
-theorem get!_insert!_self [TransOrd α] [Inhabited β] (h : t.WF) {k : α}
-    {v : β} : get! (t.insert! k v) k = v := by
-  simp_to_model [insert!] using List.getValue!_insertEntry_self
-
-theorem get!_eq_default_of_contains_eq_false [TransOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    t.contains a = false → get! t a = default := by
-  simp_to_model using List.getValue!_eq_default
-
-theorem get!_eq_default [TransOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    ¬ a ∈ t → get! t a = default := by
-  simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
-
-theorem get!_erase [TransOrd α] [Inhabited β] (h : t.WF) {k a : α} :
-    get! (t.erase k h.balanced).impl a = if compare k a = .eq then default else get! t a := by
-  simp_to_model [erase] using List.getValue!_eraseKey
-
-theorem get!_erase! [TransOrd α] [Inhabited β] (h : t.WF) {k a : α} :
-    get! (t.erase! k) a = if compare k a = .eq then default else get! t a := by
-  simp_to_model [erase!] using List.getValue!_eraseKey
-
-theorem get!_erase_self [TransOrd α] [Inhabited β] (h : t.WF) {k : α} :
-    get! (t.erase k h.balanced).impl k = default := by
-  simp_to_model [erase] using List.getValue!_eraseKey_self
-
-theorem get!_erase!_self [TransOrd α] [Inhabited β] (h : t.WF) {k : α} :
-    get! (t.erase! k) k = default := by
-  simp_to_model [erase!] using List.getValue!_eraseKey_self
-
-theorem get?_eq_some_get!_of_contains [TransOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    t.contains a = true → get? t a = some (get! t a) := by
-  simp_to_model using List.getValue?_eq_some_getValue!
-
-theorem get?_eq_some_get! [TransOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    a ∈ t → get? t a = some (get! t a) := by
-  simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
-
-theorem get!_eq_get!_get? [TransOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    get! t a = (get? t a).get! := by
-  simp_to_model using List.getValue!_eq_getValue?
-
-theorem get_eq_get! [TransOrd α] [Inhabited β] (h : t.WF) {a : α} {h} :
-    get t a h = get! t a := by
-  simp_to_model using List.getValue_eq_getValue!
-
-theorem get!_eq_get! [TransOrd α] [LawfulEqOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    get! t a = t.get! a := by
-  simp_to_model using List.getValue!_eq_getValueCast!
-
-theorem get!_congr [TransOrd α] [Inhabited β] (h : t.WF) {a b : α}
-    (hab : compare a b = .eq) : get! t a = get! t b := by
-  revert hab
-  simp_to_model using List.getValue!_congr
-
-end Const
-
-theorem getD_empty [TransOrd α] [LawfulEqOrd α] {a : α} {fallback : β a} :
-    (empty : Impl α β).getD a fallback = fallback := by
-  simp [getD, empty]
-
-theorem getD_of_isEmpty [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} : t.isEmpty = true → t.getD a fallback = fallback := by
-  simp_to_model; empty
-
-theorem getD_insert [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
-    (t.insert k v h.balanced).impl.getD a fallback =
-      if h : compare k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h)) v
-      else t.getD a fallback := by
-  simp_to_model [insert] using List.getValueCastD_insertEntry
-
-theorem getD_insert! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
-    (t.insert! k v).getD a fallback =
-      if h : compare k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h)) v
-      else t.getD a fallback := by
-  simp_to_model [insert!] using List.getValueCastD_insertEntry
-
-theorem getD_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback b : β a} :
-    (t.insert a b h.balanced).impl.getD a fallback = b := by
-  simp_to_model [insert] using List.getValueCastD_insertEntry_self
-
-theorem getD_insert!_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback b : β a} :
-    (t.insert! a b).getD a fallback = b := by
-  simp_to_model [insert!] using List.getValueCastD_insertEntry_self
-
-theorem getD_eq_fallback_of_contains_eq_false [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} :
-    t.contains a = false → t.getD a fallback = fallback := by
-  simp_to_model using List.getValueCastD_eq_fallback
-
-theorem getD_eq_fallback [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} :
-    ¬ a ∈ t → t.getD a fallback = fallback := by
-  simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
-
-theorem getD_erase [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} :
-    (t.erase k h.balanced).impl.getD a fallback = if compare k a = .eq then fallback else t.getD a fallback := by
-  simp_to_model [erase] using List.getValueCastD_eraseKey
-
-theorem getD_erase! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} :
-    (t.erase! k).getD a fallback = if compare k a = .eq then fallback else t.getD a fallback := by
-  simp_to_model [erase!] using List.getValueCastD_eraseKey
-
-theorem getD_erase_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k} :
-    (t.erase k h.balanced).impl.getD k fallback = fallback := by
-  simp_to_model [erase] using List.getValueCastD_eraseKey_self
-
-theorem getD_erase!_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k} :
-    (t.erase! k).getD k fallback = fallback := by
-  simp_to_model [erase!] using List.getValueCastD_eraseKey_self
-
-theorem get?_eq_some_getD_of_contains [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} :
-    t.contains a = true → t.get? a = some (t.getD a fallback) := by
-  simp_to_model using List.getValueCast?_eq_some_getValueCastD
-
-theorem get?_eq_some_getD [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} :
-    a ∈ t → t.get? a = some (t.getD a fallback) := by
-  simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
-
-theorem getD_eq_getD_get? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} :
-    t.getD a fallback = (t.get? a).getD fallback := by
-  simp_to_model using List.getValueCastD_eq_getValueCast?
-
-theorem get_eq_getD [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} {h} :
-    t.get a h = t.getD a fallback := by
-  simp_to_model using List.getValueCast_eq_getValueCastD
-
-theorem get!_eq_getD_default [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] :
-    t.get! a = t.getD a default := by
-  simp_to_model using List.getValueCast!_eq_getValueCastD_default
-
-namespace Const
-
-variable {β : Type v} {t : Impl α β} (h : t.WF)
-
-theorem getD_empty [TransOrd α] {a : α} {fallback : β} :
-    getD (empty : Impl α β) a fallback = fallback := by
-  simp_to_model using List.getValueD_nil
-
-theorem getD_of_isEmpty [TransOrd α] (h : t.WF) {a : α} {fallback : β} :
-    t.isEmpty = true → getD t a fallback = fallback := by
-  simp_to_model; empty
-
-theorem getD_insert [TransOrd α] (h : t.WF) {k a : α} {fallback v : β} :
-    getD (t.insert k v h.balanced).impl a fallback = if compare k a = .eq then v else getD t a fallback := by
-  simp_to_model [insert] using List.getValueD_insertEntry
-
-theorem getD_insert! [TransOrd α] (h : t.WF) {k a : α} {fallback v : β} :
-    getD (t.insert! k v) a fallback = if compare k a = .eq then v else getD t a fallback := by
-  simp_to_model [insert!] using List.getValueD_insertEntry
-
-theorem getD_insert_self [TransOrd α] (h : t.WF) {k : α} {fallback v : β} :
-    getD (t.insert k v h.balanced).impl k fallback = v := by
-  simp_to_model [insert] using List.getValueD_insertEntry_self
-
-theorem getD_insert!_self [TransOrd α] (h : t.WF) {k : α} {fallback v : β} :
-    getD (t.insert! k v) k fallback = v := by
-  simp_to_model [insert!] using List.getValueD_insertEntry_self
-
-theorem getD_eq_fallback_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} {fallback : β} :
-    t.contains a = false → getD t a fallback = fallback := by
-  simp_to_model using List.getValueD_eq_fallback
-
-theorem getD_eq_fallback [TransOrd α] (h : t.WF) {a : α} {fallback : β} :
-    ¬ a ∈ t → getD t a fallback = fallback := by
-  simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
-
-theorem getD_erase [TransOrd α] (h : t.WF) {k a : α} {fallback : β} :
-    getD (t.erase k h.balanced).impl a fallback = if compare k a = .eq then
-      fallback
-    else
-      getD t a fallback := by
-  simp_to_model [erase] using List.getValueD_eraseKey
-
-theorem getD_erase! [TransOrd α] (h : t.WF) {k a : α} {fallback : β} :
-    getD (t.erase! k) a fallback = if compare k a = .eq then
-      fallback
-    else
-      getD t a fallback := by
-  simp_to_model [erase!] using List.getValueD_eraseKey
-
-theorem getD_erase_self [TransOrd α] (h : t.WF) {k : α} {fallback : β} :
-    getD (t.erase k h.balanced).impl k fallback = fallback := by
-  simp_to_model [erase] using List.getValueD_eraseKey_self
-
-theorem getD_erase!_self [TransOrd α] (h : t.WF) {k : α} {fallback : β} :
-    getD (t.erase! k) k fallback = fallback := by
-  simp_to_model [erase!] using List.getValueD_eraseKey_self
-
-theorem get?_eq_some_getD_of_contains [TransOrd α] (h : t.WF) {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) := by
-  simp_to_model using List.getValue?_eq_some_getValueD
-
-theorem get?_eq_some_getD [TransOrd α] (h : t.WF) {a : α} {fallback : β} :
-    a ∈ t → get? t a = some (getD t a fallback) := by
-  simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
-
-theorem getD_eq_getD_get? [TransOrd α] (h : t.WF) {a : α} {fallback : β} :
-    getD t a fallback = (get? t a).getD fallback := by
-  simp_to_model using List.getValueD_eq_getValue?
-
-theorem get_eq_getD [TransOrd α] (h : t.WF) {a : α} {fallback : β} {h} :
-    get t a h = getD t a fallback := by
-  simp_to_model using List.getValue_eq_getValueD
-
-theorem get!_eq_getD_default [TransOrd α] [Inhabited β] (h : t.WF) {a : α} :
-    get! t a = getD t a default := by
-  simp_to_model using List.getValue!_eq_getValueD_default
-
-theorem getD_eq_getD [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β} :
-    getD t a fallback = t.getD a fallback := by
-  simp_to_model using List.getValueD_eq_getValueCastD
-
-theorem getD_congr [TransOrd α] (h : t.WF) {a b : α} {fallback : β}
-    (hab : compare a b = .eq) : getD t a fallback = getD t b fallback := by
-  revert hab
-  simp_to_model using List.getValueD_congr
-
-end Const
-
 end Std.DTreeMap.Internal.Impl

src/Std/Data/DTreeMap/Internal/Model.lean

@@ -202,38 +202,16 @@ def updateCell [Ord α] (k : α) (f : Cell α β (compare k) → Cell α β (com
 Model implementation of the `contains` function.
 Internal implementation detail of the tree map
 -/
-def containsₘ [Ord α] (l : Impl α β) (k : α) : Bool :=
+def containsₘ [Ord α] (k : α) (l : Impl α β) : Bool :=
   applyCell k l fun c _ => c.contains
 
 /--
 Model implementation of the `get?` function.
 Internal implementation detail of the tree map
 -/
-def get?ₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) : Option (β k) :=
+def get?ₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) : Option (β k) :=
   applyCell k l fun c _ => c.get?
 
-/--
-Model implementation of the `get` function.
-Internal implementation detail of the tree map
--/
-def getₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) (h : (get?ₘ l k).isSome) :
-    β k :=
-  get?ₘ l k |>.get h
-
-/--
-Model implementation of the `get!` function.
-Internal implementation detail of the tree map
--/
-def get!ₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) [Inhabited (β k)] : β k :=
-  get?ₘ l k |>.get!
-
-/--
-Model implementation of the `getD` function.
-Internal implementation detail of the tree map
--/
-def getDₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) (fallback : β k) : β k :=
-  get?ₘ l k |>.getD fallback
-
 /--
 Model implementation of the `insert` function.
 Internal implementation detail of the tree map
@@ -273,31 +251,9 @@ variable {β : Type v}
 Model implementation of the `get?` function.
 Internal implementation detail of the tree map
 -/
-def get?ₘ [Ord α] (l : Impl α (fun _ => β)) (k : α) : Option β :=
+def get?ₘ [Ord α] (k : α) (l : Impl α (fun _ => β)) : Option β :=
   applyCell k l fun c _ => Cell.Const.get? c
 
-/--
-Model implementation of the `get` function.
-Internal implementation detail of the tree map
--/
-def getₘ [Ord α] (l : Impl α (fun _ => β)) (k : α) (h : (get?ₘ l k).isSome) :
-    β :=
-  get?ₘ l k |>.get h
-
-/--
-Model implementation of the `get!` function.
-Internal implementation detail of the tree map
--/
-def get!ₘ [Ord α] (l : Impl α (fun _ => β)) (k : α) [Inhabited β] : β :=
-  get?ₘ l k |>.get!
-
-/--
-Model implementation of the `getD` function.
-Internal implementation detail of the tree map
--/
-def getDₘ [Ord α] (l : Impl α (fun _ => β)) (k : α) (fallback : β) : β :=
-  get?ₘ l k |>.getD fallback
-
 /--
 Model implementation of the `alter` function.
 Internal implementation detail of the tree map
@@ -345,36 +301,6 @@ theorem get?_eq_get?ₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l :
     all_goals simp_all [Cell.get?, Cell.ofEq]
   · simp [get?, applyCell]
 
-theorem get_eq_get? [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) {h} :
-    l.get k h = l.get? k := by
-  induction l
-  · simp only [applyCell, get, get?]
-    split <;> rename_i ihl ihr hcmp <;> simp_all
-  · contradiction
-
-theorem get_eq_getₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) {h} (h') :
-    l.get k h = l.getₘ k h' := by
-  apply Option.some.inj
-  simp [get_eq_get?, get?_eq_get?ₘ, getₘ]
-
-theorem get!_eq_get!ₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) [Inhabited (β k)] (l : Impl α β) :
-    l.get! k = l.get!ₘ k := by
-  simp only [get!ₘ, get?ₘ]
-  induction l
-  · simp only [applyCell, get!]
-    split <;> rename_i hcmp₁ <;> split <;> rename_i hcmp₂ <;> try (simp [hcmp₁] at hcmp₂; done)
-    all_goals simp_all [Cell.get?, Cell.ofEq]
-  · simp only [get!, applyCell, Cell.get?_empty, Option.get!_none]; rfl
-
-theorem getD_eq_getDₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β)
-    (fallback : β k) : l.getD k fallback = l.getDₘ k fallback := by
-  simp only [getDₘ, get?ₘ]
-  induction l
-  · simp only [applyCell, getD]
-    split <;> rename_i hcmp₁ <;> split <;> rename_i hcmp₂ <;> try (simp [hcmp₁] at hcmp₂; done)
-    all_goals simp_all [Cell.get?, Cell.ofEq]
-  · simp only [getD, applyCell, Cell.get?_empty, Option.getD_none]
-
 theorem balanceL_eq_balance {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceL k v l r hlb hrb hlr = balance k v l r hlb hrb (Or.inl hlr.erase) := by
   rw [balanceL_eq_balanceLErase, balanceLErase_eq_balanceL!,
@@ -543,7 +469,7 @@ namespace Const
 variable {β : Type v}
 
 theorem get?_eq_get?ₘ [Ord α] (k : α) (l : Impl α (fun _ => β)) :
-    Const.get? l k = Const.get?ₘ l k := by
+    Const.get? k l = Const.get?ₘ k l := by
   simp only [Const.get?ₘ]
   induction l
   · simp only [applyCell, Const.get?]
@@ -551,36 +477,6 @@ theorem get?_eq_get?ₘ [Ord α] (k : α) (l : Impl α (fun _ => β)) :
     all_goals simp_all [Cell.Const.get?, Cell.ofEq]
   · simp [Const.get?, applyCell]
 
-theorem get_eq_get? [Ord α] (k : α) (l : Impl α (fun _ => β)) {h} :
-    get l k h = get? l k := by
-  induction l
-  · simp only [applyCell, get, get?]
-    split <;> rename_i ihl ihr hcmp <;> simp_all
-  · contradiction
-
-theorem get_eq_getₘ [Ord α] (k : α) (l : Impl α (fun _ => β)) {h} (h') :
-    get l k h = getₘ l k h' := by
-  apply Option.some.inj
-  simp [get_eq_get?, get?_eq_get?ₘ, getₘ]
-
-theorem get!_eq_get!ₘ [Ord α] (k : α) [Inhabited β] (l : Impl α (fun _ => β)) :
-    get! l k = get!ₘ l k := by
-  simp only [get!ₘ, get?ₘ]
-  induction l
-  · simp only [applyCell, get!]
-    split <;> rename_i hcmp₁ <;> split <;> rename_i hcmp₂ <;> try (simp [hcmp₁] at hcmp₂; done)
-    all_goals simp_all [Cell.Const.get?, Cell.ofEq]
-  · simp only [get!, applyCell, Option.get!_none]; rfl
-
-theorem getD_eq_getDₘ [Ord α] (k : α) (l : Impl α (fun _ => β))
-    (fallback : β) : getD l k fallback = getDₘ l k fallback := by
-  simp only [getDₘ, get?ₘ]
-  induction l
-  · simp only [applyCell, getD]
-    split <;> rename_i hcmp₁ <;> split <;> rename_i hcmp₂ <;> try (simp [hcmp₁] at hcmp₂; done)
-    all_goals simp_all [Cell.Const.get?, Cell.ofEq]
-  · simp only [getD, applyCell, Cell.Const.get?_empty, Option.getD_none]
-
 end Const
 
 end Impl

src/Std/Data/DTreeMap/Internal/Operations.lean

@@ -606,7 +606,7 @@ variable {β : Type v}
 @[inline]
 def getThenInsertIfNew? [Ord α] (k : α) (v : β) (t : Impl α (fun _ => β))
     (ht : t.Balanced) : Option β × Impl α (fun _ => β) :=
-  match get? t k with
+  match get? k t with
   | none => (none, t.insertIfNew k v ht |>.impl)
   | some b => (some b, t)
 
@@ -617,7 +617,7 @@ information but still assumes the preconditions of `getThenInsertIfNew?`, otherw
 @[inline]
 def getThenInsertIfNew?! [Ord α] (k : α) (v : β) (t : Impl α (fun _ => β))
     : Option β × Impl α (fun _ => β) :=
-  match get? t k with
+  match get? k t with
   | none => (none, t.insertIfNew! k v)
   | some b => (some b, t)
 

src/Std/Data/DTreeMap/Internal/Queries.lean

@@ -62,122 +62,122 @@ def isEmpty (t : Impl α β) : Bool :=
   | .inner _ _ _ _ _ => false
 
 /-- Returns the value for the key `k`, or `none` if such a key does not exist. -/
-def get? [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) : Option (β k) :=
+def get? [Ord α] [LawfulEqOrd α] (k : α) (t : Impl α β) : Option (β k) :=
   match t with
   | .leaf => none
   | .inner _ k' v' l r =>
     match h : compare k k' with
-    | .lt => get? l k
-    | .gt => get? r k
+    | .lt => get? k l
+    | .gt => get? k r
     | .eq => some (cast (congrArg β (compare_eq_iff_eq.mp h).symm) v')
 
 /-- Returns the value for the key `k`. -/
-def get [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) (hlk : t.contains k = true) : β k :=
+def get [Ord α] [LawfulEqOrd α] (k : α) (t : Impl α β) (hlk : t.contains k = true) : β k :=
   match t with
   | .inner _ k' v' l r =>
     match h : compare k k' with
-    | .lt => get l k (by simpa [contains, h] using hlk)
-    | .gt => get r k (by simpa [contains, h] using hlk)
+    | .lt => get k l (by simpa [contains, h] using hlk)
+    | .gt => get k r (by simpa [contains, h] using hlk)
     | .eq => cast (congrArg β (compare_eq_iff_eq.mp h).symm) v'
 
 /-- Returns the value for the key `k`, or panics if such a key does not exist. -/
-def get! [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) [Inhabited (β k)] : β k :=
+def get! [Ord α] [LawfulEqOrd α] (k : α) (t : Impl α β) [Inhabited (β k)] : β k :=
   match t with
   | .leaf => panic! "Key is not present in map"
   | .inner _ k' v' l r =>
     match h : compare k k' with
-    | .lt => get! l k
-    | .gt => get! r k
+    | .lt => get! k l
+    | .gt => get! k r
     | .eq => cast (congrArg β (compare_eq_iff_eq.mp h).symm) v'
 
 /-- Returns the value for the key `k`, or `fallback` if such a key does not exist. -/
-def getD [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) (fallback : β k) : β k :=
+def getD [Ord α] [LawfulEqOrd α] (k : α) (t : Impl α β) (fallback : β k) : β k :=
   match t with
   | .leaf => fallback
   | .inner _ k' v' l r =>
     match h : compare k k' with
-    | .lt => getD l k fallback
-    | .gt => getD r k fallback
+    | .lt => getD k l fallback
+    | .gt => getD k r fallback
     | .eq => cast (congrArg β (compare_eq_iff_eq.mp h).symm) v'
 
 /-- Implementation detail of the tree map -/
-def getKey? [Ord α] (t : Impl α β) (k : α) : Option α :=
+def getKey? [Ord α] (k : α) (t : Impl α β) : Option α :=
   match t with
   | .leaf => none
   | .inner _ k' _ l r =>
     match compare k k' with
-    | .lt => getKey? l k
-    | .gt => getKey? r k
+    | .lt => getKey? k l
+    | .gt => getKey? k r
     | .eq => some k'
 
 /-- Implementation detail of the tree map -/
-def getKey [Ord α] (t : Impl α β) (k : α) (hlk : t.contains k = true) : α :=
+def getKey [Ord α] (k : α) (t : Impl α β) (hlk : t.contains k = true) : α :=
   match t with
   | .inner _ k' _ l r =>
     match h : compare k k' with
-    | .lt => getKey l k (by simpa [contains, h] using hlk)
-    | .gt => getKey r k (by simpa [contains, h] using hlk)
+    | .lt => getKey k l (by simpa [contains, h] using hlk)
+    | .gt => getKey k r (by simpa [contains, h] using hlk)
     | .eq => k'
 
 /-- Implementation detail of the tree map -/
-def getKey! [Ord α] (t : Impl α β) (k : α) [Inhabited α] : α :=
+def getKey! [Ord α] (k : α) (t : Impl α β) [Inhabited α] : α :=
   match t with
   | .leaf => panic! "Key is not present in map"
   | .inner _ k' _ l r =>
     match compare k k' with
-    | .lt => getKey! l k
-    | .gt => getKey! r k
+    | .lt => getKey! k l
+    | .gt => getKey! k r
     | .eq => k'
 
 /-- Implementation detail of the tree map -/
-def getKeyD [Ord α] (t : Impl α β) (k : α) (fallback : α) : α :=
+def getKeyD [Ord α] (k : α) (t : Impl α β) (fallback : α) : α :=
   match t with
   | .leaf => fallback
   | .inner _ k' _ l r =>
     match compare k k' with
-    | .lt => getKeyD l k fallback
-    | .gt => getKeyD r k fallback
+    | .lt => getKeyD k l fallback
+    | .gt => getKeyD k r fallback
     | .eq => k'
 
 namespace Const
 
 /-- Returns the value for the key `k`, or `none` if such a key does not exist. -/
-def get? [Ord α] (t : Impl α δ) (k : α) : Option δ :=
+def get? [Ord α] (k : α) (t : Impl α δ) : Option δ :=
   match t with
   | .leaf => none
   | .inner _ k' v' l r =>
     match compare k k' with
-    | .lt => get? l k
-    | .gt => get? r k
+    | .lt => get? k l
+    | .gt => get? k r
     | .eq => some v'
 
 /-- Returns the value for the key `k`. -/
-def get [Ord α] (t : Impl α δ) (k : α) (hlk : t.contains k = true) : δ :=
+def get [Ord α] (k : α) (t : Impl α δ) (hlk : t.contains k = true) : δ :=
   match t with
   | .inner _ k' v' l r =>
     match h : compare k k' with
-    | .lt => get l k (by simpa [contains, h] using hlk)
-    | .gt => get r k (by simpa [contains, h] using hlk)
+    | .lt => get k l (by simpa [contains, h] using hlk)
+    | .gt => get k r (by simpa [contains, h] using hlk)
     | .eq => v'
 
 /-- Returns the value for the key `k`, or panics if such a key does not exist. -/
-def get! [Ord α] (t : Impl α δ) (k : α) [Inhabited δ] : δ :=
+def get! [Ord α] (k : α) (t : Impl α δ) [Inhabited δ] : δ :=
   match t with
   | .leaf => panic! "Key is not present in map"
   | .inner _ k' v' l r =>
     match compare k k' with
-    | .lt => get! l k
-    | .gt => get! r k
+    | .lt => get! k l
+    | .gt => get! k r
     | .eq => v'
 
 /-- Returns the value for the key `k`, or `fallback` if such a key does not exist. -/
-def getD [Ord α] (t : Impl α δ) (k : α) (fallback : δ) : δ :=
+def getD [Ord α] (k : α) (t : Impl α δ) (fallback : δ) : δ :=
   match t with
   | .leaf => fallback
   | .inner _ k' v' l r =>
     match compare k k' with
-    | .lt => getD l k fallback
-    | .gt => getD r k fallback
+    | .lt => getD k l fallback
+    | .gt => getD k r fallback
     | .eq => v'
 
 end Const

src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean

@@ -546,7 +546,7 @@ theorem contains_eq_containsKey [Ord α] [TransOrd α] {k : α} {l : Impl α β}
   rw [contains_eq_containsₘ, containsₘ_eq_containsKey hlo]
 
 /-!
-### `get?`
+''' `get?`
 -/
 
 theorem get?ₘ_eq_getValueCast? [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β}
@@ -564,62 +564,16 @@ theorem get?_eq_getValueCast? [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {
     (hto : t.Ordered) : t.get? k = getValueCast? k t.toListModel := by
   rw [get?_eq_get?ₘ, get?ₘ_eq_getValueCast? hto]
 
-/-!
-### `get`
--/
-
-theorem contains_eq_isSome_get?ₘ [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β}
-    (hto : t.Ordered) : contains k t = (t.get?ₘ k).isSome := by
-  rw [get?ₘ_eq_getValueCast? hto, contains_eq_containsKey hto, containsKey_eq_isSome_getValueCast?]
-
-theorem getₘ_eq_getValueCast [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} (h) {h'}
-    (hto : t.Ordered) : t.getₘ k h' = getValueCast k t.toListModel h := by
-  simp only [getₘ]
-  revert h'
-  rw [get?ₘ_eq_getValueCast? hto]
-  simp [getValueCast?_eq_some_getValueCast ‹_›]
-
-theorem get_eq_getValueCast [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {h}
-    (hto : t.Ordered): t.get k h = getValueCast k t.toListModel (contains_eq_containsKey hto ▸ h) := by
-  rw [get_eq_getₘ, getₘ_eq_getValueCast _ hto]
-  exact contains_eq_isSome_get?ₘ hto ▸ h
-
-/-!
-### `get!`
--/
-
-theorem get!ₘ_eq_getValueCast! [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} [Inhabited (β k)]
-    {t : Impl α β} (hto : t.Ordered) : t.get!ₘ k = getValueCast! k t.toListModel := by
-  simp [get!ₘ, get?ₘ_eq_getValueCast? hto, getValueCast!_eq_getValueCast?]
-
-theorem get!_eq_getValueCast! [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} [Inhabited (β k)]
-    {t : Impl α β} (hto : t.Ordered) : t.get! k = getValueCast! k t.toListModel := by
-  rw [get!_eq_get!ₘ, get!ₘ_eq_getValueCast! hto]
-
-/-!
-### `getD`
--/
-
-theorem getDₘ_eq_getValueCastD [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α}
-    {t : Impl α β} {fallback : β k} (hto : t.Ordered) :
-    t.getDₘ k fallback = getValueCastD k t.toListModel fallback := by
-  simp [getDₘ, get?ₘ_eq_getValueCast? hto, getValueCastD_eq_getValueCast?]
-
-theorem getD_eq_getValueCastD [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α}
-    {t : Impl α β} {fallback : β k} (hto : t.Ordered) :
-    t.getD k fallback = getValueCastD k t.toListModel fallback := by
-  rw [getD_eq_getDₘ, getDₘ_eq_getValueCastD hto]
-
 namespace Const
 
 variable {β : Type v}
 
 /-!
-### `get?`
+''' `get?`
 -/
 
 theorem get?ₘ_eq_getValue? [Ord α] [TransOrd α] {k : α} {t : Impl α (fun _ => β)} (hto : t.Ordered) :
-    get?ₘ t k = getValue? k t.toListModel := by
+    get?ₘ k t = getValue? k t.toListModel := by
   rw [get?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => getValue? k l)]
   · rintro ⟨(_|p), hp⟩ -
     · simp [Cell.Const.get?]
@@ -630,55 +584,9 @@ theorem get?ₘ_eq_getValue? [Ord α] [TransOrd α] {k : α} {t : Impl α (fun _
   · exact fun l₁ l₂ h => getValue?_append_of_containsKey_eq_false
 
 theorem get?_eq_getValue? [Ord α] [TransOrd α] {k : α} {t : Impl α (fun _ => β)} (hto : t.Ordered) :
-    get? t k = getValue? k t.toListModel := by
+    get? k t = getValue? k t.toListModel := by
   rw [get?_eq_get?ₘ, get?ₘ_eq_getValue? hto]
 
-/-!
-### `get`
--/
-
-theorem contains_eq_isSome_get?ₘ [Ord α] [TransOrd α] {k : α} {t : Impl α β}
-    (hto : t.Ordered) : contains k t = (get?ₘ t k).isSome := by
-  rw [get?ₘ_eq_getValue? hto, contains_eq_containsKey hto, containsKey_eq_isSome_getValue?]
-
-theorem getₘ_eq_getValue [Ord α] [TransOrd α] {k : α} {t : Impl α β} (h) {h'}
-    (hto : t.Ordered) : getₘ t k h' = getValue k t.toListModel h := by
-  simp only [getₘ]
-  revert h'
-  rw [get?ₘ_eq_getValue? hto]
-  simp [getValue?_eq_some_getValue ‹_›]
-
-theorem get_eq_getValue [Ord α] [TransOrd α] {k : α} {t : Impl α β} {h}
-    (hto : t.Ordered): get t k h = getValue k t.toListModel (contains_eq_containsKey hto ▸ h) := by
-  rw [get_eq_getₘ, getₘ_eq_getValue _ hto]
-  exact contains_eq_isSome_get?ₘ hto ▸ h
-
-/-!
-### `get!`
--/
-
-theorem get!ₘ_eq_getValue! [Ord α] [TransOrd α] {k : α} [Inhabited β]
-    {t : Impl α β} (hto : t.Ordered) : get!ₘ t k = getValue! k t.toListModel := by
-  simp [get!ₘ, get?ₘ_eq_getValue? hto, getValue!_eq_getValue?]
-
-theorem get!_eq_getValue! [Ord α] [TransOrd α] {k : α} [Inhabited β]
-    {t : Impl α β} (hto : t.Ordered) : get! t k = getValue! k t.toListModel := by
-  rw [get!_eq_get!ₘ, get!ₘ_eq_getValue! hto]
-
-/-!
-### `getD`
--/
-
-theorem getDₘ_eq_getValueD [Ord α] [TransOrd α] {k : α}
-    {t : Impl α β} {fallback : β} (hto : t.Ordered) :
-    getDₘ t k fallback = getValueD k t.toListModel fallback := by
-  simp [getDₘ, get?ₘ_eq_getValue? hto, getValueD_eq_getValue?]
-
-theorem getD_eq_getValueD [Ord α] [TransOrd α] {k : α}
-    {t : Impl α β} {fallback : β} (hto : t.Ordered) :
-    getD t k fallback = getValueD k t.toListModel fallback := by
-  rw [getD_eq_getDₘ, getDₘ_eq_getValueD hto]
-
 end Const
 
 /-!

src/Std/Data/DTreeMap/Lemmas.lean

@@ -142,7 +142,7 @@ theorem size_insert_le [TransCmp cmp] {k : α} {v : β k} :
 
 @[simp]
 theorem erase_emptyc {k : α} :
-    (∅ : DTreeMap α β cmp).erase k = ∅ :=
+    (∅ : DTreeMap α β cmp).erase k = empty :=
   ext <| Impl.erase_empty (instOrd := ⟨cmp⟩) (k := k)
 
 @[simp]
@@ -339,305 +339,4 @@ theorem get?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) :
 
 end Const
 
-theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {h₁} :
-    (t.insert k v).get a h₁ =
-      if h₂ : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂)) v
-      else
-        t.get a (mem_of_mem_insert h₁ h₂) :=
-  Impl.get_insert t.wf
-
-@[simp]
-theorem get_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
-    (t.insert k v).get k mem_insert_self = v :=
-  Impl.get_insert_self t.wf
-
-@[simp]
-theorem get_erase [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {h'} :
-    (t.erase k).get a h' = t.get a (mem_of_mem_erase h') :=
-  Impl.get_erase t.wf
-
-theorem get?_eq_some_get [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {h'} :
-    t.get? a = some (t.get a h') :=
-  Impl.get?_eq_some_get t.wf
-
-namespace Const
-
-variable {β : Type v} {t : DTreeMap α β cmp}
-
-theorem get_insert [TransCmp cmp] {k a : α} {v : β} {h₁} :
-    get (t.insert k v) a h₁ =
-      if h₂ : cmp k a = .eq then v
-      else get t a (mem_of_mem_insert h₁ h₂) :=
-  Impl.Const.get_insert t.wf
-
-@[simp]
-theorem get_insert_self [TransCmp cmp] {k : α} {v : β} :
-    get (t.insert k v) k mem_insert_self = v :=
-  Impl.Const.get_insert_self t.wf
-
-@[simp]
-theorem get_erase [TransCmp cmp] {k a : α} {h'} :
-    get (t.erase k) a h' = get t a (mem_of_mem_erase h') :=
-  Impl.Const.get_erase t.wf
-
-theorem get?_eq_some_get [TransCmp cmp] {a : α} {h} :
-    get? t a = some (get t a h) :=
-  Impl.Const.get?_eq_some_get t.wf
-
-theorem get_eq_get [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {h} : get t a h = t.get a h :=
-  Impl.Const.get_eq_get t.wf
-
-theorem get_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) {h'} :
-    get t a h' = get t b ((mem_congr hab).mp h') :=
-  Impl.Const.get_congr t.wf hab
-
-end Const
-
-@[simp]
-theorem get!_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    get! (∅ : DTreeMap α β cmp) a = default :=
-  Impl.get!_empty
-
-theorem get!_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    t.isEmpty = true → t.get! a = default :=
-  Impl.get!_of_isEmpty t.wf
-
-theorem get!_insert [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] {v : β k} :
-    (t.insert k v).get! a =
-      if h : cmp k a = .eq then cast (congrArg β (compare_eq_iff_eq.mp h)) v else t.get! a :=
-  Impl.get!_insert t.wf
-
-@[simp]
-theorem get!_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] {b : β a} :
-    (t.insert a b).get! a = b :=
-  Impl.get!_insert_self t.wf
-
-theorem get!_eq_default_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α}
-    [Inhabited (β a)] : t.contains a = false → t.get! a = default :=
-  Impl.get!_eq_default_of_contains_eq_false t.wf
-
-theorem get!_eq_default [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    ¬ a ∈ t → t.get! a = default :=
-  Impl.get!_eq_default t.wf
-
-theorem get!_erase [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] :
-    (t.erase k).get! a = if cmp k a = .eq then default else t.get! a :=
-  Impl.get!_erase t.wf
-
-@[simp]
-theorem get!_erase_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} [Inhabited (β k)] :
-    (t.erase k).get! k = default :=
-  Impl.get!_erase_self t.wf
-
-theorem get?_eq_some_get!_of_contains [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    t.contains a = true → t.get? a = some (t.get! a) :=
-  Impl.get?_eq_some_get!_of_contains t.wf
-
-theorem get?_eq_some_get! [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    a ∈ t → t.get? a = some (t.get! a) :=
-  Impl.get?_eq_some_get! t.wf
-
-theorem get!_eq_get!_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    t.get! a = (t.get? a).get! :=
-  Impl.get!_eq_get!_get? t.wf
-
-theorem get_eq_get! [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] {h} :
-    t.get a h = t.get! a :=
-  Impl.get_eq_get! t.wf
-
-namespace Const
-
-variable {β : Type v} {t : DTreeMap α β cmp}
-
-@[simp]
-theorem get!_emptyc [TransCmp cmp] [Inhabited β] {a : α} :
-    get! (∅ : DTreeMap α β cmp) a = default :=
-  Impl.Const.get!_empty
-
-theorem get!_of_isEmpty [TransCmp cmp] [Inhabited β] {a : α} :
-    t.isEmpty = true → get! t a = default :=
-  Impl.Const.get!_of_isEmpty t.wf
-
-theorem get!_insert [TransCmp cmp] [Inhabited β] {k a : α} {v : β} :
-    get! (t.insert k v) a = if cmp k a = .eq then v else get! t a :=
-  Impl.Const.get!_insert t.wf
-
-@[simp]
-theorem get!_insert_self [TransCmp cmp] [Inhabited β] {k : α} {v : β} : get! (t.insert k v) k = v :=
-  Impl.Const.get!_insert_self t.wf
-
-theorem get!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited β] {a : α} :
-    t.contains a = false → get! t a = default :=
-  Impl.Const.get!_eq_default_of_contains_eq_false t.wf
-
-theorem get!_eq_default [TransCmp cmp] [Inhabited β] {a : α} :
-    ¬ a ∈ t → get! t a = default :=
-  Impl.Const.get!_eq_default t.wf
-
-theorem get!_erase [TransCmp cmp] [Inhabited β] {k a : α} :
-    get! (t.erase k) a = if cmp k a = .eq then default else get! t a :=
-  Impl.Const.get!_erase t.wf
-
-@[simp]
-theorem get!_erase_self [TransCmp cmp] [Inhabited β] {k : α} :
-    get! (t.erase k) k = default :=
-  Impl.Const.get!_erase_self t.wf
-
-theorem get?_eq_some_get!_of_contains [TransCmp cmp] [Inhabited β] {a : α} :
-    t.contains a = true → get? t a = some (get! t a) :=
-  Impl.Const.get?_eq_some_get! t.wf
-
-theorem get?_eq_some_get! [TransCmp cmp] [Inhabited β] {a : α} :
-    a ∈ t → get? t a = some (get! t a) :=
-  Impl.Const.get?_eq_some_get! t.wf
-
-theorem get!_eq_get!_get? [TransCmp cmp] [Inhabited β] {a : α} :
-    get! t a = (get? t a).get! :=
-  Impl.Const.get!_eq_get!_get? t.wf
-
-theorem get_eq_get! [TransCmp cmp] [Inhabited β] {a : α} {h} :
-    get t a h = get! t a :=
-  Impl.Const.get_eq_get! t.wf
-
-theorem get!_eq_get! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited β] {a : α} :
-    get! t a = t.get! a :=
-  Impl.Const.get!_eq_get! t.wf
-
-theorem get!_congr [TransCmp cmp] [Inhabited β] {a b : α} (hab : cmp a b = .eq) :
-    get! t a = get! t b :=
-  Impl.Const.get!_congr t.wf hab
-
-end Const
-
-@[simp]
-theorem getD_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    (∅ : DTreeMap α β cmp).getD a fallback = fallback :=
-  Impl.getD_empty
-
-theorem getD_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    t.isEmpty = true → t.getD a fallback = fallback :=
-  Impl.getD_of_isEmpty t.wf
-
-theorem getD_insert [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
-    (t.insert k v).getD a fallback =
-      if h : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h)) v
-      else t.getD a fallback :=
-  Impl.getD_insert t.wf
-
-@[simp]
-theorem getD_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback b : β a} :
-    (t.insert a b).getD a fallback = b :=
-  Impl.getD_insert_self t.wf
-
-theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α}
-    {fallback : β a} : t.contains a = false → t.getD a fallback = fallback :=
-  Impl.getD_eq_fallback_of_contains_eq_false t.wf
-
-theorem getD_eq_fallback [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    ¬ a ∈ t → t.getD a fallback = fallback :=
-  Impl.getD_eq_fallback t.wf
-
-theorem getD_erase [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} :
-    (t.erase k).getD a fallback = if cmp k a = .eq then fallback else t.getD a fallback :=
-  Impl.getD_erase t.wf
-
-@[simp]
-theorem getD_erase_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {fallback : β k} :
-    (t.erase k).getD k fallback = fallback :=
-  Impl.getD_erase_self t.wf
-
-theorem get?_eq_some_getD_of_contains [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    t.contains a = true → t.get? a = some (t.getD a fallback) :=
-  Impl.get?_eq_some_getD_of_contains t.wf
-
-theorem get?_eq_some_getD [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    a ∈ t → t.get? a = some (t.getD a fallback) :=
-  Impl.get?_eq_some_getD t.wf
-
-theorem getD_eq_getD_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    t.getD a fallback = (t.get? a).getD fallback :=
-  Impl.getD_eq_getD_get? t.wf
-
-theorem get_eq_getD [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} {h} :
-    t.get a h = t.getD a fallback :=
-  Impl.get_eq_getD t.wf
-
-theorem get!_eq_getD_default [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    t.get! a = t.getD a default :=
-  Impl.get!_eq_getD_default t.wf
-
-namespace Const
-
-variable {β : Type v} {t : DTreeMap α β cmp}
-
-@[simp]
-theorem getD_emptyc [TransCmp cmp] {a : α} {fallback : β} :
-    getD (∅ : DTreeMap α β cmp) a fallback = fallback :=
-  Impl.Const.getD_empty
-
-theorem getD_of_isEmpty [TransCmp cmp] {a : α} {fallback : β} :
-    t.isEmpty = true → getD t a fallback = fallback :=
-  Impl.Const.getD_of_isEmpty t.wf
-
-theorem getD_insert [TransCmp cmp] {k a : α} {fallback v : β} :
-    getD (t.insert k v) a fallback = if cmp k a = .eq then v else getD t a fallback :=
-  Impl.Const.getD_insert t.wf
-
-@[simp]
-theorem getD_insert_self [TransCmp cmp] {k : α} {fallback v : β} :
-    getD (t.insert k v) k fallback = v :=
-  Impl.Const.getD_insert_self t.wf
-
-theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] {a : α} {fallback : β} :
-    t.contains a = false → getD t a fallback = fallback :=
-  Impl.Const.getD_eq_fallback_of_contains_eq_false t.wf
-
-theorem getD_eq_fallback [TransCmp cmp] {a : α} {fallback : β} :
-    ¬ a ∈ t → getD t a fallback = fallback :=
-  Impl.Const.getD_eq_fallback t.wf
-
-theorem getD_erase [TransCmp cmp] {k a : α} {fallback : β} :
-    getD (t.erase k) a fallback = if cmp k a = .eq then
-      fallback
-    else
-      getD t a fallback :=
-  Impl.Const.getD_erase t.wf
-
-@[simp]
-theorem getD_erase_self [TransCmp cmp] {k : α} {fallback : β} :
-    getD (t.erase k) k fallback = fallback :=
-  Impl.Const.getD_erase_self t.wf
-
-theorem get?_eq_some_getD_of_contains [TransCmp cmp] {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) :=
-  Impl.Const.get?_eq_some_getD_of_contains t.wf
-
-theorem get?_eq_some_getD [TransCmp cmp] {a : α} {fallback : β} :
-    a ∈ t → get? t a = some (getD t a fallback) :=
-  Impl.Const.get?_eq_some_getD t.wf
-
-theorem getD_eq_getD_get? [TransCmp cmp] {a : α} {fallback : β} :
-    getD t a fallback = (get? t a).getD fallback :=
-  Impl.Const.getD_eq_getD_get? t.wf
-
-theorem get_eq_getD [TransCmp cmp] {a : α} {fallback : β} {h} :
-    get t a h = getD t a fallback :=
-  Impl.Const.get_eq_getD t.wf
-
-theorem get!_eq_getD_default [TransCmp cmp] [Inhabited β] {a : α} :
-    get! t a = getD t a default :=
-  Impl.Const.get!_eq_getD_default t.wf
-
-theorem getD_eq_getD [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β} :
-    getD t a fallback = t.getD a fallback :=
-  Impl.Const.getD_eq_getD t.wf
-
-theorem getD_congr [TransCmp cmp] {a b : α} {fallback : β} (hab : cmp a b = .eq) :
-    getD t a fallback = getD t b fallback :=
-  Impl.Const.getD_congr t.wf hab
-
-end Const
-
 end Std.DTreeMap

src/Std/Data/DTreeMap/Raw.lean

@@ -411,7 +411,7 @@ def getThenInsertIfNew? (t : Raw α β cmp) (a : α) (b : β) : Option β × Raw
 
 @[inline, inherit_doc DTreeMap.Const.get?]
 def get? (t : Raw α β cmp) (a : α) : Option β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.get? t.inner a
+  letI : Ord α := ⟨cmp⟩; Impl.Const.get? a t.inner
 
 @[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
 def find? (t : Raw α β cmp) (a : α) : Option β :=
@@ -419,11 +419,11 @@ def find? (t : Raw α β cmp) (a : α) : Option β :=
 
 @[inline, inherit_doc DTreeMap.Const.get]
 def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.get t.inner a h
+  letI : Ord α := ⟨cmp⟩; Impl.Const.get a t.inner h
 
 @[inline, inherit_doc DTreeMap.Const.get!]
 def get! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.get! t.inner a
+  letI : Ord α := ⟨cmp⟩; Impl.Const.get! a t.inner
 
 @[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
 def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
@@ -431,7 +431,7 @@ def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
 
 @[inline, inherit_doc DTreeMap.Const.getD]
 def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.getD t.inner a fallback
+  letI : Ord α := ⟨cmp⟩; Impl.Const.getD a t.inner fallback
 
 @[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
 def findD (t : Raw α β cmp) (a : α) (fallback : β) : β :=

src/Std/Data/DTreeMap/RawLemmas.lean

@@ -142,7 +142,7 @@ theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
 
 @[simp]
 theorem erase_emptyc {k : α} :
-    (∅ : Raw α β cmp).erase k = ∅ :=
+    (∅ : Raw α β cmp).erase k = empty :=
   ext <| Impl.erase!_empty (instOrd := ⟨cmp⟩) (k := k)
 
 @[simp]
@@ -339,307 +339,4 @@ theorem get?_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq) :
 
 end Const
 
-theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
-    (t.insert k v).get a h₁ =
-      if h₂ : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂)) v
-      else
-        t.get a (mem_of_mem_insert h h₁ h₂) :=
-  Impl.get_insert! h
-
-@[simp]
-theorem get_insert_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
-    (t.insert k v).get k (mem_insert_self h) = v :=
-  Impl.get_insert!_self h
-
-@[simp]
-theorem get_erase [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {h'} :
-    (t.erase k).get a h' = t.get a (mem_of_mem_erase h h') :=
-  Impl.get_erase! h
-
-theorem get?_eq_some_get [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {h'} :
-    t.get? a = some (t.get a h') :=
-  Impl.get?_eq_some_get h
-
-namespace Const
-
-variable {β : Type v} {t : Raw α β cmp}
-
-theorem get_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁} :
-    get (t.insert k v) a h₁ =
-      if h₂ : cmp k a = .eq then v
-      else get t a (mem_of_mem_insert h h₁ h₂) :=
-  Impl.Const.get_insert! h
-
-@[simp]
-theorem get_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    get (t.insert k v) k (mem_insert_self h) = v :=
-  Impl.Const.get_insert!_self h
-
-@[simp]
-theorem get_erase [TransCmp cmp] (h : t.WF) {k a : α} {h'} :
-    get (t.erase k) a h' = get t a (mem_of_mem_erase h h') :=
-  Impl.Const.get_erase! h
-
-theorem get?_eq_some_get [TransCmp cmp] (h : t.WF) {a : α} {h'} :
-    get? t a = some (get t a h') :=
-  Impl.Const.get?_eq_some_get h
-
-theorem get_eq_get [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {h'} :
-    get t a h' = t.get a h' :=
-  Impl.Const.get_eq_get h
-
-theorem get_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq) {h'} :
-    get t a h' = get t b ((mem_congr h hab).mp h') :=
-  Impl.Const.get_congr h hab
-
-end Const
-
-@[simp]
-theorem get!_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
-    get! (∅ : Raw α β cmp) a = default :=
-  Impl.get!_empty
-
-theorem get!_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [Inhabited (β a)] :
-    t.isEmpty = true → t.get! a = default :=
-  Impl.get!_of_isEmpty h
-
-theorem get!_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} [Inhabited (β a)]
-    {v : β k} : (t.insert k v).get! a =
-      if h : cmp k a = .eq then cast (congrArg β (compare_eq_iff_eq.mp h)) v else t.get! a :=
-  Impl.get!_insert! h
-
-@[simp]
-theorem get!_insert_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [Inhabited (β a)]
-    {b : β a} : (t.insert a b).get! a = b :=
-  Impl.get!_insert!_self h
-
-theorem get!_eq_default_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α}
-    [Inhabited (β a)] : t.contains a = false → t.get! a = default :=
-  Impl.get!_eq_default_of_contains_eq_false h
-
-theorem get!_eq_default [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [Inhabited (β a)] :
-    ¬ a ∈ t → t.get! a = default :=
-  Impl.get!_eq_default h
-
-theorem get!_erase [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} [Inhabited (β a)] :
-    (t.erase k).get! a = if cmp k a = .eq then default else t.get! a :=
-  Impl.get!_erase! h
-
-@[simp]
-theorem get!_erase_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} [Inhabited (β k)] :
-    (t.erase k).get! k = default :=
-  Impl.get!_erase!_self h
-
-theorem get?_eq_some_get!_of_contains [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α}
-    [Inhabited (β a)] : t.contains a = true → t.get? a = some (t.get! a) :=
-  Impl.get?_eq_some_get!_of_contains h
-
-theorem get?_eq_some_get! [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [Inhabited (β a)] :
-    a ∈ t → t.get? a = some (t.get! a) :=
-  Impl.get?_eq_some_get! h
-
-theorem get!_eq_get!_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [Inhabited (β a)] :
-    t.get! a = (t.get? a).get! :=
-  Impl.get!_eq_get!_get? h
-
-theorem get_eq_get! [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [Inhabited (β a)] {h'} :
-    t.get a h' = t.get! a :=
-  Impl.get_eq_get! h
-
-namespace Const
-
-variable {β : Type v} {t : Raw α β cmp}
-
-@[simp]
-theorem get!_emptyc [TransCmp cmp] [Inhabited β] {a : α} :
-    get! (∅ : Raw α β cmp) a = default :=
-  Impl.Const.get!_empty
-
-theorem get!_of_isEmpty [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t.isEmpty = true → get! t a = default :=
-  Impl.Const.get!_of_isEmpty h
-
-theorem get!_insert [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} {v : β} :
-    get! (t.insert k v) a = if cmp k a = .eq then v else get! t a :=
-  Impl.Const.get!_insert! h
-
-@[simp]
-theorem get!_insert_self [TransCmp cmp] [Inhabited β] (h : t.WF) {k : α} {v : β} :
-    get! (t.insert k v) k = v :=
-  Impl.Const.get!_insert!_self h
-
-theorem get!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t.contains a = false → get! t a = default :=
-  Impl.Const.get!_eq_default_of_contains_eq_false h
-
-theorem get!_eq_default [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    ¬ a ∈ t → get! t a = default :=
-  Impl.Const.get!_eq_default h
-
-theorem get!_erase [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} :
-    get! (t.erase k) a = if cmp k a = .eq then default else get! t a :=
-  Impl.Const.get!_erase! h
-
-@[simp]
-theorem get!_erase_self [TransCmp cmp] [Inhabited β] (h : t.WF) {k : α} :
-    get! (t.erase k) k = default :=
-  Impl.Const.get!_erase!_self h
-
-theorem get?_eq_some_get!_of_contains [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t.contains a = true → get? t a = some (get! t a) :=
-  Impl.Const.get?_eq_some_get! h
-
-theorem get?_eq_some_get! [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    a ∈ t → get? t a = some (get! t a) :=
-  Impl.Const.get?_eq_some_get! h
-
-theorem get!_eq_get!_get? [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    get! t a = (get? t a).get! :=
-  Impl.Const.get!_eq_get!_get? h
-
-theorem get_eq_get! [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} {h'} :
-    get t a h' = get! t a :=
-  Impl.Const.get_eq_get! h
-
-theorem get!_eq_get! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    get! t a = t.get! a :=
-  Impl.Const.get!_eq_get! h
-
-theorem get!_congr [TransCmp cmp] [Inhabited β] (h : t.WF) {a b : α} (hab : cmp a b = .eq) :
-    get! t a = get! t b :=
-  Impl.Const.get!_congr h hab
-
-end Const
-
-@[simp]
-theorem getD_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    (∅ : DTreeMap α β cmp).getD a fallback = fallback :=
-  Impl.getD_empty
-
-theorem getD_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β a} :
-    t.isEmpty = true → t.getD a fallback = fallback :=
-  Impl.getD_of_isEmpty h
-
-theorem getD_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
-    (t.insert k v).getD a fallback =
-      if h : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h)) v
-      else t.getD a fallback :=
-  Impl.getD_insert! h
-
-@[simp]
-theorem getD_insert_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback b : β a} :
-    (t.insert a b).getD a fallback = b :=
-  Impl.getD_insert!_self h
-
-theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β a} :
-    t.contains a = false → t.getD a fallback = fallback :=
-  Impl.getD_eq_fallback_of_contains_eq_false h
-
-theorem getD_eq_fallback [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β a} :
-    ¬ a ∈ t → t.getD a fallback = fallback :=
-  Impl.getD_eq_fallback h
-
-theorem getD_erase [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {fallback : β a} :
-    (t.erase k).getD a fallback = if cmp k a = .eq then fallback else t.getD a fallback :=
-  Impl.getD_erase! h
-
-@[simp]
-theorem getD_erase_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {fallback : β k} :
-    (t.erase k).getD k fallback = fallback :=
-  Impl.getD_erase!_self h
-
-theorem get?_eq_some_getD_of_contains [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α}
-    {fallback : β a} : t.contains a = true → t.get? a = some (t.getD a fallback) :=
-  Impl.get?_eq_some_getD_of_contains h
-
-theorem get?_eq_some_getD [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β a} :
-    a ∈ t → t.get? a = some (t.getD a fallback) :=
-  Impl.get?_eq_some_getD h
-
-theorem getD_eq_getD_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β a} :
-    t.getD a fallback = (t.get? a).getD fallback :=
-  Impl.getD_eq_getD_get? h
-
-theorem get_eq_getD [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β a} {h'} :
-    t.get a h' = t.getD a fallback :=
-  Impl.get_eq_getD h
-
-theorem get!_eq_getD_default [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [Inhabited (β a)] :
-    t.get! a = t.getD a default :=
-  Impl.get!_eq_getD_default h
-
-namespace Const
-
-variable {β : Type v} {t : Raw α β cmp}
-
-@[simp]
-theorem getD_emptyc [TransCmp cmp] {a : α} {fallback : β} :
-    getD (∅ : Raw α β cmp) a fallback = fallback :=
-  Impl.Const.getD_empty
-
-theorem getD_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    t.isEmpty = true → getD t a fallback = fallback :=
-  Impl.Const.getD_of_isEmpty h
-
-theorem getD_insert [TransCmp cmp] (h : t.WF) {k a : α} {fallback v : β} :
-    getD (t.insert k v) a fallback = if cmp k a = .eq then v else getD t a fallback :=
-  Impl.Const.getD_insert! h
-
-@[simp]
-theorem getD_insert_self [TransCmp cmp] (h : t.WF) {k : α} {fallback v : β} :
-    getD (t.insert k v) k fallback = v :=
-  Impl.Const.getD_insert!_self h
-
-theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    t.contains a = false → getD t a fallback = fallback :=
-  Impl.Const.getD_eq_fallback_of_contains_eq_false h
-
-theorem getD_eq_fallback [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    ¬ a ∈ t → getD t a fallback = fallback :=
-  Impl.Const.getD_eq_fallback h
-
-theorem getD_erase [TransCmp cmp] (h : t.WF) {k a : α} {fallback : β} :
-    getD (t.erase k) a fallback = if cmp k a = .eq then
-      fallback
-    else
-      getD t a fallback :=
-  Impl.Const.getD_erase! h
-
-@[simp]
-theorem getD_erase_self [TransCmp cmp] (h : t.WF) {k : α} {fallback : β} :
-    getD (t.erase k) k fallback = fallback :=
-  Impl.Const.getD_erase!_self h
-
-theorem get?_eq_some_getD_of_contains [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) :=
-  Impl.Const.get?_eq_some_getD_of_contains h
-
-theorem get?_eq_some_getD [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    a ∈ t → get? t a = some (getD t a fallback) :=
-  Impl.Const.get?_eq_some_getD h
-
-theorem getD_eq_getD_get? [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    getD t a fallback = (get? t a).getD fallback :=
-  Impl.Const.getD_eq_getD_get? h
-
-theorem get_eq_getD [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} {h'} :
-    get t a h' = getD t a fallback :=
-  Impl.Const.get_eq_getD h
-
-theorem get!_eq_getD_default [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    get! t a = getD t a default :=
-  Impl.Const.get!_eq_getD_default h
-
-theorem getD_eq_getD [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    getD t a fallback = t.getD a fallback :=
-  Impl.Const.getD_eq_getD h
-
-theorem getD_congr [TransCmp cmp] (h : t.WF) {a b : α} {fallback : β} (hab : cmp a b = .eq) :
-    getD t a fallback = getD t b fallback :=
-  Impl.Const.getD_congr h hab
-
-end Const
-
 end Std.DTreeMap.Raw

src/Std/Data/TreeMap/Lemmas.lean

@@ -139,7 +139,7 @@ theorem size_insert_le [TransCmp cmp] {k : α} {v : β} :
 
 @[simp]
 theorem erase_emptyc {k : α} :
-    (∅ : TreeMap α β cmp).erase k = ∅ :=
+    (∅ : TreeMap α β cmp).erase k = empty :=
   ext <| DTreeMap.erase_emptyc
 
 @[simp]
@@ -288,145 +288,4 @@ theorem getElem?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) :
     t[a]? = t[b]? :=
   DTreeMap.Const.get?_congr hab
 
-theorem getElem_insert [TransCmp cmp] {k a : α} {v : β} {h₁} :
-    (t.insert k v)[a]'h₁ =
-      if h₂ : cmp k a = .eq then v
-      else get t a (mem_of_mem_insert h₁ h₂) :=
-  DTreeMap.Const.get_insert
-
-@[simp]
-theorem getElem_insert_self [TransCmp cmp] {k : α} {v : β} :
-    (t.insert k v)[k]'mem_insert_self = v :=
-  DTreeMap.Const.get_insert_self
-
-@[simp]
-theorem getElem_erase [TransCmp cmp] {k a : α} {h'} :
-    (t.erase k)[a]'h' = t[a]'(mem_of_mem_erase h') :=
-  DTreeMap.Const.get_erase
-
-theorem getElem?_eq_some_getElem [TransCmp cmp] {a : α} {h} :
-    t[a]? = some (t[a]'h) :=
-  DTreeMap.Const.get?_eq_some_get
-
-theorem getElem_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) {h'} :
-    t[a]'h' = t[b]'((mem_congr hab).mp h') :=
-  DTreeMap.Const.get_congr hab
-
-@[simp]
-theorem getElem!_emptyc [TransCmp cmp] [Inhabited β] {a : α} :
-    (∅ : TreeMap α β cmp)[a]! = default :=
-  DTreeMap.Const.get!_emptyc (cmp := cmp) (a := a)
-
-theorem getElem!_of_isEmpty [TransCmp cmp] [Inhabited β] {a : α} :
-    t.isEmpty = true → t[a]! = default :=
-  DTreeMap.Const.get!_of_isEmpty
-
-theorem getElem!_insert [TransCmp cmp] [Inhabited β] {k a : α} {v : β} :
-    (t.insert k v)[a]! = if cmp k a = .eq then v else t[a]! :=
-  DTreeMap.Const.get!_insert
-
-@[simp]
-theorem getElem!_insert_self [TransCmp cmp] [Inhabited β] {k : α}
-    {v : β} : (t.insert k v)[k]! = v :=
-  DTreeMap.Const.get!_insert_self
-
-theorem getElem!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited β] {a : α} :
-    t.contains a = false → t[a]! = default :=
-  DTreeMap.Const.get!_eq_default_of_contains_eq_false
-
-theorem getElem!_eq_default [TransCmp cmp] [Inhabited β] {a : α} :
-    ¬ a ∈ t → t[a]! = default :=
-  DTreeMap.Const.get!_eq_default
-
-theorem getElem!_erase [TransCmp cmp] [Inhabited β] {k a : α} :
-    (t.erase k)[a]! = if cmp k a = .eq then default else t[a]! :=
-  DTreeMap.Const.get!_erase
-
-@[simp]
-theorem getElem!_erase_self [TransCmp cmp] [Inhabited β] {k : α} :
-    (t.erase k)[k]! = default :=
-  DTreeMap.Const.get!_erase_self
-
-theorem getElem?_eq_some_getElem!_of_contains [TransCmp cmp] [Inhabited β] {a : α} :
-    t.contains a = true → t[a]? = some t[a]! :=
-  DTreeMap.Const.get?_eq_some_get!
-
-theorem getElem?_eq_some_getElem! [TransCmp cmp] [Inhabited β] {a : α} :
-    a ∈ t → t[a]? = some t[a]! :=
-  DTreeMap.Const.get?_eq_some_get!
-
-theorem getElem!_eq_getElem!_getElem? [TransCmp cmp] [Inhabited β] {a : α} :
-    t[a]! = t[a]?.get! :=
-  DTreeMap.Const.get!_eq_get!_get?
-
-theorem getElem_eq_getElem! [TransCmp cmp] [Inhabited β] {a : α} {h} :
-    t[a]'h = t[a]! :=
-  DTreeMap.Const.get_eq_get!
-
-theorem getElem!_congr [TransCmp cmp] [Inhabited β] {a b : α}
-    (hab : cmp a b = .eq) : t[a]! = t[b]! :=
-  DTreeMap.Const.get!_congr hab
-
-@[simp]
-theorem getD_emptyc [TransCmp cmp] {a : α} {fallback : β} :
-    getD (∅ : TreeMap α β cmp) a fallback = fallback :=
-  DTreeMap.Const.getD_emptyc
-
-theorem getD_of_isEmpty [TransCmp cmp] {a : α} {fallback : β} :
-    t.isEmpty = true → getD t a fallback = fallback :=
-  DTreeMap.Const.getD_of_isEmpty
-
-theorem getD_insert [TransCmp cmp] {k a : α} {fallback v : β} :
-    getD (t.insert k v) a fallback = if cmp k a = .eq then v else getD t a fallback :=
-  DTreeMap.Const.getD_insert
-
-@[simp]
-theorem getD_insert_self [TransCmp cmp] {k : α} {fallback v : β} :
-    getD (t.insert k v) k fallback = v :=
-  DTreeMap.Const.getD_insert_self
-
-theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] {a : α} {fallback : β} :
-    t.contains a = false → getD t a fallback = fallback :=
-  DTreeMap.Const.getD_eq_fallback_of_contains_eq_false
-
-theorem getD_eq_fallback [TransCmp cmp] {a : α} {fallback : β} :
-    ¬ a ∈ t → getD t a fallback = fallback :=
-  DTreeMap.Const.getD_eq_fallback
-
-theorem getD_erase [TransCmp cmp] {k a : α} {fallback : β} :
-    getD (t.erase k) a fallback = if cmp k a = .eq then
-      fallback
-    else
-      getD t a fallback :=
-  DTreeMap.Const.getD_erase
-
-@[simp]
-theorem getD_erase_self [TransCmp cmp] {k : α} {fallback : β} :
-    getD (t.erase k) k fallback = fallback :=
-  DTreeMap.Const.getD_erase_self
-
-theorem getElem?_eq_some_getD_of_contains [TransCmp cmp] {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) :=
-  DTreeMap.Const.get?_eq_some_getD_of_contains
-
-theorem getElem?_eq_some_getD [TransCmp cmp] {a : α} {fallback : β} :
-    a ∈ t → t[a]? = some (getD t a fallback) :=
-  DTreeMap.Const.get?_eq_some_getD
-
-theorem getD_eq_getD_getElem? [TransCmp cmp] {a : α} {fallback : β} :
-    getD t a fallback = t[a]?.getD fallback :=
-  DTreeMap.Const.getD_eq_getD_get?
-
-theorem getElem_eq_getD [TransCmp cmp] {a : α} {fallback : β} {h} :
-    t[a]'h = getD t a fallback :=
-  DTreeMap.Const.get_eq_getD
-
-theorem getElem!_eq_getD_default [TransCmp cmp] [Inhabited β] {a : α} :
-    t[a]! = getD t a default :=
-  DTreeMap.Const.get!_eq_getD_default
-
-theorem getD_congr [TransCmp cmp] {a b : α} {fallback : β}
-    (hab : cmp a b = .eq) : getD t a fallback = getD t b fallback :=
-  DTreeMap.Const.getD_congr hab
-
 end Std.TreeMap

src/Std/Data/TreeMap/RawLemmas.lean

@@ -139,7 +139,7 @@ theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
 
 @[simp]
 theorem erase_emptyc {k : α} :
-    (∅ : Raw α β cmp).erase k = ∅ :=
+    (empty : Raw α β cmp).erase k = empty :=
   ext <| DTreeMap.Raw.erase_emptyc
 
 @[simp]
@@ -286,145 +286,4 @@ theorem getElem?_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq
     t[a]? = t[b]? :=
   DTreeMap.Raw.Const.get?_congr h hab
 
-theorem getElem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁} :
-    (t.insert k v)[a]'h₁ =
-      if h₂ : cmp k a = .eq then v
-      else t[a]'(mem_of_mem_insert h h₁ h₂) :=
-  DTreeMap.Raw.Const.get_insert h
-
-@[simp]
-theorem getElem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    (t.insert k v)[k]'(mem_insert_self h) = v :=
-  DTreeMap.Raw.Const.get_insert_self h
-
-@[simp]
-theorem getElem_erase [TransCmp cmp] (h : t.WF) {k a : α} {h'} :
-    (t.erase k)[a]'h' = t[a]'(mem_of_mem_erase h h') :=
-  DTreeMap.Raw.Const.get_erase h
-
-theorem getElem?_eq_some_getElem [TransCmp cmp] (h : t.WF) {a : α} {h'} :
-    t[a]? = some (t[a]'h') :=
-  DTreeMap.Raw.Const.get?_eq_some_get h
-
-theorem getElem_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq) {h'} :
-    t[a]'h' = t[b]'((mem_congr h hab).mp h') :=
-  DTreeMap.Raw.Const.get_congr h hab
-
-@[simp]
-theorem getElem!_emptyc [TransCmp cmp] [Inhabited β] {a : α} :
-    (∅ : Raw α β cmp)[a]! = default :=
-  DTreeMap.Raw.Const.get!_emptyc (cmp := cmp) (a := a)
-
-theorem getElem!_of_isEmpty [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t.isEmpty = true → t[a]! = default :=
-  DTreeMap.Raw.Const.get!_of_isEmpty h
-
-theorem getElem!_insert [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} {v : β} :
-    (t.insert k v)[a]! = if cmp k a = .eq then v else t[a]! :=
-  DTreeMap.Raw.Const.get!_insert h
-
-@[simp]
-theorem getElem!_insert_self [TransCmp cmp] [Inhabited β] (h : t.WF) {k : α}
-    {v : β} : (t.insert k v)[k]! = v :=
-  DTreeMap.Raw.Const.get!_insert_self h
-
-theorem getElem!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t.contains a = false → t[a]! = default :=
-  DTreeMap.Raw.Const.get!_eq_default_of_contains_eq_false h
-
-theorem getElem!_eq_default [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    ¬ a ∈ t → t[a]! = default :=
-  DTreeMap.Raw.Const.get!_eq_default h
-
-theorem getElem!_erase [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} :
-    (t.erase k)[a]! = if cmp k a = .eq then default else t[a]! :=
-  DTreeMap.Raw.Const.get!_erase h
-
-@[simp]
-theorem getElem!_erase_self [TransCmp cmp] [Inhabited β] (h : t.WF) {k : α} :
-    (t.erase k)[k]! = default :=
-  DTreeMap.Raw.Const.get!_erase_self h
-
-theorem getElem?_eq_some_getElem!_of_contains [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t.contains a = true → t[a]? = some t[a]! :=
-  DTreeMap.Raw.Const.get?_eq_some_get! h
-
-theorem getElem?_eq_some_getElem! [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    a ∈ t → t[a]? = some t[a]! :=
-  DTreeMap.Raw.Const.get?_eq_some_get! h
-
-theorem getElem!_eq_getElem!_getElem? [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t[a]! = t[a]?.get! :=
-  DTreeMap.Raw.Const.get!_eq_get!_get? h
-
-theorem getElem_eq_getElem! [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} {h'} :
-    t[a]'h' = t[a]! :=
-  DTreeMap.Raw.Const.get_eq_get! h
-
-theorem getElem!_congr [TransCmp cmp] [Inhabited β] (h : t.WF) {a b : α}
-    (hab : cmp a b = .eq) : t[a]! = t[b]! :=
-  DTreeMap.Raw.Const.get!_congr h hab
-
-@[simp]
-theorem getD_emptyc [TransCmp cmp] {a : α} {fallback : β} :
-    getD (∅ : Raw α β cmp) a fallback = fallback :=
-  DTreeMap.Raw.Const.getD_emptyc
-
-theorem getD_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    t.isEmpty = true → getD t a fallback = fallback :=
-  DTreeMap.Raw.Const.getD_of_isEmpty h
-
-theorem getD_insert [TransCmp cmp] (h : t.WF) {k a : α} {fallback v : β} :
-    getD (t.insert k v) a fallback = if cmp k a = .eq then v else getD t a fallback :=
-  DTreeMap.Raw.Const.getD_insert h
-
-@[simp]
-theorem getD_insert_self [TransCmp cmp] (h : t.WF) {k : α} {fallback v : β} :
-    getD (t.insert k v) k fallback = v :=
-  DTreeMap.Raw.Const.getD_insert_self h
-
-theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    t.contains a = false → getD t a fallback = fallback :=
-  DTreeMap.Raw.Const.getD_eq_fallback_of_contains_eq_false h
-
-theorem getD_eq_fallback [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    ¬ a ∈ t → getD t a fallback = fallback :=
-  DTreeMap.Raw.Const.getD_eq_fallback h
-
-theorem getD_erase [TransCmp cmp] (h : t.WF) {k a : α} {fallback : β} :
-    getD (t.erase k) a fallback = if cmp k a = .eq then
-      fallback
-    else
-      getD t a fallback :=
-  DTreeMap.Raw.Const.getD_erase h
-
-@[simp]
-theorem getD_erase_self [TransCmp cmp] (h : t.WF) {k : α} {fallback : β} :
-    getD (t.erase k) k fallback = fallback :=
-  DTreeMap.Raw.Const.getD_erase_self h
-
-theorem getElem?_eq_some_getD_of_contains [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) :=
-  DTreeMap.Raw.Const.get?_eq_some_getD_of_contains h
-
-theorem getElem?_eq_some_getD [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    a ∈ t → t[a]? = some (getD t a fallback) :=
-  DTreeMap.Raw.Const.get?_eq_some_getD h
-
-theorem getD_eq_getD_getElem? [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    getD t a fallback = t[a]?.getD fallback :=
-  DTreeMap.Raw.Const.getD_eq_getD_get? h
-
-theorem getElem_eq_getD [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} {h'} :
-    t[a]'h' = getD t a fallback :=
-  DTreeMap.Raw.Const.get_eq_getD h
-
-theorem getElem!_eq_getD_default [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} :
-    t[a]! = getD t a default :=
-  DTreeMap.Raw.Const.get!_eq_getD_default h
-
-theorem getD_congr [TransCmp cmp] (h : t.WF) {a b : α} {fallback : β}
-    (hab : cmp a b = .eq) : getD t a fallback = getD t b fallback :=
-  DTreeMap.Raw.Const.getD_congr h hab
-
 end Std.TreeMap.Raw

src/Std/Data/TreeSet/Lemmas.lean

@@ -134,7 +134,7 @@ theorem size_insert_le [TransCmp cmp] {k : α} :
 
 @[simp]
 theorem erase_emptyc {k : α} :
-    (∅ : TreeSet α cmp).erase k = ∅ :=
+    (empty : TreeSet α cmp).erase k = empty :=
   ext <| TreeMap.erase_emptyc
 
 @[simp]

src/Std/Data/TreeSet/RawLemmas.lean

@@ -134,7 +134,7 @@ theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} :
 
 @[simp]
 theorem erase_emptyc {k : α} :
-    (∅ : Raw α cmp).erase k = ∅ :=
+    (empty : Raw α cmp).erase k = empty :=
   ext <| TreeMap.Raw.erase_emptyc
 
 @[simp]

src/lakefile.toml.in

@@ -44,4 +44,3 @@ globs = [
 [[lean_lib]]
 name = "Lake"
 srcDir = "lake"
-moreLeanArgs = ["--plugin=${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]