Hash set lemmas #

This module contains lemmas about Std.Data.HashSet.Raw. Most of the lemmas require EquivBEq α and LawfulHashable α for the key type α. The easiest way to obtain these instances is to provide an instance of LawfulBEq α.

source

@[simp]

theorem Std.HashSet.Raw.size_empty {α : Type u} {c : Nat} :

(empty c).size = 0

source

@[simp]

theorem Std.HashSet.Raw.size_emptyc {α : Type u} :

∅.size = 0

source

theorem Std.HashSet.Raw.isEmpty_eq_size_eq_zero {α : Type u} {m : Raw α} :

m.isEmpty = (m.size == 0)

source

@[simp]

theorem Std.HashSet.Raw.isEmpty_empty {α : Type u} [BEq α] [Hashable α] {c : Nat} :

(empty c).isEmpty = true

source

@[simp]

theorem Std.HashSet.Raw.isEmpty_emptyc {α : Type u} [BEq α] [Hashable α] :

∅.isEmpty = true

source

@[simp]

theorem Std.HashSet.Raw.isEmpty_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

(m.insert a).isEmpty = false

source

theorem Std.HashSet.Raw.mem_iff_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] {a : α} :

a ∈ m ↔ m.contains a = true

source

theorem Std.HashSet.Raw.contains_congr {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : (a == b) = true) :

m.contains a = m.contains b

source

theorem Std.HashSet.Raw.mem_congr {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : (a == b) = true) :

a ∈ m ↔ b ∈ m

source

@[simp]

theorem Std.HashSet.Raw.contains_empty {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :

(empty c).contains a = false

source

@[simp]

theorem Std.HashSet.Raw.not_mem_empty {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :

¬a ∈ empty c

source

@[simp]

theorem Std.HashSet.Raw.contains_emptyc {α : Type u} [BEq α] [Hashable α] {a : α} :

∅.contains a = false

source

@[simp]

theorem Std.HashSet.Raw.not_mem_emptyc {α : Type u} [BEq α] [Hashable α] {a : α} :

¬a ∈ ∅

source

theorem Std.HashSet.Raw.contains_of_isEmpty {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

m.isEmpty = true → m.contains a = false

source

theorem Std.HashSet.Raw.not_mem_of_isEmpty {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

m.isEmpty = true → ¬a ∈ m

source

theorem Std.HashSet.Raw.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :

m.isEmpty = false ↔ ∃ (a : α), m.contains a = true

source

theorem Std.HashSet.Raw.isEmpty_eq_false_iff_exists_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :

m.isEmpty = false ↔ ∃ (a : α), a ∈ m

source

theorem Std.HashSet.Raw.isEmpty_iff_forall_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :

m.isEmpty = true ↔ ∀ (a : α), m.contains a = false

source

theorem Std.HashSet.Raw.isEmpty_iff_forall_not_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :

m.isEmpty = true ↔ ∀ (a : α), ¬a ∈ m

source

@[simp]

theorem Std.HashSet.Raw.insert_eq_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] {a : α} :

Insert.insert a m = m.insert a

source

@[simp]

theorem Std.HashSet.Raw.singleton_eq_insert {α : Type u} [BEq α] [Hashable α] {a : α} :

{a} = ∅.insert a

source

@[simp]

theorem Std.HashSet.Raw.contains_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.insert k).contains a = (k == a || m.contains a)

source

@[simp]

theorem Std.HashSet.Raw.mem_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

a ∈ m.insert k ↔ (k == a) = true ∨ a ∈ m

source

theorem Std.HashSet.Raw.contains_of_contains_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.insert k).contains a = true → (k == a) = false → m.contains a = true

source

theorem Std.HashSet.Raw.mem_of_mem_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

a ∈ m.insert k → (k == a) = false → a ∈ m

source

theorem Std.HashSet.Raw.contains_of_contains_insert' {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.insert k).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true

This is a restatement of contains_insert that is written to exactly match the proof obligation in the statement of get_insert.

source

theorem Std.HashSet.Raw.mem_of_mem_insert' {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

a ∈ m.insert k → ¬((k == a) = true ∧ ¬k ∈ m) → a ∈ m

This is a restatement of mem_insert that is written to exactly match the proof obligation in the statement of get_insertIfNew.

source

@[simp]

theorem Std.HashSet.Raw.contains_insert_self {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.insert k).contains k = true

source

@[simp]

theorem Std.HashSet.Raw.mem_insert_self {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

k ∈ m.insert k

source

theorem Std.HashSet.Raw.size_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.insert k).size = if k ∈ m then m.size else m.size + 1

source

theorem Std.HashSet.Raw.size_le_size_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

m.size ≤ (m.insert k).size

source

theorem Std.HashSet.Raw.size_insert_le {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.insert k).size ≤ m.size + 1

source

@[simp]

theorem Std.HashSet.Raw.erase_empty {α : Type u} [BEq α] [Hashable α] {k : α} {c : Nat} :

(empty c).erase k = empty c

source

@[simp]

theorem Std.HashSet.Raw.erase_emptyc {α : Type u} [BEq α] [Hashable α] {k : α} :

∅.erase k = ∅

source

@[simp]

theorem Std.HashSet.Raw.isEmpty_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)

source

@[simp]

theorem Std.HashSet.Raw.contains_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.erase k).contains a = (!k == a && m.contains a)

source

@[simp]

theorem Std.HashSet.Raw.mem_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

source

theorem Std.HashSet.Raw.contains_of_contains_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.erase k).contains a = true → m.contains a = true

source

theorem Std.HashSet.Raw.mem_of_mem_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

a ∈ m.erase k → a ∈ m

source

theorem Std.HashSet.Raw.size_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.erase k).size = if k ∈ m then m.size - 1 else m.size

source

theorem Std.HashSet.Raw.size_erase_le {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.erase k).size ≤ m.size

source

theorem Std.HashSet.Raw.size_le_size_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

m.size ≤ (m.erase k).size + 1

source

@[simp]

theorem Std.HashSet.Raw.get?_empty {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :

(empty c).get? a = none

source

@[simp]

theorem Std.HashSet.Raw.get?_emptyc {α : Type u} [BEq α] [Hashable α] {a : α} :

∅.get? a = none

source

theorem Std.HashSet.Raw.get?_of_isEmpty {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

m.isEmpty = true → m.get? a = none

source

theorem Std.HashSet.Raw.get?_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.insert k).get? a = if (k == a) = true ∧ ¬k ∈ m then some k else m.get? a

source

theorem Std.HashSet.Raw.contains_eq_isSome_get? {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

m.contains a = (m.get? a).isSome

source

theorem Std.HashSet.Raw.get?_eq_none_of_contains_eq_false {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

m.contains a = false → m.get? a = none

source

theorem Std.HashSet.Raw.get?_eq_none {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

¬a ∈ m → m.get? a = none

source

theorem Std.HashSet.Raw.get?_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.erase k).get? a = if (k == a) = true then none else m.get? a

source

theorem Std.HashSet.Raw.get_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h₁ : a ∈ m.insert k} :

(m.insert k).get a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then k else m.get a ⋯

source

@[simp]

theorem Std.HashSet.Raw.get_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h' : a ∈ m.erase k} :

(m.erase k).get a h' = m.get a ⋯

source

theorem Std.HashSet.Raw.get?_eq_some_get {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m} :

m.get? a = some (m.get a h')

source

@[simp]

theorem Std.HashSet.Raw.get?_erase_self {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.erase k).get? k = none

source

@[simp]

theorem Std.HashSet.Raw.get!_empty {α : Type u} [BEq α] [Hashable α] [Inhabited α] {a : α} {c : Nat} :

(empty c).get! a = default

source

@[simp]

theorem Std.HashSet.Raw.get!_emptyc {α : Type u} [BEq α] [Hashable α] [Inhabited α] {a : α} :

∅.get! a = default

source

theorem Std.HashSet.Raw.get!_of_isEmpty {α : Type u} {m : Raw α} [BEq α] [Hashable α] [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

m.isEmpty = true → m.get! a = default

source

theorem Std.HashSet.Raw.get!_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.insert k).get! a = if (k == a) = true ∧ ¬k ∈ m then k else m.get! a

source

theorem Std.HashSet.Raw.get!_eq_default_of_contains_eq_false {α : Type u} {m : Raw α} [BEq α] [Hashable α] [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

m.contains a = false → m.get! a = default

source

theorem Std.HashSet.Raw.get!_eq_default {α : Type u} {m : Raw α} [BEq α] [Hashable α] [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :

¬a ∈ m → m.get! a = default

source

theorem Std.HashSet.Raw.get!_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :

(m.erase k).get! a = if (k == a) = true then default else m.get! a

source

@[simp]

theorem Std.HashSet.Raw.get!_erase_self {α : Type u} {m : Raw α} [BEq α] [Hashable α] [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

(m.erase k).get! k = default

source

theorem Std.HashSet.Raw.get?_eq_some_get!_of_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :

m.contains a = true → m.get? a = some (m.get! a)

source

theorem Std.HashSet.Raw.get?_eq_some_get! {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :

a ∈ m → m.get? a = some (m.get! a)

source

theorem Std.HashSet.Raw.get!_eq_get!_get? {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :

m.get! a = (m.get? a).get!

source

theorem Std.HashSet.Raw.get_eq_get! {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h' : a ∈ m} :

m.get a h' = m.get! a

source

@[simp]

theorem Std.HashSet.Raw.getD_empty {α : Type u} [BEq α] [Hashable α] {a fallback : α} {c : Nat} :

(empty c).getD a fallback = fallback

source

@[simp]

theorem Std.HashSet.Raw.getD_emptyc {α : Type u} [BEq α] [Hashable α] {a fallback : α} :

∅.getD a fallback = fallback

source

theorem Std.HashSet.Raw.getD_of_isEmpty {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :

m.isEmpty = true → m.getD a fallback = fallback

source

theorem Std.HashSet.Raw.getD_insert {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :

(m.insert k).getD a fallback = if (k == a) = true ∧ ¬k ∈ m then k else m.getD a fallback

source

theorem Std.HashSet.Raw.getD_eq_fallback_of_contains_eq_false {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :

m.contains a = false → m.getD a fallback = fallback

source

theorem Std.HashSet.Raw.getD_eq_fallback {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :

¬a ∈ m → m.getD a fallback = fallback

source

theorem Std.HashSet.Raw.getD_erase {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :

(m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback

source

@[simp]

theorem Std.HashSet.Raw.getD_erase_self {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :

(m.erase k).getD k fallback = fallback

source

theorem Std.HashSet.Raw.get?_eq_some_getD_of_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :

m.contains a = true → m.get? a = some (m.getD a fallback)

source

theorem Std.HashSet.Raw.get?_eq_some_getD {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :

a ∈ m → m.get? a = some (m.getD a fallback)

source

theorem Std.HashSet.Raw.getD_eq_getD_get? {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :

m.getD a fallback = (m.get? a).getD fallback

source

theorem Std.HashSet.Raw.get_eq_getD {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {h' : a ∈ m} :

m.get a h' = m.getD a fallback

source

theorem Std.HashSet.Raw.get!_eq_getD_default {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :

m.get! a = m.getD a default

source

@[simp]

theorem Std.HashSet.Raw.containsThenInsert_fst {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) {k : α} :

(m.containsThenInsert k).fst = m.contains k

source

@[simp]

theorem Std.HashSet.Raw.containsThenInsert_snd {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) {k : α} :

(m.containsThenInsert k).snd = m.insert k

source

@[simp]

theorem Std.HashSet.Raw.length_toList {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :

m.toList.length = m.size

source

@[simp]

theorem Std.HashSet.Raw.isEmpty_toList {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :

m.toList.isEmpty = m.isEmpty

source

@[simp]

theorem Std.HashSet.Raw.contains_toList {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF) :

m.toList.contains k = m.contains k

source

@[simp]

theorem Std.HashSet.Raw.mem_toList {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :

k ∈ m.toList ↔ k ∈ m

source

theorem Std.HashSet.Raw.distinct_toList {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :

List.Pairwise (fun (a b : α) => (a == b) = false) m.toList

source

@[simp]

theorem Std.HashSet.Raw.insertMany_nil {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) :

m.insertMany [] = m

source

@[simp]

theorem Std.HashSet.Raw.insertMany_list_singleton {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) {k : α} :

m.insertMany [k] = m.insert k

source

theorem Std.HashSet.Raw.insertMany_cons {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) {l : List α} {k : α} :

m.insertMany (k :: l) = (m.insert k).insertMany l

source

@[simp]

theorem Std.HashSet.Raw.contains_insertMany_list {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :

(m.insertMany l).contains k = (m.contains k || l.contains k)

source

@[simp]

theorem Std.HashSet.Raw.mem_insertMany_list {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :

k ∈ m.insertMany l ↔ k ∈ m ∨ l.contains k = true

source

theorem Std.HashSet.Raw.mem_of_mem_insertMany_list {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} (contains_eq_false : l.contains k = false) :

k ∈ m.insertMany l → k ∈ m

source

theorem Std.HashSet.Raw.get?_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) :

(m.insertMany l).get? k = none

source

theorem Std.HashSet.Raw.get?_insertMany_list_of_not_mem_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :

(m.insertMany l).get? k' = some k

source

theorem Std.HashSet.Raw.get?_insertMany_list_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) :

(m.insertMany l).get? k = m.get? k

source

theorem Std.HashSet.Raw.get_insertMany_list_of_not_mem_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) {h' : k' ∈ m.insertMany l} :

(m.insertMany l).get k' h' = k

source

theorem Std.HashSet.Raw.get_insertMany_list_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) {h₃ : k ∈ m.insertMany l} :

(m.insertMany l).get k h₃ = m.get k mem

source

theorem Std.HashSet.Raw.get!_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) :

(m.insertMany l).get! k = default

source

theorem Std.HashSet.Raw.get!_insertMany_list_of_not_mem_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :

(m.insertMany l).get! k' = k

source

theorem Std.HashSet.Raw.get!_insertMany_list_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) :

(m.insertMany l).get! k = m.get! k

source

theorem Std.HashSet.Raw.getD_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) :

(m.insertMany l).getD k fallback = fallback

source

theorem Std.HashSet.Raw.getD_insertMany_list_of_not_mem_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :

(m.insertMany l).getD k' fallback = k

source

theorem Std.HashSet.Raw.getD_insertMany_list_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α} (mem : k ∈ m) :

(m.insertMany l).getD k fallback = m.getD k fallback

source

theorem Std.HashSet.Raw.size_insertMany_list {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :

(∀ (a : α), a ∈ m → l.contains a = false) → (m.insertMany l).size = m.size + l.length

source

theorem Std.HashSet.Raw.size_le_size_insertMany_list {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} :

m.size ≤ (m.insertMany l).size

source

theorem Std.HashSet.Raw.size_insertMany_list_le {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} :

(m.insertMany l).size ≤ m.size + l.length

source

@[simp]

theorem Std.HashSet.Raw.isEmpty_insertMany_list {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} :

(m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)

source

@[simp]

theorem Std.HashSet.Raw.ofList_nil {α : Type u} [BEq α] [Hashable α] :

ofList [] = ∅

source

@[simp]

theorem Std.HashSet.Raw.ofList_singleton {α : Type u} [BEq α] [Hashable α] {k : α} :

ofList [k] = ∅.insert k

source

theorem Std.HashSet.Raw.ofList_cons {α : Type u} [BEq α] [Hashable α] {hd : α} {tl : List α} :

ofList (hd :: tl) = (∅.insert hd).insertMany tl

source

@[simp]

theorem Std.HashSet.Raw.contains_ofList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :

(ofList l).contains k = l.contains k

source

@[simp]

theorem Std.HashSet.Raw.mem_ofList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :

k ∈ ofList l ↔ l.contains k = true

source

theorem Std.HashSet.Raw.get?_ofList_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :

(ofList l).get? k = none

source

theorem Std.HashSet.Raw.get?_ofList_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :

(ofList l).get? k' = some k

source

theorem Std.HashSet.Raw.get_ofList_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) {h' : k' ∈ ofList l} :

(ofList l).get k' h' = k

source

theorem Std.HashSet.Raw.get!_ofList_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :

(ofList l).get! k = default

source

theorem Std.HashSet.Raw.get!_ofList_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :

(ofList l).get! k' = k

source

theorem Std.HashSet.Raw.getD_ofList_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) :

(ofList l).getD k fallback = fallback

source

theorem Std.HashSet.Raw.getD_ofList_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :

(ofList l).getD k' fallback = k

source

theorem Std.HashSet.Raw.size_ofList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :

(ofList l).size = l.length

source

theorem Std.HashSet.Raw.size_ofList_le {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} :

(ofList l).size ≤ l.length

source

@[simp]

theorem Std.HashSet.Raw.isEmpty_ofList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} :

(ofList l).isEmpty = l.isEmpty

Documentation

Std.Data.HashSet.RawLemmas

Hash set lemmas #