Loogle!

Result

Found 2318 declarations mentioning Std.TransOrd. Of these, only the first 200 are shown.

• Bool.instTransOrd 📋 Init.Data.Order.Ord
  : Std.TransOrd Bool
• Int.instTransOrd 📋 Init.Data.Order.Ord
  : Std.TransOrd ℤ
• Nat.instTransOrd 📋 Init.Data.Order.Ord
  : Std.TransOrd ℕ
• Std.TransOrd 📋 Init.Data.Order.Ord
  (α : Type u) [Ord α] : Prop
• Fin.instTransOrd 📋 Init.Data.Order.Ord
  (n : ℕ) : Std.TransOrd (Fin n)
• Std.TransOrd.opposite 📋 Init.Data.Order.Ord
  {α : Type u} [Ord α] [Std.TransOrd α] : Std.TransOrd α
• Array.instTransOrd 📋 Init.Data.Order.Ord
  {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (Array α)
• List.instTransOrd 📋 Init.Data.Order.Ord
  {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (List α)
• Option.instTransOrd 📋 Init.Data.Order.Ord
  {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (Option α)
• Std.LawfulBEqOrd.equivBEq 📋 Init.Data.Order.Ord
  {α : Type u} [BEq α] [Ord α] [Std.LawfulBEqOrd α] [Std.TransOrd α] : EquivBEq α
• Std.instTransCmpCompareOnOfTransOrd 📋 Init.Data.Order.Ord
  {α : Type u_1} {β : Type u_2} {f : α → β} [Ord β] [Std.TransOrd β] : Std.TransCmp (compareOn f)
• Std.instTransOrdProd 📋 Init.Data.Order.Ord
  {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [Std.TransOrd α] [Std.TransOrd β] : Std.TransOrd (α × β)
• Std.TransOrd.isGE_trans 📋 Init.Data.Order.Ord
  {α : Type u} [Ord α] [Std.TransOrd α] {a b c : α} : (compare a b).isGE = true → (compare b c).isGE = true → (compare a c).isGE = true
• Std.TransOrd.isLE_trans 📋 Init.Data.Order.Ord
  {α : Type u} [Ord α] [Std.TransOrd α] {a b c : α} : (compare a b).isLE = true → (compare b c).isLE = true → (compare a c).isLE = true
• BitVec.instTransOrd 📋 Init.Data.Ord.BitVec
  {n : ℕ} : Std.TransOrd (BitVec n)
• ISize.instTransOrd 📋 Init.Data.Ord.SInt
  : Std.TransOrd ISize
• Int16.instTransOrd 📋 Init.Data.Ord.SInt
  : Std.TransOrd Int16
• Int32.instTransOrd 📋 Init.Data.Ord.SInt
  : Std.TransOrd Int32
• Int64.instTransOrd 📋 Init.Data.Ord.SInt
  : Std.TransOrd Int64
• Int8.instTransOrd 📋 Init.Data.Ord.SInt
  : Std.TransOrd Int8
• Char.instTransOrd 📋 Init.Data.Ord.String
  : Std.TransOrd Char
• String.instTransOrd 📋 Init.Data.Ord.String
  : Std.TransOrd String
• UInt16.instTransOrd 📋 Init.Data.Ord.UInt
  : Std.TransOrd UInt16
• UInt32.instTransOrd 📋 Init.Data.Ord.UInt
  : Std.TransOrd UInt32
• UInt64.instTransOrd 📋 Init.Data.Ord.UInt
  : Std.TransOrd UInt64
• UInt8.instTransOrd 📋 Init.Data.Ord.UInt
  : Std.TransOrd UInt8
• USize.instTransOrd 📋 Init.Data.Ord.UInt
  : Std.TransOrd USize
• Vector.instTransOrd 📋 Init.Data.Ord.Vector
  {α : Type u_1} [Ord α] [Std.TransOrd α] {n : ℕ} : Std.TransOrd (Vector α n)
• Std.instTransOrdOfLawfulOrderOrdOfIsPreorder 📋 Init.Data.Order.LemmasExtra
  {α : Type u} [Ord α] [LE α] [Std.LawfulOrderOrd α] [Std.IsPreorder α] : Std.TransOrd α
• Std.IsLinearPreorder.of_ord 📋 Init.Data.Order.LemmasExtra
  {α : Type u} [LE α] [Ord α] [Std.LawfulOrderOrd α] [Std.TransOrd α] : Std.IsLinearPreorder α
• Std.IsLinearOrder.of_ord 📋 Init.Data.Order.LemmasExtra
  {α : Type u} [LE α] [Ord α] [Std.LawfulOrderOrd α] [Std.TransOrd α] [Std.LawfulEqOrd α] : Std.IsLinearOrder α
• Std.Packages.LinearPreorderOfOrdArgs.transOrd 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α) : Std.TransOrd α
• Std.Packages.LinearPreorderOfOrdArgs.lawfulOrderOrd 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α) : let this := self.ord; let this_1 := ⋯; let this_2 := self.le; Std.LawfulOrderOrd α
• Std.Packages.LinearPreorderOfOrdArgs.decidableLE 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α) : let this := self.ord; let this := self.le; have this_1 := ⋯; DecidableLE α
• Std.Packages.LinearPreorderOfOrdArgs.lt_iff 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α) : let this := self.ord; let this_1 := self.le; have this_2 := ⋯; let this_3 := self.lt; ∀ (a b : α), a < b ↔ compare a b = Ordering.lt
• Std.Packages.LinearPreorderOfOrdArgs.beq_iff 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α) : let this := self.ord; let this_1 := self.le; have this_2 := ⋯; let this_3 := self.beq; ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq
• Std.Packages.LinearOrderOfOrdArgs.max_eq 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearOrderOfOrdArgs α) : let this := self.ord; let this_1 := self.le; let this_2 := self.max; have this_3 := ⋯; ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b
• Std.Packages.LinearOrderOfOrdArgs.min_eq 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearOrderOfOrdArgs α) : let this := self.ord; let this_1 := self.le; let this_2 := self.min; have this_3 := ⋯; ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b
• Std.Packages.LinearPreorderOfOrdArgs.decidableLT 📋 Init.Data.Order.PackageFactories
  {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α) : let this := self.ord; let this := self.lt; let this_1 := self.le; have this_2 := ⋯; have this_3 := ⋯; DecidableLT α
• Std.Packages.LinearOrderOfOrdArgs.mk 📋 Init.Data.Order.PackageFactories
  {α : Type u} (toLinearPreorderOfOrdArgs : Std.Packages.LinearPreorderOfOrdArgs α) (eq_of_compare : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; ∀ (a b : α), compare a b = Ordering.eq → a = b := by extract_lets first | exact fun _ _ => _root_.Std.LawfulEqOrd.eq_of_compare | fail "Failed to derive a `LawfulEqOrd` instance. \ Please make sure that it can be synthesized or \ manually provide the field `eq_of_compare`.") (min : let this := toLinearPreorderOfOrdArgs.ord; Min α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMinOfOrd) (max : let this := toLinearPreorderOfOrdArgs.ord; Max α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMaxOfOrd) (min_eq : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; let this_2 := min; have this_3 := ⋯; ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.min_eq_if_isLE_compare (a := a) (b := b) | fail "Failed to automatically prove that `min` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \ manually provide the field `min_eq`.") (max_eq : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; let this_2 := max; have this_3 := ⋯; ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.max_eq_if_isGE_compare (a := a) (b := b) | fail "Failed to automatically prove that `max` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \ manually provide the field `max_eq`.") : Std.Packages.LinearOrderOfOrdArgs α
• Std.Packages.LinearPreorderOfOrdArgs.mk 📋 Init.Data.Order.PackageFactories
  {α : Type u} (ord : Ord α := by infer_instance) (transOrd : Std.TransOrd α := by infer_instance) (le : let this := ord; LE α := by extract_lets first | infer_instance | exact _root_.LE.ofOrd _) (lawfulOrderOrd : let this := ord; let this_1 := transOrd; let this_2 := le; Std.LawfulOrderOrd α := by extract_lets first | infer_instance | fail "Failed to automatically derive a `LawfulOrderOrd` instance. \ Please ensure that the instance can be synthesized or \ manually provide the field `lawfulOrderOrd`.") (decidableLE : let this := ord; let this := le; have this_1 := lawfulOrderOrd; DecidableLE α := by extract_lets first | infer_instance | exact _root_.DecidableLE.ofOrd _ | fail "Failed to automatically derive that `LE` is decidable.\ Please ensure that a `DecidableLE` instance can be synthesized or \ manually provide the field `decidableLE`.") (lt : let this := ord; LT α := by extract_lets first | infer_instance | exact LT.ofOrd _) (lt_iff : let this := ord; let this_1 := le; have this_2 := lawfulOrderOrd; let this_3 := lt; ∀ (a b : α), a < b ↔ compare a b = Ordering.lt := by extract_lets first | exact fun _ _ => _root_.Std.compare_eq_lt.symm | fail "Failed to automatically derive that `LT` and `Ord` are compatible. \ Please ensure that a `LawfulOrderLT` instance can be synthesized or \ manually provide the field `lt_iff`.") (decidableLT : let this := ord; let this := lt; let this_1 := le; have this_2 := lawfulOrderOrd; have this_3 := lt_iff; DecidableLT α := by extract_lets first | infer_instance | exact _root_DecidableLT.ofOrd _ | fail "Failed to automatically derive that `LT` is decidable. \ Please ensure that a `DecidableLT` instance can be synthesized or \ manually provide the field `decidableLT`.") (beq : let this := ord; BEq α := by extract_lets first | infer_instance | exact _root_.BEq.ofOrd _) (beq_iff : let this := ord; let this_1 := le; have this_2 := lawfulOrderOrd; let this_3 := beq; ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq := by extract_lets first | exact fun _ _ => Std.compare_eq_eq.symm | fail "Failed to automatically derive that `BEq` and `Ord` are compatible. \ Please ensure that a `LawfulOrderBEq` instance can be synthesized or \ manually provide the field `beq_iff`.") : Std.Packages.LinearPreorderOfOrdArgs α
• Std.Packages.LinearOrderOfOrdArgs.mk.sizeOf_spec 📋 Init.Data.Order.PackageFactories
  {α : Type u} [SizeOf α] (toLinearPreorderOfOrdArgs : Std.Packages.LinearPreorderOfOrdArgs α) (eq_of_compare : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; ∀ (a b : α), compare a b = Ordering.eq → a = b := by extract_lets first | exact fun _ _ => _root_.Std.LawfulEqOrd.eq_of_compare | fail "Failed to derive a `LawfulEqOrd` instance. \ Please make sure that it can be synthesized or \ manually provide the field `eq_of_compare`.") (min : let this := toLinearPreorderOfOrdArgs.ord; Min α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMinOfOrd) (max : let this := toLinearPreorderOfOrdArgs.ord; Max α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMaxOfOrd) (min_eq : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; let this_2 := min; have this_3 := ⋯; ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.min_eq_if_isLE_compare (a := a) (b := b) | fail "Failed to automatically prove that `min` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \ manually provide the field `min_eq`.") (max_eq : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; let this_2 := max; have this_3 := ⋯; ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.max_eq_if_isGE_compare (a := a) (b := b) | fail "Failed to automatically prove that `max` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \ manually provide the field `max_eq`.") : sizeOf { toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs, eq_of_compare := eq_of_compare, min := min, max := max, min_eq := min_eq, max_eq := max_eq } = 1 + sizeOf toLinearPreorderOfOrdArgs + sizeOf min + sizeOf max
• Std.Packages.LinearPreorderOfOrdArgs.mk.sizeOf_spec 📋 Init.Data.Order.PackageFactories
  {α : Type u} [SizeOf α] (ord : Ord α := by infer_instance) (transOrd : Std.TransOrd α := by infer_instance) (le : let this := ord; LE α := by extract_lets first | infer_instance | exact _root_.LE.ofOrd _) (lawfulOrderOrd : let this := ord; let this_1 := transOrd; let this_2 := le; Std.LawfulOrderOrd α := by extract_lets first | infer_instance | fail "Failed to automatically derive a `LawfulOrderOrd` instance. \ Please ensure that the instance can be synthesized or \ manually provide the field `lawfulOrderOrd`.") (decidableLE : let this := ord; let this := le; have this_1 := lawfulOrderOrd; DecidableLE α := by extract_lets first | infer_instance | exact _root_.DecidableLE.ofOrd _ | fail "Failed to automatically derive that `LE` is decidable.\ Please ensure that a `DecidableLE` instance can be synthesized or \ manually provide the field `decidableLE`.") (lt : let this := ord; LT α := by extract_lets first | infer_instance | exact LT.ofOrd _) (lt_iff : let this := ord; let this_1 := le; have this_2 := lawfulOrderOrd; let this_3 := lt; ∀ (a b : α), a < b ↔ compare a b = Ordering.lt := by extract_lets first | exact fun _ _ => _root_.Std.compare_eq_lt.symm | fail "Failed to automatically derive that `LT` and `Ord` are compatible. \ Please ensure that a `LawfulOrderLT` instance can be synthesized or \ manually provide the field `lt_iff`.") (decidableLT : let this := ord; let this := lt; let this_1 := le; have this_2 := lawfulOrderOrd; have this_3 := lt_iff; DecidableLT α := by extract_lets first | infer_instance | exact _root_DecidableLT.ofOrd _ | fail "Failed to automatically derive that `LT` is decidable. \ Please ensure that a `DecidableLT` instance can be synthesized or \ manually provide the field `decidableLT`.") (beq : let this := ord; BEq α := by extract_lets first | infer_instance | exact _root_.BEq.ofOrd _) (beq_iff : let this := ord; let this_1 := le; have this_2 := lawfulOrderOrd; let this_3 := beq; ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq := by extract_lets first | exact fun _ _ => Std.compare_eq_eq.symm | fail "Failed to automatically derive that `BEq` and `Ord` are compatible. \ Please ensure that a `LawfulOrderBEq` instance can be synthesized or \ manually provide the field `beq_iff`.") : sizeOf { ord := ord, transOrd := transOrd, le := le, lawfulOrderOrd := lawfulOrderOrd, decidableLE := decidableLE, lt := lt, lt_iff := lt_iff, decidableLT := decidableLT, beq := beq, beq_iff := beq_iff } = 1 + sizeOf ord + sizeOf transOrd + sizeOf le + sizeOf lawfulOrderOrd + sizeOf lt + sizeOf beq
• Std.Packages.LinearOrderOfOrdArgs.mk.injEq 📋 Init.Data.Order.PackageFactories
  {α : Type u} (toLinearPreorderOfOrdArgs : Std.Packages.LinearPreorderOfOrdArgs α) (eq_of_compare : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; ∀ (a b : α), compare a b = Ordering.eq → a = b := by extract_lets first | exact fun _ _ => _root_.Std.LawfulEqOrd.eq_of_compare | fail "Failed to derive a `LawfulEqOrd` instance. \ Please make sure that it can be synthesized or \ manually provide the field `eq_of_compare`.") (min : let this := toLinearPreorderOfOrdArgs.ord; Min α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMinOfOrd) (max : let this := toLinearPreorderOfOrdArgs.ord; Max α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMaxOfOrd) (min_eq : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; let this_2 := min; have this_3 := ⋯; ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.min_eq_if_isLE_compare (a := a) (b := b) | fail "Failed to automatically prove that `min` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \ manually provide the field `min_eq`.") (max_eq : let this := toLinearPreorderOfOrdArgs.ord; let this_1 := toLinearPreorderOfOrdArgs.le; let this_2 := max; have this_3 := ⋯; ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.max_eq_if_isGE_compare (a := a) (b := b) | fail "Failed to automatically prove that `max` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \ manually provide the field `max_eq`.") (toLinearPreorderOfOrdArgs✝ : Std.Packages.LinearPreorderOfOrdArgs α) (eq_of_compare✝ : let this := toLinearPreorderOfOrdArgs✝.ord; let this_1 := toLinearPreorderOfOrdArgs✝.le; ∀ (a b : α), compare a b = Ordering.eq → a = b := by extract_lets first | exact fun _ _ => _root_.Std.LawfulEqOrd.eq_of_compare | fail "Failed to derive a `LawfulEqOrd` instance. \ Please make sure that it can be synthesized or \ manually provide the field `eq_of_compare`.") (min✝ : let this := toLinearPreorderOfOrdArgs✝.ord; Min α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMinOfOrd) (max✝ : let this := toLinearPreorderOfOrdArgs✝.ord; Max α := by extract_lets first | infer_instance | exact _root_.Std.FactoryInstances.instMaxOfOrd) (min_eq✝ : let this := toLinearPreorderOfOrdArgs✝.ord; let this_1 := toLinearPreorderOfOrdArgs✝.le; let this_2 := min✝; have this_3 := ⋯; ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.min_eq_if_isLE_compare (a := a) (b := b) | fail "Failed to automatically prove that `min` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \ manually provide the field `min_eq`.") (max_eq✝ : let this := toLinearPreorderOfOrdArgs✝.ord; let this_1 := toLinearPreorderOfOrdArgs✝.le; let this_2 := max✝; have this_3 := ⋯; ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b := by extract_lets first | exact fun a b => _root_.Std.max_eq_if_isGE_compare (a := a) (b := b) | fail "Failed to automatically prove that `max` is left-leaning. \ Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \ manually provide the field `max_eq`.") : ({ toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs, eq_of_compare := eq_of_compare, min := min, max := max, min_eq := min_eq, max_eq := max_eq } = { toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs✝, eq_of_compare := eq_of_compare✝, min := min✝, max := max✝, min_eq := min_eq✝, max_eq := max_eq✝ }) = (toLinearPreorderOfOrdArgs = toLinearPreorderOfOrdArgs✝ ∧ min = min✝ ∧ max = max✝)
• Std.Packages.LinearPreorderOfOrdArgs.mk.injEq 📋 Init.Data.Order.PackageFactories
  {α : Type u} (ord : Ord α := by infer_instance) (transOrd : Std.TransOrd α := by infer_instance) (le : let this := ord; LE α := by extract_lets first | infer_instance | exact _root_.LE.ofOrd _) (lawfulOrderOrd : let this := ord; let this_1 := transOrd; let this_2 := le; Std.LawfulOrderOrd α := by extract_lets first | infer_instance | fail "Failed to automatically derive a `LawfulOrderOrd` instance. \ Please ensure that the instance can be synthesized or \ manually provide the field `lawfulOrderOrd`.") (decidableLE : let this := ord; let this := le; have this_1 := lawfulOrderOrd; DecidableLE α := by extract_lets first | infer_instance | exact _root_.DecidableLE.ofOrd _ | fail "Failed to automatically derive that `LE` is decidable.\ Please ensure that a `DecidableLE` instance can be synthesized or \ manually provide the field `decidableLE`.") (lt : let this := ord; LT α := by extract_lets first | infer_instance | exact LT.ofOrd _) (lt_iff : let this := ord; let this_1 := le; have this_2 := lawfulOrderOrd; let this_3 := lt; ∀ (a b : α), a < b ↔ compare a b = Ordering.lt := by extract_lets first | exact fun _ _ => _root_.Std.compare_eq_lt.symm | fail "Failed to automatically derive that `LT` and `Ord` are compatible. \ Please ensure that a `LawfulOrderLT` instance can be synthesized or \ manually provide the field `lt_iff`.") (decidableLT : let this := ord; let this := lt; let this_1 := le; have this_2 := lawfulOrderOrd; have this_3 := lt_iff; DecidableLT α := by extract_lets first | infer_instance | exact _root_DecidableLT.ofOrd _ | fail "Failed to automatically derive that `LT` is decidable. \ Please ensure that a `DecidableLT` instance can be synthesized or \ manually provide the field `decidableLT`.") (beq : let this := ord; BEq α := by extract_lets first | infer_instance | exact _root_.BEq.ofOrd _) (beq_iff : let this := ord; let this_1 := le; have this_2 := lawfulOrderOrd; let this_3 := beq; ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq := by extract_lets first | exact fun _ _ => Std.compare_eq_eq.symm | fail "Failed to automatically derive that `BEq` and `Ord` are compatible. \ Please ensure that a `LawfulOrderBEq` instance can be synthesized or \ manually provide the field `beq_iff`.") (ord✝ : Ord α := by infer_instance) (transOrd✝ : Std.TransOrd α := by infer_instance) (le✝ : let this := ord✝; LE α := by extract_lets first | infer_instance | exact _root_.LE.ofOrd _) (lawfulOrderOrd✝ : let this := ord✝; let this_1 := transOrd✝; let this_2 := le✝; Std.LawfulOrderOrd α := by extract_lets first | infer_instance | fail "Failed to automatically derive a `LawfulOrderOrd` instance. \ Please ensure that the instance can be synthesized or \ manually provide the field `lawfulOrderOrd`.") (decidableLE✝ : let this := ord✝; let this := le✝; have this_1 := lawfulOrderOrd✝; DecidableLE α := by extract_lets first | infer_instance | exact _root_.DecidableLE.ofOrd _ | fail "Failed to automatically derive that `LE` is decidable.\ Please ensure that a `DecidableLE` instance can be synthesized or \ manually provide the field `decidableLE`.") (lt✝ : let this := ord✝; LT α := by extract_lets first | infer_instance | exact LT.ofOrd _) (lt_iff✝ : let this := ord✝; let this_1 := le✝; have this_2 := lawfulOrderOrd✝; let this_3 := lt✝; ∀ (a b : α), a < b ↔ compare a b = Ordering.lt := by extract_lets first | exact fun _ _ => _root_.Std.compare_eq_lt.symm | fail "Failed to automatically derive that `LT` and `Ord` are compatible. \ Please ensure that a `LawfulOrderLT` instance can be synthesized or \ manually provide the field `lt_iff`.") (decidableLT✝ : let this := ord✝; let this := lt✝; let this_1 := le✝; have this_2 := lawfulOrderOrd✝; have this_3 := lt_iff✝; DecidableLT α := by extract_lets first | infer_instance | exact _root_DecidableLT.ofOrd _ | fail "Failed to automatically derive that `LT` is decidable. \ Please ensure that a `DecidableLT` instance can be synthesized or \ manually provide the field `decidableLT`.") (beq✝ : let this := ord✝; BEq α := by extract_lets first | infer_instance | exact _root_.BEq.ofOrd _) (beq_iff✝ : let this := ord✝; let this_1 := le✝; have this_2 := lawfulOrderOrd✝; let this_3 := beq✝; ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq := by extract_lets first | exact fun _ _ => Std.compare_eq_eq.symm | fail "Failed to automatically derive that `BEq` and `Ord` are compatible. \ Please ensure that a `LawfulOrderBEq` instance can be synthesized or \ manually provide the field `beq_iff`.") : ({ ord := ord, transOrd := transOrd, le := le, lawfulOrderOrd := lawfulOrderOrd, decidableLE := decidableLE, lt := lt, lt_iff := lt_iff, decidableLT := decidableLT, beq := beq, beq_iff := beq_iff } = { ord := ord✝, transOrd := transOrd✝, le := le✝, lawfulOrderOrd := lawfulOrderOrd✝, decidableLE := decidableLE✝, lt := lt✝, lt_iff := lt_iff✝, decidableLT := decidableLT✝, beq := beq✝, beq_iff := beq_iff✝ }) = (ord = ord✝ ∧ le = le✝ ∧ decidableLE ≍ decidableLE✝ ∧ lt = lt✝ ∧ decidableLT ≍ decidableLT✝ ∧ beq = beq✝)
• Std.Internal.List.maxKey?_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] {l : List ((a : α) × β a)} (he : l.isEmpty = true) : Std.Internal.List.maxKey? l = none
• Std.Internal.List.minKey?_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] {l : List ((a : α) × β a)} (he : l.isEmpty = true) : Std.Internal.List.minKey? l = none
• Std.Internal.List.maxKeyD_eq_getD_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} : Std.Internal.List.maxKeyD l fallback = (Std.Internal.List.maxKey? l).getD fallback
• Std.Internal.List.minKeyD_eq_getD_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} : Std.Internal.List.minKeyD l fallback = (Std.Internal.List.minKey? l).getD fallback
• Std.Internal.List.maxKey!_eq_get!_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} : Std.Internal.List.maxKey! l = (Std.Internal.List.maxKey? l).get!
• Std.Internal.List.maxKey!_eq_maxKeyD_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} : Std.Internal.List.maxKey! l = Std.Internal.List.maxKeyD l default
• Std.Internal.List.minKey!_eq_get!_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} : Std.Internal.List.minKey! l = (Std.Internal.List.minKey? l).get!
• Std.Internal.List.minKey!_eq_minKeyD_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} : Std.Internal.List.minKey! l = Std.Internal.List.minKeyD l default
• Std.Internal.List.isSome_maxKey?_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hc : Std.Internal.List.containsKey k l = true) : (Std.Internal.List.maxKey? l).isSome = true
• Std.Internal.List.isSome_minKey?_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hc : Std.Internal.List.containsKey k l = true) : (Std.Internal.List.minKey? l).isSome = true
• Std.Internal.List.maxKeyD_eq_fallback 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (h : l.isEmpty = true) : Std.Internal.List.maxKeyD l fallback = fallback
• Std.Internal.List.minKeyD_eq_fallback 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (h : l.isEmpty = true) : Std.Internal.List.minKeyD l fallback = fallback
• Std.Internal.List.maxKey!_eq_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (h : l.isEmpty = true) : Std.Internal.List.maxKey! l = default
• Std.Internal.List.minKey!_eq_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (h : l.isEmpty = true) : Std.Internal.List.minKey! l = default
• Std.Internal.List.isSome_maxKey?_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : (Std.Internal.List.maxKey? (Std.Internal.List.insertEntry k v l)).isSome = true
• Std.Internal.List.isSome_maxKey?_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : (Std.Internal.List.maxKey? (Std.Internal.List.insertEntryIfNew k v l)).isSome = true
• Std.Internal.List.isSome_minEntry?_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hc : Std.Internal.List.containsKey k l = true) : (Std.Internal.List.minEntry? l).isSome = true
• Std.Internal.List.isSome_minKey?_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) : (Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l)).isSome = true
• Std.Internal.List.isSome_minKey?_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) : (Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l)).isSome = true
• Std.Internal.List.min?_keys 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [Std.LawfulEqOrd α] [LE α] [Std.LawfulOrderOrd α] [Min α] [Std.LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)) : (Std.Internal.List.keys l).min? = Std.Internal.List.minKey? l
• Std.Internal.List.Const.isSome_maxKey?_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} : (Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = !l.isEmpty
• Std.Internal.List.Const.isSome_minKey?_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} : (Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = !l.isEmpty
• Std.Internal.List.maxKey_eq_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} {fallback : α} : Std.Internal.List.maxKey l he = Std.Internal.List.maxKeyD l fallback
• Std.Internal.List.minKey_eq_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} {fallback : α} : Std.Internal.List.minKey l he = Std.Internal.List.minKeyD l fallback
• Std.Internal.List.Const.isSome_maxKey?_modifyKey_eq_isSome 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} : (Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = (Std.Internal.List.maxKey? l).isSome
• Std.Internal.List.Const.isSome_minKey?_modifyKey_eq_isSome 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} : (Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = (Std.Internal.List.minKey? l).isSome
• Std.Internal.List.containsKey_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} (hkm : Std.Internal.List.maxKey? l = some km) : Std.Internal.List.containsKey km l = true
• Std.Internal.List.containsKey_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} (hkm : Std.Internal.List.minKey? l = some km) : Std.Internal.List.containsKey km l = true
• Std.Internal.List.isSome_maxKey?_of_isSome_maxKey?_eraseKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hs : (Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l)).isSome = true) : (Std.Internal.List.maxKey? l).isSome = true
• Std.Internal.List.isSome_minKey?_of_isSome_minKey?_eraseKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hs : (Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l)).isSome = true) : (Std.Internal.List.minKey? l).isSome = true
• Std.Internal.List.maxKey?_eq_some_maxKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} : Std.Internal.List.maxKey? l = some (Std.Internal.List.maxKey l he)
• Std.Internal.List.maxKey_eq_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} : Std.Internal.List.maxKey l he = Std.Internal.List.maxKey! l
• Std.Internal.List.minKey?_eq_some_minKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} : Std.Internal.List.minKey? l = some (Std.Internal.List.minKey l he)
• Std.Internal.List.minKey_eq_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} : Std.Internal.List.minKey l he = Std.Internal.List.minKey! l
• Std.Internal.List.maxKey?_eq_some_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (he : l.isEmpty = false) : Std.Internal.List.maxKey? l = some (Std.Internal.List.maxKeyD l fallback)
• Std.Internal.List.minKey?_eq_some_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (he : l.isEmpty = false) : Std.Internal.List.minKey? l = some (Std.Internal.List.minKeyD l fallback)
• Std.Internal.List.getKeyD_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km fallback : α} (hkm : Std.Internal.List.maxKey? l = some km) : Std.Internal.List.getKeyD km l fallback = km
• Std.Internal.List.getKeyD_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km fallback : α} (hkm : Std.Internal.List.minKey? l = some km) : Std.Internal.List.getKeyD km l fallback = km
• Std.Internal.List.isSome_minEntry?_insert 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) : (Std.Internal.List.minEntry? (Std.Internal.List.insertEntry k v l)).isSome = true
• Std.Internal.List.isSome_minEntry?_insertIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) : (Std.Internal.List.minEntry? (Std.Internal.List.insertEntryIfNew k v l)).isSome = true
• Std.Internal.List.maxKey?_bind_getKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : ((Std.Internal.List.maxKey? l).bind fun k => Std.Internal.List.getKey? k l) = Std.Internal.List.maxKey? l
• Std.Internal.List.maxKey?_eq_some_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (he : l.isEmpty = false) : Std.Internal.List.maxKey? l = some (Std.Internal.List.maxKey! l)
• Std.Internal.List.minKey?_bind_getKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : ((Std.Internal.List.minKey? l).bind fun k => Std.Internal.List.getKey? k l) = Std.Internal.List.minKey? l
• Std.Internal.List.minKey?_eq_some_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (he : l.isEmpty = false) : Std.Internal.List.minKey? l = some (Std.Internal.List.minKey! l)
• Std.Internal.List.containsKey_maxKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.containsKey (Std.Internal.List.maxKey l he) l = true
• Std.Internal.List.containsKey_minKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.containsKey (Std.Internal.List.minKey l he) l = true
• Std.Internal.List.getKey!_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [Inhabited α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} (hkm : Std.Internal.List.maxKey? l = some km) : Std.Internal.List.getKey! km l = km
• Std.Internal.List.getKey!_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [Inhabited α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} (hkm : Std.Internal.List.minKey? l = some km) : Std.Internal.List.getKey! km l = km
• Std.Internal.List.minKeyD_insertEntryIfNew_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} {fallback : α} : (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback) k).isLE = true
• Std.Internal.List.minKeyD_insertEntry_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} {fallback : α} : (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntry k v l) fallback) k).isLE = true
• Std.Internal.List.self_le_maxKeyD_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} {fallback : α} : (compare k (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntry k v l) fallback)).isLE = true
• Std.Internal.List.self_le_maxKeyD_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} {fallback : α} : (compare k (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback)).isLE = true
• Std.Internal.List.containsKey_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.containsKey (Std.Internal.List.maxKeyD l fallback) l = true
• Std.Internal.List.containsKey_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.containsKey (Std.Internal.List.minKeyD l fallback) l = true
• Std.Internal.List.le_maxKeyD_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} (hc : Std.Internal.List.containsKey k l = true) {fallback : α} : (compare k (Std.Internal.List.maxKeyD l fallback)).isLE = true
• Std.Internal.List.minKey!_insertEntryIfNew_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntryIfNew k v l)) k).isLE = true
• Std.Internal.List.minKey!_insertEntry_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntry k v l)) k).isLE = true
• Std.Internal.List.minKeyD_le_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} (hc : Std.Internal.List.containsKey k l = true) {fallback : α} : (compare (Std.Internal.List.minKeyD l fallback) k).isLE = true
• Std.Internal.List.self_le_maxKey!_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare k (Std.Internal.List.maxKey! (Std.Internal.List.insertEntry k v l))).isLE = true
• Std.Internal.List.self_le_maxKey!_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare k (Std.Internal.List.maxKey! (Std.Internal.List.insertEntryIfNew k v l))).isLE = true
• Std.Internal.List.containsKey_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) : Std.Internal.List.containsKey (Std.Internal.List.maxKey! l) l = true
• Std.Internal.List.containsKey_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) : Std.Internal.List.containsKey (Std.Internal.List.minKey! l) l = true
• Std.Internal.List.getKey?_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} (hkm : Std.Internal.List.maxKey? l = some km) : Std.Internal.List.getKey? km l = some km
• Std.Internal.List.getKey?_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} (hkm : Std.Internal.List.minKey? l = some km) : Std.Internal.List.getKey? km l = some km
• Std.Internal.List.isEmpty_eq_false_of_isEmpty_eraseKey_eq_false 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} (he : (Std.Internal.List.eraseKey k l).isEmpty = false) : l.isEmpty = false
• Std.Internal.List.le_maxKey!_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} (hc : Std.Internal.List.containsKey k l = true) : (compare k (Std.Internal.List.maxKey! l)).isLE = true
• Std.Internal.List.maxKey_eq_get_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} : Std.Internal.List.maxKey l he = (Std.Internal.List.maxKey? l).get ⋯
• Std.Internal.List.minKey!_le_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} (hc : Std.Internal.List.containsKey k l = true) : (compare (Std.Internal.List.minKey! l) k).isLE = true
• Std.Internal.List.minKey_eq_get_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} : Std.Internal.List.minKey l he = (Std.Internal.List.minKey? l).get ⋯
• Std.Internal.List.Const.maxKey?_modifyKey_eq_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.maxKey? l
• Std.Internal.List.Const.minKey?_modifyKey_eq_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.minKey? l
• Std.Internal.List.containsKey_maxKey?_eraseKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {kme : α} (hkme : Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l) = some kme) : Std.Internal.List.containsKey kme l = true
• Std.Internal.List.containsKey_minKey?_eraseKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {kme : α} (hkme : Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l) = some kme) : Std.Internal.List.containsKey kme l = true
• Std.Internal.List.maxKey?_of_perm 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (hp : l.Perm l') : Std.Internal.List.maxKey? l = Std.Internal.List.maxKey? l'
• Std.Internal.List.minKey?_of_perm 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (hp : l.Perm l') : Std.Internal.List.minKey? l = Std.Internal.List.minKey? l'
• Std.Internal.List.Const.maxKeyD_modifyKey_eq_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} {fallback : α} : Std.Internal.List.maxKeyD (Std.Internal.List.Const.modifyKey k f l) fallback = Std.Internal.List.maxKeyD l fallback
• Std.Internal.List.Const.minKeyD_modifyKey_eq_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} {fallback : α} : Std.Internal.List.minKeyD (Std.Internal.List.Const.modifyKey k f l) fallback = Std.Internal.List.minKeyD l fallback
• Std.Internal.List.maxKeyD_of_perm 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {fallback : α} (hd : Std.Internal.List.DistinctKeys l) (hp : l.Perm l') : Std.Internal.List.maxKeyD l fallback = Std.Internal.List.maxKeyD l' fallback
• Std.Internal.List.minKeyD_insertEntryIfNew_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) {fallback : α} : Std.Internal.List.minKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback = k
• Std.Internal.List.minKeyD_insertEntry_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) {fallback : α} : Std.Internal.List.minKeyD (Std.Internal.List.insertEntry k v l) fallback = k
• Std.Internal.List.minKeyD_of_perm 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {fallback : α} (hd : Std.Internal.List.DistinctKeys l) (hp : l.Perm l') : Std.Internal.List.minKeyD l fallback = Std.Internal.List.minKeyD l' fallback
• Std.Internal.List.minKey_insertEntryIfNew_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare (Std.Internal.List.minKey (Std.Internal.List.insertEntryIfNew k v l) ⋯) k).isLE = true
• Std.Internal.List.minKey_insertEntry_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare (Std.Internal.List.minKey (Std.Internal.List.insertEntry k v l) ⋯) k).isLE = true
• Std.Internal.List.self_le_maxKey_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare k (Std.Internal.List.maxKey (Std.Internal.List.insertEntry k v l) ⋯)).isLE = true
• Std.Internal.List.self_le_maxKey_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {v : β k} : (compare k (Std.Internal.List.maxKey (Std.Internal.List.insertEntryIfNew k v l) ⋯)).isLE = true
• Std.Internal.List.Const.maxKey!_modifyKey_eq_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} : Std.Internal.List.maxKey! (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.maxKey! l
• Std.Internal.List.Const.maxKeyD_modifyKey_beq 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} {fallback : α} : (Std.Internal.List.maxKeyD (Std.Internal.List.Const.modifyKey k f l) fallback == Std.Internal.List.maxKeyD l fallback) = true
• Std.Internal.List.Const.minKey!_modifyKey_eq_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} : Std.Internal.List.minKey! (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.minKey! l
• Std.Internal.List.Const.minKeyD_modifyKey_beq 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} {fallback : α} : (Std.Internal.List.minKeyD (Std.Internal.List.Const.modifyKey k f l) fallback == Std.Internal.List.minKeyD l fallback) = true
• Std.Internal.List.isEmpty_eq_isEmpty_eraseKey_and_not_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (k : α) : l.isEmpty = ((Std.Internal.List.eraseKey k l).isEmpty && !Std.Internal.List.containsKey k l)
• Std.Internal.List.maxKey!_of_perm 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l l' : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (hp : l.Perm l') : Std.Internal.List.maxKey! l = Std.Internal.List.maxKey! l'
• Std.Internal.List.minKey!_insertEntryIfNew_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) : Std.Internal.List.minKey! (Std.Internal.List.insertEntryIfNew k v l) = k
• Std.Internal.List.minKey!_insertEntry_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) : Std.Internal.List.minKey! (Std.Internal.List.insertEntry k v l) = k
• Std.Internal.List.minKey!_of_perm 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l l' : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (hp : l.Perm l') : Std.Internal.List.minKey! l = Std.Internal.List.minKey! l'
• Std.Internal.List.minKey?_insertEntryIfNew_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) : Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l) = some k
• Std.Internal.List.minKey?_insertEntry_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) : Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l) = some k
• Std.Internal.List.Const.maxKey!_modifyKey_beq 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} : (Std.Internal.List.maxKey! (Std.Internal.List.Const.modifyKey k f l) == Std.Internal.List.maxKey! l) = true
• Std.Internal.List.Const.minKey!_modifyKey_beq 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β → β} : (Std.Internal.List.minKey! (Std.Internal.List.Const.modifyKey k f l) == Std.Internal.List.minKey! l) = true
• Std.Internal.List.getKeyD_maxKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} {fallback : α} : Std.Internal.List.getKeyD (Std.Internal.List.maxKey l he) l fallback = Std.Internal.List.maxKey l he
• Std.Internal.List.getKeyD_minKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} {fallback : α} : Std.Internal.List.getKeyD (Std.Internal.List.minKey l he) l fallback = Std.Internal.List.minKey l he
• Std.Internal.List.minEntry?_of_perm 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (hp : l.Perm l') : Std.Internal.List.minEntry? l = Std.Internal.List.minEntry? l'
• Std.Internal.List.minKey?_bind_getEntry? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : ((Std.Internal.List.minKey? l).bind fun k => Std.Internal.List.getEntry? k l) = Std.Internal.List.minEntry? l
• Std.Internal.List.getKey!_maxKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.getKey! (Std.Internal.List.maxKey l he) l = Std.Internal.List.maxKey l he
• Std.Internal.List.getKey!_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) : Std.Internal.List.getKey! (Std.Internal.List.maxKey! l) l = Std.Internal.List.maxKey! l
• Std.Internal.List.getKey!_minKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.getKey! (Std.Internal.List.minKey l he) l = Std.Internal.List.minKey l he
• Std.Internal.List.getKey!_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) : Std.Internal.List.getKey! (Std.Internal.List.minKey! l) l = Std.Internal.List.minKey! l
• Std.Internal.List.getKey?_maxKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.getKey? (Std.Internal.List.maxKey l he) l = some (Std.Internal.List.maxKey l he)
• Std.Internal.List.getKey?_minKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.getKey? (Std.Internal.List.minKey l he) l = some (Std.Internal.List.minKey l he)
• Std.Internal.List.getKeyD_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback fallback' : α} : Std.Internal.List.getKeyD (Std.Internal.List.maxKeyD l fallback) l fallback' = Std.Internal.List.maxKeyD l fallback
• Std.Internal.List.getKeyD_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback fallback' : α} : Std.Internal.List.getKeyD (Std.Internal.List.minKeyD l fallback) l fallback' = Std.Internal.List.minKeyD l fallback
• Std.Internal.List.getKey!_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.getKey! (Std.Internal.List.maxKeyD l fallback) l = Std.Internal.List.maxKeyD l fallback
• Std.Internal.List.getKey!_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.getKey! (Std.Internal.List.minKeyD l fallback) l = Std.Internal.List.minKeyD l fallback
• Std.Internal.List.getKey?_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.getKey? (Std.Internal.List.maxKeyD l fallback) l = some (Std.Internal.List.maxKeyD l fallback)
• Std.Internal.List.getKey?_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.getKey? (Std.Internal.List.minKeyD l fallback) l = some (Std.Internal.List.minKeyD l fallback)
• Std.Internal.List.getKeyD_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.getKeyD (Std.Internal.List.maxKey! l) l fallback = Std.Internal.List.maxKey! l
• Std.Internal.List.getKeyD_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {fallback : α} : Std.Internal.List.getKeyD (Std.Internal.List.minKey! l) l fallback = Std.Internal.List.minKey! l
• Std.Internal.List.maxKey?_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.maxKey? (Std.Internal.List.modifyKey k f l) = Std.Internal.List.maxKey? l
• Std.Internal.List.minKey?_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.minKey? (Std.Internal.List.modifyKey k f l) = Std.Internal.List.minKey? l
• Std.Internal.List.getKey?_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) : Std.Internal.List.getKey? (Std.Internal.List.maxKey! l) l = some (Std.Internal.List.maxKey! l)
• Std.Internal.List.getKey?_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) : Std.Internal.List.getKey? (Std.Internal.List.minKey! l) l = some (Std.Internal.List.minKey! l)
• Std.Internal.List.minKey_insertEntryIfNew_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) : Std.Internal.List.minKey (Std.Internal.List.insertEntryIfNew k v l) ⋯ = k
• Std.Internal.List.minKey_insertEntry_of_isEmpty 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = true) : Std.Internal.List.minKey (Std.Internal.List.insertEntry k v l) ⋯ = k
• Std.Internal.List.getKey_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {fallback : α} {he : Std.Internal.List.containsKey (Std.Internal.List.maxKeyD l fallback) l = true} : Std.Internal.List.getKey (Std.Internal.List.maxKeyD l fallback) l he = Std.Internal.List.maxKeyD l fallback
• Std.Internal.List.getKey_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {fallback : α} {he : Std.Internal.List.containsKey (Std.Internal.List.minKeyD l fallback) l = true} : Std.Internal.List.getKey (Std.Internal.List.minKeyD l fallback) l he = Std.Internal.List.minKeyD l fallback
• Std.Internal.List.maxKeyD_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β k → β k} {fallback : α} : Std.Internal.List.maxKeyD (Std.Internal.List.modifyKey k f l) fallback = Std.Internal.List.maxKeyD l fallback
• Std.Internal.List.minKeyD_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β k → β k} {fallback : α} : Std.Internal.List.minKeyD (Std.Internal.List.modifyKey k f l) fallback = Std.Internal.List.minKeyD l fallback
• Std.Internal.List.getKey_maxKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : Std.Internal.List.containsKey (Std.Internal.List.maxKey! l) l = true} : Std.Internal.List.getKey (Std.Internal.List.maxKey! l) l he = Std.Internal.List.maxKey! l
• Std.Internal.List.getKey_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : Std.Internal.List.containsKey (Std.Internal.List.minKey! l) l = true} : Std.Internal.List.getKey (Std.Internal.List.minKey! l) l he = Std.Internal.List.minKey! l
• Std.Internal.List.maxKey!_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β k → β k} : Std.Internal.List.maxKey! (Std.Internal.List.modifyKey k f l) = Std.Internal.List.maxKey! l
• Std.Internal.List.minKey!_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} {f : β k → β k} : Std.Internal.List.minKey! (Std.Internal.List.modifyKey k f l) = Std.Internal.List.minKey! l
• Std.Internal.List.getKey_maxKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.getKey (Std.Internal.List.maxKey l he) l ⋯ = Std.Internal.List.maxKey l he
• Std.Internal.List.getKey_minKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false} : Std.Internal.List.getKey (Std.Internal.List.minKey l he) l ⋯ = Std.Internal.List.minKey l he
• Std.Internal.List.maxKey?_eraseKey_eq_of_beq_maxKey?_eq_false 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (hc : ∀ {km : α}, Std.Internal.List.maxKey? l = some km → (k == km) = false) : Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey? l
• Std.Internal.List.maxKeyD_le_maxKeyD_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} : (compare (Std.Internal.List.maxKeyD l fallback) (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntry k v l) fallback)).isLE = true
• Std.Internal.List.maxKeyD_le_maxKeyD_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} : (compare (Std.Internal.List.maxKeyD l fallback) (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback)).isLE = true
• Std.Internal.List.minKey?_eraseKey_eq_of_beq_minKey?_eq_false 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (hc : ∀ {km : α}, Std.Internal.List.minKey? l = some km → (k == km) = false) : Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey? l
• Std.Internal.List.minKeyD_insertEntryIfNew_le_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} : (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback) (Std.Internal.List.minKeyD l fallback)).isLE = true
• Std.Internal.List.minKeyD_insertEntry_le_minKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} : (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntry k v l) fallback) (Std.Internal.List.minKeyD l fallback)).isLE = true
• Std.Internal.List.getKey_maxKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} {hc : Std.Internal.List.containsKey km l = true} (hkm : (Std.Internal.List.maxKey? l).get ⋯ = km) : Std.Internal.List.getKey km l hc = km
• Std.Internal.List.getKey_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km : α} {hc : Std.Internal.List.containsKey km l = true} (hkm : (Std.Internal.List.minKey? l).get ⋯ = km) : Std.Internal.List.getKey km l hc = km
• Std.Internal.List.maxKey!_le_maxKey!_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} : (compare (Std.Internal.List.maxKey! l) (Std.Internal.List.maxKey! (Std.Internal.List.insertEntry k v l))).isLE = true
• Std.Internal.List.maxKey!_le_maxKey!_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} : (compare (Std.Internal.List.maxKey! l) (Std.Internal.List.maxKey! (Std.Internal.List.insertEntryIfNew k v l))).isLE = true
• Std.Internal.List.maxKey?_eraseKey_eq_iff_beq_maxKey?_eq_false 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey? l ↔ ∀ {km : α}, Std.Internal.List.maxKey? l = some km → (k == km) = false
• Std.Internal.List.maxKey?_le_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k km : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (hc : Std.Internal.List.containsKey k l = true) (hkm : (Std.Internal.List.maxKey? l).get ⋯ = km) : (compare k km).isLE = true
• Std.Internal.List.minKey!_insertEntryIfNew_le_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} : (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntryIfNew k v l)) (Std.Internal.List.minKey! l)).isLE = true
• Std.Internal.List.minKey!_insertEntry_le_minKey! 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} : (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntry k v l)) (Std.Internal.List.minKey! l)).isLE = true
• Std.Internal.List.minKey?_eraseKey_eq_iff_beq_minKey?_eq_false 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey? l ↔ ∀ {km : α}, Std.Internal.List.minKey? l = some km → (k == km) = false
• Std.Internal.List.minKey?_insertEntryIfNew_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) (hkmi : (Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l)).get ⋯ = kmi) : (compare kmi k).isLE = true
• Std.Internal.List.minKey?_insertEntry_le_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) {kmi : α} (hkmi : (Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l)).get ⋯ = kmi) : (compare kmi k).isLE = true
• Std.Internal.List.minKey?_le_of_containsKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k km : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (hc : Std.Internal.List.containsKey k l = true) (hkm : (Std.Internal.List.minKey? l).get ⋯ = km) : (compare km k).isLE = true
• Std.Internal.List.self_le_maxKey?_insertEntry 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {kmi : α} (hkmi : (Std.Internal.List.maxKey? (Std.Internal.List.insertEntry k v l)).get ⋯ = kmi) : (compare k kmi).isLE = true
• Std.Internal.List.self_le_maxKey?_insertEntryIfNew 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) (hkmi : (Std.Internal.List.maxKey? (Std.Internal.List.insertEntryIfNew k v l)).get ⋯ = kmi) : (compare k kmi).isLE = true
• Std.Internal.List.maxKeyD_eraseKey_le_maxKeyD 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} (he : (Std.Internal.List.eraseKey k l).isEmpty = false) {fallback : α} : (compare (Std.Internal.List.maxKeyD (Std.Internal.List.eraseKey k l) fallback) (Std.Internal.List.maxKeyD l fallback)).isLE = true
• Std.Internal.List.minKeyD_le_minKeyD_erase 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α} (he : (Std.Internal.List.eraseKey k l).isEmpty = false) {fallback : α} : (compare (Std.Internal.List.minKeyD l fallback) (Std.Internal.List.minKeyD (Std.Internal.List.eraseKey k l) fallback)).isLE = true
• Std.Internal.List.le_minKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) : (∀ (k' : α), Std.Internal.List.minKey? l = some k' → (compare k k').isLE = true) ↔ ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 1a6e4fd