# 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_emptyWithCapacity {α : Type u} {c : Nat} :
(emptyWithCapacity c).size = 0
source
@[simp]
theorem Std.HashSet.Raw.size_empty {α : Type u} :
∅.size = 0
source
@[reducible, inline, deprecated Std.HashSet.Raw.size_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.size_emptyc {α : Type u_1} :
∅.size = 0
Equations

- @Std.HashSet.Raw.size_emptyc = @Std.HashSet.Raw.size_empty

Instances For

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_emptyWithCapacity {α : Type u} [BEq α] [Hashable α] {c : Nat} :
(emptyWithCapacity c).isEmpty = true
source
@[simp]
theorem Std.HashSet.Raw.isEmpty_empty {α : Type u} [BEq α] [Hashable α] :
∅.isEmpty = true
source
@[reducible, inline, deprecated Std.HashSet.Raw.isEmpty_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.isEmpty_emptyc {α : Type u_1} [BEq α] [Hashable α] :
∅.isEmpty = true
Equations

- @Std.HashSet.Raw.isEmpty_emptyc = @Std.HashSet.Raw.isEmpty_empty

Instances For

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
@[simp]
theorem Std.HashSet.Raw.contains_iff_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] {a : α} :
m.contains a = true ↔ a ∈ m
source
@[simp]
theorem Std.HashSet.Raw.contains_eq_false_iff_not_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] {k : α} :
m.contains k = false ↔ ¬k ∈ m
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_emptyWithCapacity {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :
(emptyWithCapacity c).contains a = false
source
@[simp]
theorem Std.HashSet.Raw.not_mem_emptyWithCapacity {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :
¬a ∈ emptyWithCapacity c
source
@[simp]
theorem Std.HashSet.Raw.contains_empty {α : Type u} [BEq α] [Hashable α] {a : α} :
∅.contains a = false
source
@[reducible, inline, deprecated Std.HashSet.Raw.contains_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.contains_emptyc {α : Type u_1} [BEq α] [Hashable α] {a : α} :
∅.contains a = false
Equations

- @Std.HashSet.Raw.contains_emptyc = @Std.HashSet.Raw.contains_empty

Instances For

source
@[simp]
theorem Std.HashSet.Raw.not_mem_empty {α : Type u} [BEq α] [Hashable α] {a : α} :
¬a ∈ ∅
source
@[reducible, inline, deprecated Std.HashSet.Raw.not_mem_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.not_mem_emptyc {α : Type u_1} [BEq α] [Hashable α] {a : α} :
¬a ∈ ∅
Equations

- @Std.HashSet.Raw.not_mem_emptyc = @Std.HashSet.Raw.not_mem_empty

Instances For

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_insert`.

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_emptyWithCapacity {α : Type u} [BEq α] [Hashable α] {k : α} {c : Nat} :
(emptyWithCapacity c).erase k = emptyWithCapacity c
source
@[simp]
theorem Std.HashSet.Raw.erase_empty {α : Type u} [BEq α] [Hashable α] {k : α} :
∅.erase k = ∅
source
@[reducible, inline, deprecated Std.HashSet.Raw.erase_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.erase_emptyc {α : Type u_1} [BEq α] [Hashable α] {k : α} :
∅.erase k = ∅
Equations

- @Std.HashSet.Raw.erase_emptyc = @Std.HashSet.Raw.erase_empty

Instances For

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?_emptyWithCapacity {α : Type u} [BEq α] [Hashable α] {a : α} {c : Nat} :
(emptyWithCapacity c).get? a = none
source
@[simp]
theorem Std.HashSet.Raw.get?_empty {α : Type u} [BEq α] [Hashable α] {a : α} :
∅.get? a = none
source
@[reducible, inline, deprecated Std.HashSet.Raw.get?_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.get?_emptyc {α : Type u_1} [BEq α] [Hashable α] {a : α} :
∅.get? a = none
Equations

- @Std.HashSet.Raw.get?_emptyc = @Std.HashSet.Raw.get?_empty

Instances For

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
@[simp]
theorem Std.HashSet.Raw.isSome_get?_eq_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.get? a).isSome = m.contains a
source
theorem Std.HashSet.Raw.mem_iff_isSome_get? {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
a ∈ m ↔ (m.get? a).isSome = true
source
@[simp]
theorem Std.HashSet.Raw.isSome_get?_iff_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
(m.get? a).isSome = true ↔ a ∈ m
source
theorem Std.HashSet.Raw.get?_eq_some_iff {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} :
m.get? k = some k' ↔ ∃ (h : k ∈ m), m.get k h = k'
source
theorem Std.HashSet.Raw.mem_of_get?_eq_some {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a a' : α} :
m.get? a = some a' → a' ∈ m
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?_beq {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
Option.all (fun (x : α) => x == k) (m.get? k) = true
source
theorem Std.HashSet.Raw.get?_congr {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} (h' : (k == k') = true) :
m.get? k = m.get? k'
source
theorem Std.HashSet.Raw.get?_eq_some_of_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k = true) :
m.get? k = some k
source
theorem Std.HashSet.Raw.get?_eq_some {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
m.get? k = some k
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
theorem Std.HashSet.Raw.get_eq_get_get? {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {h' : k ∈ m} :
m.get k h' = (m.get? k).get ⋯
source
theorem Std.HashSet.Raw.get_get? {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {h' : (m.get? k).isSome = true} :
(m.get? k).get h' = m.get k ⋯
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
theorem Std.HashSet.Raw.get_beq {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} (h' : k ∈ m) :
(m.get k h' == k) = true
source
theorem Std.HashSet.Raw.get_congr {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α} (h' : (k₁ == k₂) = true) (h₁ : k₁ ∈ m) :
m.get k₁ h₁ = m.get k₂ ⋯
source
@[simp]
theorem Std.HashSet.Raw.get_eq {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k = true) :
m.get k h' = k
source
@[simp]
theorem Std.HashSet.Raw.get!_emptyWithCapacity {α : Type u} [BEq α] [Hashable α] [Inhabited α] {a : α} {c : Nat} :
(emptyWithCapacity c).get! a = default
source
@[simp]
theorem Std.HashSet.Raw.get!_empty {α : Type u} [BEq α] [Hashable α] [Inhabited α] {a : α} :
∅.get! a = default
source
@[reducible, inline, deprecated Std.HashSet.Raw.get!_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.get!_emptyc {α : Type u_1} [BEq α] [Hashable α] [Inhabited α] {a : α} :
∅.get! a = default
Equations

- @Std.HashSet.Raw.get!_emptyc = @Std.HashSet.Raw.get!_empty

Instances For

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
theorem Std.HashSet.Raw.get!_congr {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k k' : α} (h' : (k == k') = true) :
m.get! k = m.get! k'
source
theorem Std.HashSet.Raw.get!_eq_of_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : m.contains k = true) :
m.get! k = k
source
theorem Std.HashSet.Raw.get!_eq_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k ∈ m) :
m.get! k = k
source
@[simp]
theorem Std.HashSet.Raw.getD_emptyWithCapacity {α : Type u} [BEq α] [Hashable α] {a fallback : α} {c : Nat} :
(emptyWithCapacity c).getD a fallback = fallback
source
@[simp]
theorem Std.HashSet.Raw.getD_empty {α : Type u} [BEq α] [Hashable α] {a fallback : α} :
∅.getD a fallback = fallback
source
@[reducible, inline, deprecated Std.HashSet.Raw.getD_empty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.getD_emptyc {α : Type u_1} [BEq α] [Hashable α] {a fallback : α} :
∅.getD a fallback = fallback
Equations

- @Std.HashSet.Raw.getD_emptyc = @Std.HashSet.Raw.getD_empty

Instances For

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
theorem Std.HashSet.Raw.getD_congr {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' fallback : α} (h' : (k == k') = true) :
m.getD k fallback = m.getD k' fallback
source
theorem Std.HashSet.Raw.getD_eq_of_contains {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : m.contains k = true) :
m.getD k fallback = k
source
theorem Std.HashSet.Raw.getD_eq_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : k ∈ m) :
m.getD k fallback = k
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 α] (h : m.WF) {k : α} :
k ∈ m.toList ↔ k ∈ m
source
theorem Std.HashSet.Raw.mem_of_mem_toList {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [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.toArray_toList {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) :
m.toList.toArray = m.toArray
source
@[simp]
theorem Std.HashSet.Raw.toList_toArray {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) :
m.toArray.toList = m.toList
source
@[simp]
theorem Std.HashSet.Raw.size_toArray {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.size = m.size
source
@[simp]
theorem Std.HashSet.Raw.isEmpty_toArray {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.isEmpty = m.isEmpty
source
@[simp]
theorem Std.HashSet.Raw.contains_toArray {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF) :
m.toArray.contains k = m.contains k
source
@[simp]
theorem Std.HashSet.Raw.mem_toArray {α : Type u} {m : Raw α} [BEq α] [Hashable α] [LawfulBEq α] {k : α} (h : m.WF) :
k ∈ m.toArray ↔ k ∈ m
source
theorem Std.HashSet.Raw.forall_mem_toArray_iff_forall_mem_get {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {p : α → Prop} (h : m.WF) :
(∀ (k : α), k ∈ m.toArray → p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.get k h)
source
theorem Std.HashSet.Raw.contains_of_mem_toArray {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} (h' : k ∈ m.toArray) :
m.contains k = true
source
theorem Std.HashSet.Raw.foldM_eq_foldlM_toList {α : Type u} [BEq α] [Hashable α] {m : Raw α} {δ : Type v} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] (h : m.WF) {f : δ → α → m' δ} {init : δ} :
foldM f init m = List.foldlM f init m.toList
source
theorem Std.HashSet.Raw.fold_eq_foldl_toList {α : Type u} [BEq α] [Hashable α] {m : Raw α} {δ : Type v} (h : m.WF) {f : δ → α → δ} {init : δ} :
fold f init m = List.foldl f init m.toList
source
@[simp]
theorem Std.HashSet.Raw.forM_eq_forM {α : Type u} {m : Raw α} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
forM f m = ForM.forM m f
source
theorem Std.HashSet.Raw.forM_eq_forM_toList {α : Type u} [BEq α] [Hashable α] {m : Raw α} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α → m' PUnit} :
ForM.forM m f = ForM.forM m.toList f
source
@[simp]
theorem Std.HashSet.Raw.forIn_eq_forIn {α : Type u} {m : Raw α} {δ : Type v} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} :
forIn f init m = ForIn.forIn m init f
source
theorem Std.HashSet.Raw.forIn_eq_forIn_toList {α : Type u} [BEq α] [Hashable α] {m : Raw α} {δ : Type v} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α → δ → m' (ForInStep δ)} {init : δ} :
ForIn.forIn m init f = ForIn.forIn m.toList init f
source
theorem Std.HashSet.Raw.foldM_eq_foldlM_toArray {α : Type u} [BEq α] [Hashable α] {m : Raw α} {δ : Type v} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ} (h : m.WF) :
foldM (fun (d : δ) (a : α) => f d a) init m = Array.foldlM f init m.toArray
source
theorem Std.HashSet.Raw.fold_eq_foldl_toArray {α : Type u} [BEq α] [Hashable α] {m : Raw α} {δ : Type v} {f : δ → α → δ} {init : δ} (h : m.WF) :
fold (fun (d : δ) (a : α) => f d a) init m = Array.foldl f init m.toArray
source
theorem Std.HashSet.Raw.forM_eq_forM_toArray {α : Type u} [BEq α] [Hashable α] {m : Raw α} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} (h : m.WF) :
forM (fun (a : α) => f a) m = Array.forM f m.toArray
source
theorem Std.HashSet.Raw.forIn_eq_forIn_toArray {α : Type u} [BEq α] [Hashable α] {m : Raw α} {δ : Type v} {m' : Type v → Type w} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
forIn (fun (a : α) (d : δ) => f a d) init m = ForIn.forIn m.toArray init f
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
theorem Std.HashSet.Raw.insertMany_append {α : Type u} {m : Raw α} [BEq α] [Hashable α] (h : m.WF) {l₁ l₂ : List α} :
m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
source
theorem Std.HashSet.Raw.insertMany_ind {α : Type u} [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] {motive : Raw α → Prop} (m : Raw α) (l : ρ) (init : motive m) (insert : ∀ (m : Raw α) (a : α), motive m → motive (m.insert a)) :
motive (m.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.mem_insertMany_of_mem {α : Type u} {m : Raw α} [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : ρ} {k : α} :
k ∈ m → k ∈ m.insertMany l
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_le_size_insertMany {α : Type u} {m : Raw α} [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : ρ} :
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
theorem Std.HashSet.Raw.isEmpty_of_isEmpty_insertMany {α : Type u} {m : Raw α} [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : ρ} :
(m.insertMany l).isEmpty = true → m.isEmpty = true
source
@[simp]
theorem Std.HashSet.Raw.union_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} :
m₁.union m₂ = m₁ ∪ m₂
source
@[simp]
theorem Std.HashSet.Raw.contains_union {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
(m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
source
theorem Std.HashSet.Raw.mem_union_of_left {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
k ∈ m₁ → k ∈ m₁ ∪ m₂
source
theorem Std.HashSet.Raw.mem_union_of_right {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
k ∈ m₂ → k ∈ m₁ ∪ m₂
source
@[simp]
theorem Std.HashSet.Raw.mem_union_iff {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
source
theorem Std.HashSet.Raw.mem_of_mem_union_of_not_mem_right {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁
source
theorem Std.HashSet.Raw.mem_of_mem_union_of_not_mem_left {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂
source
theorem Std.HashSet.Raw.get?_union {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
(m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
source
theorem Std.HashSet.Raw.get?_union_of_not_mem_left {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : ¬k ∈ m₁) :
(m₁ ∪ m₂).get? k = m₂.get? k
source
theorem Std.HashSet.Raw.get?_union_of_not_mem_right {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : ¬k ∈ m₂) :
(m₁ ∪ m₂).get? k = m₁.get? k
source
theorem Std.HashSet.Raw.get_union_of_mem_right {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂) :
(m₁ ∪ m₂).get k ⋯ = m₂.get k mem
source
theorem Std.HashSet.Raw.get_union_of_not_mem_left {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : ¬k ∈ m₁) {h' : k ∈ m₁ ∪ m₂} :
(m₁ ∪ m₂).get k h' = m₂.get k ⋯
source
theorem Std.HashSet.Raw.get_union_of_not_mem_right {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : ¬k ∈ m₂) {h' : k ∈ m₁ ∪ m₂} :
(m₁ ∪ m₂).get k h' = m₁.get k ⋯
source
theorem Std.HashSet.Raw.getD_union {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k fallback : α} :
(m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
source
theorem Std.HashSet.Raw.getD_union_of_not_mem_left {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k fallback : α} (not_mem : ¬k ∈ m₁) :
(m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
source
theorem Std.HashSet.Raw.getD_union_of_not_mem_right {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k fallback : α} (not_mem : ¬k ∈ m₂) :
(m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
source
theorem Std.HashSet.Raw.get!_union {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
(m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
source
theorem Std.HashSet.Raw.get!_union_of_not_mem_left {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [Inhabited α] [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : ¬k ∈ m₁) :
(m₁ ∪ m₂).get! k = m₂.get! k
source
theorem Std.HashSet.Raw.get!_union_of_not_mem_right {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [Inhabited α] [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : ¬k ∈ m₂) :
(m₁ ∪ m₂).get! k = m₁.get! k
source
theorem Std.HashSet.Raw.size_union_of_not_mem {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
(∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
source
theorem Std.HashSet.Raw.size_left_le_size_union {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
m₁.size ≤ (m₁ ∪ m₂).size
source
theorem Std.HashSet.Raw.size_right_le_size_union {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
m₂.size ≤ (m₁ ∪ m₂).size
source
theorem Std.HashSet.Raw.size_union_le_size_add_size {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁ ∪ m₂).size ≤ m₁.size + m₂.size
source
@[simp]
theorem Std.HashSet.Raw.isEmpty_union {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.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
theorem Std.HashSet.Raw.ofList_eq_insertMany_empty {α : Type u} [BEq α] [Hashable α] {l : List α} :
ofList l = ∅.insertMany l
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
source
@[simp]
theorem Std.HashSet.Raw.Equiv.refl {α : Type u} (m : Raw α) :
m.Equiv m
source
theorem Std.HashSet.Raw.Equiv.rfl {α : Type u} {m : Raw α} :
m.Equiv m
source
theorem Std.HashSet.Raw.Equiv.symm {α : Type u} {m₁ m₂ : Raw α} :
m₁.Equiv m₂ → m₂.Equiv m₁
source
theorem Std.HashSet.Raw.Equiv.trans {α : Type u} {m₁ m₂ m₃ : Raw α} :
m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
source
instance Std.HashSet.Raw.Equiv.instTrans {α : Type u} :
Trans Equiv Equiv Equiv
Equations

- Std.HashSet.Raw.Equiv.instTrans = { trans := ⋯ }

source
theorem Std.HashSet.Raw.Equiv.comm {α : Type u} {m₁ m₂ : Raw α} :
m₁.Equiv m₂ ↔ m₂.Equiv m₁
source
theorem Std.HashSet.Raw.Equiv.congr_left {α : Type u} {m₁ m₂ m₃ : Raw α} (h : m₁.Equiv m₂) :
m₁.Equiv m₃ ↔ m₂.Equiv m₃
source
theorem Std.HashSet.Raw.Equiv.congr_right {α : Type u} {m₁ m₂ m₃ : Raw α} (h : m₁.Equiv m₂) :
m₃.Equiv m₁ ↔ m₃.Equiv m₂
source
theorem Std.HashSet.Raw.Equiv.toList_perm {α : Type u} {m₁ m₂ : Raw α} (h : m₁.Equiv m₂) :
m₁.toList.Perm m₂.toList
source
theorem Std.HashSet.Raw.Equiv.of_toList_perm {α : Type u} {m₁ m₂ : Raw α} (h : m₁.toList.Perm m₂.toList) :
m₁.Equiv m₂
source
theorem Std.HashSet.Raw.Equiv.isEmpty_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) :
m₁.isEmpty = m₂.isEmpty
source
theorem Std.HashSet.Raw.Equiv.size_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) :
m₁.size = m₂.size
source
theorem Std.HashSet.Raw.Equiv.contains_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) :
m₁.contains k = m₂.contains k
source
theorem Std.HashSet.Raw.Equiv.mem_iff {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) :
k ∈ m₁ ↔ k ∈ m₂
source
theorem Std.HashSet.Raw.Equiv.get?_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) :
m₁.get? k = m₂.get? k
source
theorem Std.HashSet.Raw.Equiv.get_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂) :
m₁.get k hk = m₂.get k ⋯
source
theorem Std.HashSet.Raw.Equiv.get!_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) :
m₁.get! k = m₂.get! k
source
theorem Std.HashSet.Raw.Equiv.getD_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) :
m₁.getD k fallback = m₂.getD k fallback
source
theorem Std.HashSet.Raw.Equiv.insert {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : α) (h : m₁.Equiv m₂) :
(m₁.insert k).Equiv (m₂.insert k)
source
theorem Std.HashSet.Raw.Equiv.erase {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : α) (h : m₁.Equiv m₂) :
(m₁.erase k).Equiv (m₂.erase k)
source
theorem Std.HashSet.Raw.Equiv.insertMany_list {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (l : List α) (h : m₁.Equiv m₂) :
(m₁.insertMany l).Equiv (m₂.insertMany l)
source
theorem Std.HashSet.Raw.Equiv.filter {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (f : α → Bool) (h : m₁.Equiv m₂) :
(Raw.filter f m₁).Equiv (Raw.filter f m₂)
source
theorem Std.HashSet.Raw.Equiv.of_forall_get?_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : ∀ (k : α), m₁.get? k = m₂.get? k) :
m₁.Equiv m₂
source
theorem Std.HashSet.Raw.Equiv.of_forall_contains_eq {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : ∀ (k : α), m₁.contains k = m₂.contains k) :
m₁.Equiv m₂
source
theorem Std.HashSet.Raw.Equiv.of_forall_mem_iff {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) :
m₁.Equiv m₂
source
theorem Std.HashSet.Raw.equiv_emptyWithCapacity_iff_isEmpty {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) :
m.Equiv (emptyWithCapacity c) ↔ m.isEmpty = true
source
theorem Std.HashSet.Raw.equiv_empty_iff_isEmpty {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.Equiv ∅ ↔ m.isEmpty = true
source
@[reducible, inline, deprecated Std.HashSet.Raw.equiv_empty_iff_isEmpty (since := "2025-03-12")]
abbrev Std.HashSet.Raw.equiv_emptyc_iff_isEmpty {α : Type u_1} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.Equiv ∅ ↔ m.isEmpty = true
Equations

- @Std.HashSet.Raw.equiv_emptyc_iff_isEmpty = @Std.HashSet.Raw.equiv_empty_iff_isEmpty

Instances For

source
theorem Std.HashSet.Raw.equiv_iff_toList_perm {α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] :
m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
source
theorem Std.HashSet.Raw.toList_filter {α : Type u} {m : Raw α} [BEq α] [Hashable α] {f : α → Bool} (h : m.WF) :
(filter f m).toList.Perm (List.filter f m.toList)
source
theorem Std.HashSet.Raw.isEmpty_filter_iff {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} (h : m.WF) :
(filter f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = false
source
theorem Std.HashSet.Raw.isEmpty_filter_eq_false_iff {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} (h : m.WF) :
(filter f m).isEmpty = false ↔ ∃ (k : α), ∃ (h : k ∈ m), f (m.get k h) = true
source
@[simp]
theorem Std.HashSet.Raw.mem_filter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} (h : m.WF) :
k ∈ filter f m ↔ ∃ (h' : k ∈ m), f (m.get k h') = true
source
theorem Std.HashSet.Raw.mem_of_mem_filter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} (h : m.WF) :
k ∈ filter f m → k ∈ m
source
theorem Std.HashSet.Raw.size_filter_le_size {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} (h : m.WF) :
(filter f m).size ≤ m.size
source
theorem Std.HashSet.Raw.size_filter_eq_size_iff {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} (h : m.WF) :
(filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true
source
theorem Std.HashSet.Raw.filter_equiv_self_iff {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} (h : m.WF) :
(filter f m).Equiv m ↔ ∀ (a : α) (h : a ∈ m), f (m.get a h) = true
source
@[simp]
theorem Std.HashSet.Raw.get?_filter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} (h : m.WF) :
(filter f m).get? k = Option.filter f (m.get? k)
source
@[simp]
theorem Std.HashSet.Raw.get_filter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} {h' : k ∈ filter f m} (h : m.WF) :
(filter f m).get k h' = m.get k ⋯
source
theorem Std.HashSet.Raw.get!_filter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → Bool} {k : α} (h : m.WF) :
(filter f m).get! k = (Option.filter f (m.get? k)).get!
source
theorem Std.HashSet.Raw.getD_filter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} (h : m.WF) :
(filter f m).getD k fallback = (Option.filter f (m.get? k)).getD fallback