Hash set lemmas

This module contains lemmas about Std.Data.HashSet. 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 α.

@[simp]

theorem Std.HashSet.isEmpty_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {c : Nat}, (Std.HashSet.empty c).isEmpty = true

@[simp]

theorem Std.HashSet.isEmpty_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α}, ∅.isEmpty = true

@[simp]

theorem Std.HashSet.isEmpty_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, (m.insert a).isEmpty = false

theorem Std.HashSet.mem_iff_contains {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {a : α}, a ∈ m ↔ m.contains a = true

theorem Std.HashSet.contains_congr {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {a b : α}, (a == b) = true → m.contains a = m.contains b

theorem Std.HashSet.mem_congr {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)

@[simp]

theorem Std.HashSet.contains_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α} {c : Nat}, (Std.HashSet.empty c).contains a = false

@[simp]

theorem Std.HashSet.not_mem_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α} {c : Nat}, ¬a ∈ Std.HashSet.empty c

@[simp]

theorem Std.HashSet.contains_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.contains a = false

@[simp]

theorem Std.HashSet.not_mem_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α}, ¬a ∈ ∅

theorem Std.HashSet.contains_of_isEmpty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.isEmpty = true → m.contains a = false

theorem Std.HashSet.not_mem_of_isEmpty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.isEmpty = true → ¬a ∈ m

theorem Std.HashSet.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α], m.isEmpty = false ↔ ∃ (a : α), m.contains a = true

theorem Std.HashSet.isEmpty_eq_false_iff_exists_mem {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α], m.isEmpty = false ↔ ∃ (a : α), a ∈ m

theorem Std.HashSet.isEmpty_iff_forall_contains {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α], m.isEmpty = true ↔ ∀ (a : α), m.contains a = false

theorem Std.HashSet.isEmpty_iff_forall_not_mem {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α], m.isEmpty = true ↔ ∀ (a : α), ¬a ∈ m

@[simp]

theorem Std.HashSet.contains_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, (m.insert k).contains a = (k == a || m.contains a)

@[simp]

theorem Std.HashSet.mem_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, a ∈ m.insert k ↔ (k == a) = true ∨ a ∈ m

theorem Std.HashSet.contains_of_contains_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, (m.insert k).contains a = true → (k == a) = false → m.contains a = true

theorem Std.HashSet.mem_of_mem_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, a ∈ m.insert k → (k == a) = false → a ∈ m

@[simp]

theorem Std.HashSet.contains_insert_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.insert k).contains k = true

@[simp]

theorem Std.HashSet.mem_insert_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, k ∈ m.insert k

@[simp]

theorem Std.HashSet.size_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {c : Nat}, (Std.HashSet.empty c).size = 0

@[simp]

theorem Std.HashSet.size_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α}, ∅.size = 0

theorem Std.HashSet.isEmpty_eq_size_eq_zero {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α}, m.isEmpty = (m.size == 0)

theorem Std.HashSet.size_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.insert k).size = if k ∈ m then m.size else m.size + 1

theorem Std.HashSet.size_le_size_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, m.size ≤ (m.insert k).size

theorem Std.HashSet.size_insert_le {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.insert k).size ≤ m.size + 1

@[simp]

theorem Std.HashSet.erase_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α} {c : Nat}, (Std.HashSet.empty c).erase a = Std.HashSet.empty c

@[simp]

theorem Std.HashSet.erase_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.erase a = ∅

@[simp]

theorem Std.HashSet.isEmpty_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)

@[simp]

theorem Std.HashSet.contains_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)

@[simp]

theorem Std.HashSet.mem_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

theorem Std.HashSet.contains_of_contains_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, (m.erase k).contains a = true → m.contains a = true

theorem Std.HashSet.mem_of_mem_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, a ∈ m.erase k → a ∈ m

theorem Std.HashSet.size_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size

theorem Std.HashSet.size_erase_le {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.erase k).size ≤ m.size

theorem Std.HashSet.size_le_size_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, m.size ≤ (m.erase k).size + 1

@[simp]

theorem Std.HashSet.containsThenInsert_fst {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {k : α}, (m.containsThenInsert k).fst = m.contains k

@[simp]

theorem Std.HashSet.containsThenInsert_snd {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {k : α}, (m.containsThenInsert k).snd = m.insert k