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_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {c : Nat} : (emptyWithCapacity c).isEmpty = true

@[simp]

theorem Std.HashSet.isEmpty_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} : ∅.isEmpty = true

@[reducible, inline, deprecated Std.HashSet.isEmpty_empty (since := "2025-03-12")]

abbrev Std.HashSet.isEmpty_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} : ∅.isEmpty = true

Equations

• @Std.HashSet.isEmpty_emptyc = @Std.HashSet.isEmpty_empty

@[simp]

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

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

theorem Std.HashSet.contains_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) : m.contains a = m.contains b

theorem Std.HashSet.mem_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) : a ∈ m ↔ b ∈ m

@[simp]

theorem Std.HashSet.contains_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : (emptyWithCapacity c).contains a = false

@[simp]

theorem Std.HashSet.not_mem_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : ¬a ∈ emptyWithCapacity c

@[simp]

theorem Std.HashSet.contains_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.contains a = false

@[reducible, inline, deprecated Std.HashSet.contains_empty (since := "2025-03-12")]

abbrev Std.HashSet.contains_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.contains a = false

Equations

• @Std.HashSet.contains_emptyc = @Std.HashSet.contains_empty

@[simp]

theorem Std.HashSet.not_mem_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ¬a ∈ ∅

@[reducible, inline, deprecated Std.HashSet.not_mem_empty (since := "2025-03-12")]

abbrev Std.HashSet.not_mem_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ¬a ∈ ∅

Equations

• @Std.HashSet.not_mem_emptyc = @Std.HashSet.not_mem_empty

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

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

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

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

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

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

@[simp]

theorem Std.HashSet.insert_eq_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {a : α} : Insert.insert a m = m.insert a

@[simp]

theorem Std.HashSet.singleton_eq_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : {a} = ∅.insert a

@[simp]

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

@[simp]

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

theorem Std.HashSet.contains_of_contains_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [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✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k → (k == a) = false → a ∈ m

theorem Std.HashSet.contains_of_contains_insert' {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {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.

theorem Std.HashSet.mem_of_mem_insert' {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {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.

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

theorem Std.HashSet.mem_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k

@[simp]

theorem Std.HashSet.size_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {c : Nat} : (emptyWithCapacity c).size = 0

@[simp]

theorem Std.HashSet.size_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} : ∅.size = 0

@[reducible, inline, deprecated Std.HashSet.size_empty (since := "2025-03-12")]

abbrev Std.HashSet.size_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} : ∅.size = 0

Equations

• @Std.HashSet.size_emptyc = @Std.HashSet.size_empty

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

theorem Std.HashSet.size_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [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✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size

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

@[simp]

theorem Std.HashSet.erase_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : (emptyWithCapacity c).erase a = emptyWithCapacity c

@[simp]

theorem Std.HashSet.erase_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.erase a = ∅

@[reducible, inline, deprecated Std.HashSet.erase_empty (since := "2025-03-12")]

abbrev Std.HashSet.erase_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.erase a = ∅

Equations

• @Std.HashSet.erase_emptyc = @Std.HashSet.erase_empty

@[simp]

theorem Std.HashSet.isEmpty_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [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✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = (!k == a && m.contains a)

@[simp]

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

theorem Std.HashSet.contains_of_contains_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [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✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m

theorem Std.HashSet.size_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [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✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size

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

@[simp]

theorem Std.HashSet.get?_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : (emptyWithCapacity c).get? a = none

@[simp]

theorem Std.HashSet.get?_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.get? a = none

@[reducible, inline, deprecated Std.HashSet.get?_empty (since := "2025-03-12")]

abbrev Std.HashSet.get?_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.get? a = none

Equations

• @Std.HashSet.get?_emptyc = @Std.HashSet.get?_empty

theorem Std.HashSet.get?_of_isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.get? a = none

theorem Std.HashSet.get?_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.insert k).get? a = if (k == a) = true ∧ ¬k ∈ m then some k else m.get? a

theorem Std.HashSet.contains_eq_isSome_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = (m.get? a).isSome

theorem Std.HashSet.get?_eq_none_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m.get? a = none

theorem Std.HashSet.get?_eq_none {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.get? a = none

theorem Std.HashSet.get?_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).get? a = if (k == a) = true then none else m.get? a

@[simp]

theorem Std.HashSet.get?_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).get? k = none

theorem Std.HashSet.get?_beq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : Option.all (fun (x : α) => x == k) (m.get? k) = true

theorem Std.HashSet.get?_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k k' : α} (h : (k == k') = true) : m.get? k = m.get? k'

theorem Std.HashSet.get?_eq_some_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] {k : α} (h : m.contains k = true) : m.get? k = some k

theorem Std.HashSet.get?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] {k : α} (h : k ∈ m) : m.get? k = some k

theorem Std.HashSet.get_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {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 ⋯

@[simp]

theorem Std.HashSet.get_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} : (m.erase k).get a h' = m.get a ⋯

theorem Std.HashSet.get?_eq_some_get {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} : m.get? a = some (m.get a h')

theorem Std.HashSet.get_beq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) : (m.get k h == k) = true

theorem Std.HashSet.get_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m) : m.get k₁ h₁ = m.get k₂ ⋯

theorem Std.HashSet.get_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] {k : α} (h : k ∈ m) : m.get k h = k

@[simp]

theorem Std.HashSet.get!_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] {a : α} {c : Nat} : (emptyWithCapacity c).get! a = default

@[simp]

theorem Std.HashSet.get!_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] {a : α} : ∅.get! a = default

@[reducible, inline, deprecated Std.HashSet.get!_empty (since := "2025-03-12")]

abbrev Std.HashSet.get!_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] {a : α} : ∅.get! a = default

Equations

• @Std.HashSet.get!_emptyc = @Std.HashSet.get!_empty

theorem Std.HashSet.get!_of_isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.get! a = default

theorem Std.HashSet.get!_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} : (m.insert k).get! a = if (k == a) = true ∧ ¬k ∈ m then k else m.get! a

theorem Std.HashSet.get!_eq_default_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m.get! a = default

theorem Std.HashSet.get!_eq_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.get! a = default

theorem Std.HashSet.get!_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).get! a = if (k == a) = true then default else m.get! a

@[simp]

theorem Std.HashSet.get!_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).get! k = default

theorem Std.HashSet.get?_eq_some_get!_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.contains a = true → m.get? a = some (m.get! a)

theorem Std.HashSet.get?_eq_some_get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : a ∈ m → m.get? a = some (m.get! a)

theorem Std.HashSet.get!_eq_get!_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.get! a = (m.get? a).get!

theorem Std.HashSet.get_eq_get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h' : a ∈ m} : m.get a h' = m.get! a

theorem Std.HashSet.get!_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : (k == k') = true) : m.get! k = m.get! k'

theorem Std.HashSet.get!_eq_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k = true) : m.get! k = k

theorem Std.HashSet.get!_eq_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.get! k = k

@[simp]

theorem Std.HashSet.getD_emptyWithCapacity {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a fallback : α} {c : Nat} : (emptyWithCapacity c).getD a fallback = fallback

@[simp]

theorem Std.HashSet.getD_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {a fallback : α} : ∅.getD a fallback = fallback

@[reducible, inline, deprecated Std.HashSet.getD_empty (since := "2025-03-12")]

abbrev Std.HashSet.getD_emptyc {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {a fallback : α} : ∅.getD a fallback = fallback

Equations

• @Std.HashSet.getD_emptyc = @Std.HashSet.getD_empty

theorem Std.HashSet.getD_of_isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.isEmpty = true → m.getD a fallback = fallback

theorem Std.HashSet.getD_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a fallback : α} : (m.insert k).getD a fallback = if (k == a) = true ∧ ¬k ∈ m then k else m.getD a fallback

theorem Std.HashSet.getD_eq_fallback_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.contains a = false → m.getD a fallback = fallback

theorem Std.HashSet.getD_eq_fallback {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : ¬a ∈ m → m.getD a fallback = fallback

theorem Std.HashSet.getD_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k a fallback : α} : (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback

@[simp]

theorem Std.HashSet.getD_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} : (m.erase k).getD k fallback = fallback

theorem Std.HashSet.get?_eq_some_getD_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.contains a = true → m.get? a = some (m.getD a fallback)

theorem Std.HashSet.get?_eq_some_getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : a ∈ m → m.get? a = some (m.getD a fallback)

theorem Std.HashSet.getD_eq_getD_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.getD a fallback = (m.get? a).getD fallback

theorem Std.HashSet.get_eq_getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} {h' : a ∈ m} : m.get a h' = m.getD a fallback

theorem Std.HashSet.get!_eq_getD_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.get! a = m.getD a default

theorem Std.HashSet.getD_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} (h : (k == k') = true) : m.getD k fallback = m.getD k' fallback

theorem Std.HashSet.getD_eq_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] {k fallback : α} (h : m.contains k = true) : m.getD k fallback = k

theorem Std.HashSet.getD_eq_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] {k fallback : α} (h : k ∈ m) : m.getD k fallback = k

@[simp]

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

@[simp]

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

@[simp]

theorem Std.HashSet.length_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] : m.toList.length = m.size

@[simp]

theorem Std.HashSet.isEmpty_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] : m.toList.isEmpty = m.isEmpty

@[simp]

theorem Std.HashSet.contains_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : m.toList.contains k = m.contains k

@[simp]

theorem Std.HashSet.mem_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [LawfulBEq α] [LawfulHashable α] {k : α} : k ∈ m.toList ↔ k ∈ m

theorem Std.HashSet.distinct_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] : List.Pairwise (fun (a b : α) => (a == b) = false) m.toList

theorem Std.HashSet.foldM_eq_foldlM_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {δ : Type v} {m' : Type v → Type v} [Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ} : foldM f init m = List.foldlM f init m.toList

theorem Std.HashSet.fold_eq_foldl_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {δ : Type v} {f : δ → α → δ} {init : δ} : fold f init m = List.foldl f init m.toList

@[simp]

theorem Std.HashSet.forM_eq_forM {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {m' : Type v → Type v} [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} : forM f m = ForM.forM m f

theorem Std.HashSet.forM_eq_forM_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {m' : Type v → Type v} [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} : ForM.forM m f = ForM.forM m.toList f

@[simp]

theorem Std.HashSet.forIn_eq_forIn {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {δ : Type v} {m' : Type v → Type v} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} : ForIn.forIn m init f = ForIn.forIn m init f

theorem Std.HashSet.forIn_eq_forIn_toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {δ : Type v} {m' : Type v → Type v} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} : ForIn.forIn m init f = ForIn.forIn m.toList init f

@[simp]

theorem Std.HashSet.insertMany_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} : m.insertMany [] = m

@[simp]

theorem Std.HashSet.insertMany_list_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {k : α} : m.insertMany [k] = m.insert k

theorem Std.HashSet.insertMany_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} {l : List α} {k : α} : m.insertMany (k :: l) = (m.insert k).insertMany l

@[simp]

theorem Std.HashSet.contains_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (m.insertMany l).contains k = (m.contains k || l.contains k)

@[simp]

theorem Std.HashSet.mem_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : k ∈ m.insertMany l ↔ k ∈ m ∨ l.contains k = true

theorem Std.HashSet.mem_of_mem_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : k ∈ m.insertMany l → k ∈ m

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

theorem Std.HashSet.get?_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {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

theorem Std.HashSet.get?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) : (m.insertMany l).get? k = m.get? k

theorem Std.HashSet.get_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {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

theorem Std.HashSet.get_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) {h : k ∈ m.insertMany l} : (m.insertMany l).get k h = m.get k mem

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

theorem Std.HashSet.get!_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {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

theorem Std.HashSet.get!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (mem : k ∈ m) : (m.insertMany l).get! k = m.get! k

theorem Std.HashSet.getD_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) : (m.insertMany l).getD k fallback = fallback

theorem Std.HashSet.getD_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {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

theorem Std.HashSet.getD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (mem : k ∈ m) : (m.insertMany l).getD k fallback = m.getD k fallback

theorem Std.HashSet.size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {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

theorem Std.HashSet.size_le_size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} : m.size ≤ (m.insertMany l).size

theorem Std.HashSet.size_insertMany_list_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} : (m.insertMany l).size ≤ m.size + l.length

@[simp]

theorem Std.HashSet.isEmpty_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} : (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)

@[simp]

theorem Std.HashSet.ofList_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} : ofList [] = ∅

@[simp]

theorem Std.HashSet.ofList_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {k : α} : ofList [k] = ∅.insert k

theorem Std.HashSet.ofList_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {hd : α} {tl : List α} : ofList (hd :: tl) = (∅.insert hd).insertMany tl

@[simp]

theorem Std.HashSet.contains_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (ofList l).contains k = l.contains k

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

theorem Std.HashSet.get?_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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

theorem Std.HashSet.get_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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

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

theorem Std.HashSet.get!_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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

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

theorem Std.HashSet.getD_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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

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

theorem Std.HashSet.size_ofList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : (ofList l).size ≤ l.length

@[simp]

theorem Std.HashSet.isEmpty_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : (ofList l).isEmpty = l.isEmpty

theorem Std.HashSet.Equiv.refl {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashSet α) : m.Equiv m

theorem Std.HashSet.Equiv.rfl {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} : m.Equiv m

theorem Std.HashSet.Equiv.symm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} : m₁.Equiv m₂ → m₂.Equiv m₁

theorem Std.HashSet.Equiv.trans {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : HashSet α} : m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃

theorem Std.HashSet.Equiv.comm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} : m₁.Equiv m₂ ↔ m₂.Equiv m₁

theorem Std.HashSet.Equiv.congr_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : HashSet α} (h : m₁.Equiv m₂) : m₁.Equiv m₃ ↔ m₂.Equiv m₃

theorem Std.HashSet.Equiv.congr_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : HashSet α} (h : m₁.Equiv m₂) : m₃.Equiv m₁ ↔ m₃.Equiv m₂

theorem Std.HashSet.Equiv.isEmpty_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] (h : m₁.Equiv m₂) : m₁.isEmpty = m₂.isEmpty

theorem Std.HashSet.Equiv.size_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] (h : m₁.Equiv m₂) : m₁.size = m₂.size

theorem Std.HashSet.Equiv.contains_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : m₁.Equiv m₂) : m₁.contains k = m₂.contains k

theorem Std.HashSet.Equiv.mem_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : m₁.Equiv m₂) : k ∈ m₁ ↔ k ∈ m₂

theorem Std.HashSet.Equiv.toList_perm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} (h : m₁.Equiv m₂) : m₁.toList.Perm m₂.toList

theorem Std.HashSet.Equiv.of_toList_perm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} (h : m₁.toList.Perm m₂.toList) : m₁.Equiv m₂

theorem Std.HashSet.Equiv.get?_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : m₁.Equiv m₂) : m₁.get? k = m₂.get? k

theorem Std.HashSet.Equiv.get_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (hk : k ∈ m₁) (h : m₁.Equiv m₂) : m₁.get k hk = m₂.get k ⋯

theorem Std.HashSet.Equiv.get!_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (h : m₁.Equiv m₂) : m₁.get! k = m₂.get! k

theorem Std.HashSet.Equiv.getD_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (h : m₁.Equiv m₂) : m₁.getD k fallback = m₂.getD k fallback

theorem Std.HashSet.Equiv.insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] (k : α) (h : m₁.Equiv m₂) : (m₁.insert k).Equiv (m₂.insert k)

theorem Std.HashSet.Equiv.erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] (k : α) (h : m₁.Equiv m₂) : (m₁.erase k).Equiv (m₂.erase k)

theorem Std.HashSet.Equiv.insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] (l : List α) (h : m₁.Equiv m₂) : (m₁.insertMany l).Equiv (m₂.insertMany l)

theorem Std.HashSet.Equiv.filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} (f : α → Bool) (h : m₁.Equiv m₂) : (HashSet.filter f m₁).Equiv (HashSet.filter f m₂)

theorem Std.HashSet.Equiv.of_forall_get?_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] (h : ∀ (k : α), m₁.get? k = m₂.get? k) : m₁.Equiv m₂

theorem Std.HashSet.Equiv.of_forall_contains_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [LawfulBEq α] (h : ∀ (k : α), m₁.contains k = m₂.contains k) : m₁.Equiv m₂

theorem Std.HashSet.Equiv.of_forall_mem_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [LawfulBEq α] (h : ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) : m₁.Equiv m₂

@[simp]

theorem Std.HashSet.equiv_emptyWithCapacity_iff_isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {c : Nat} : m.Equiv (emptyWithCapacity c) ↔ m.isEmpty = true

@[simp]

theorem Std.HashSet.equiv_empty_iff_isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] : m.Equiv ∅ ↔ m.isEmpty = true

@[reducible, inline, deprecated Std.HashSet.equiv_empty_iff_isEmpty (since := "2025-03-12")]

abbrev Std.HashSet.equiv_emptyc_iff_isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] : m.Equiv ∅ ↔ m.isEmpty = true

Equations

• @Std.HashSet.equiv_emptyc_iff_isEmpty = @Std.HashSet.equiv_empty_iff_isEmpty

@[simp]

theorem Std.HashSet.emptyWithCapacity_equiv_iff_isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] {c : Nat} : (emptyWithCapacity c).Equiv m ↔ m.isEmpty = true

@[simp]

theorem Std.HashSet.empty_equiv_iff_isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] : ∅.Equiv m ↔ m.isEmpty = true

@[reducible, inline, deprecated Std.HashSet.empty_equiv_iff_isEmpty (since := "2025-03-12")]

abbrev Std.HashSet.emptyc_equiv_iff_isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashSet α} [EquivBEq α] [LawfulHashable α] : ∅.Equiv m ↔ m.isEmpty = true

Equations

• @Std.HashSet.emptyc_equiv_iff_isEmpty = @Std.HashSet.empty_equiv_iff_isEmpty

theorem Std.HashSet.equiv_iff_toList_perm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : HashSet α} [EquivBEq α] [LawfulHashable α] : m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList