Extensional hash set lemmas

This module contains lemmas about Std.ExtHashSet.

@[simp]

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

@[simp]

theorem Std.ExtHashSet.isEmpty_eq_false_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m.isEmpty = false ↔ ¬m = ∅

@[simp]

theorem Std.ExtHashSet.empty_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} : ∅ = m ↔ m = ∅

@[simp]

theorem Std.ExtHashSet.emptyWithCapacity_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {c : Nat} : emptyWithCapacity c = ∅

@[simp]

theorem Std.ExtHashSet.not_insert_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : ¬m.insert k = ∅

theorem Std.ExtHashSet.mem_iff_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a = true

@[simp]

theorem Std.ExtHashSet.contains_iff_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = true ↔ a ∈ m

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

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

@[simp]

theorem Std.ExtHashSet.contains_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} : ∅.contains a = false

@[simp]

theorem Std.ExtHashSet.not_mem_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ ∅

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

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

@[simp]

theorem Std.ExtHashSet.insert_eq_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : Insert.insert a m = m.insert a

@[simp]

theorem Std.ExtHashSet.singleton_eq_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} : {a} = ∅.insert a

@[simp]

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

@[simp]

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

theorem Std.ExtHashSet.contains_of_contains_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.insert k).contains a = true → (k == a) = false → m.contains a = true

theorem Std.ExtHashSet.mem_of_mem_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k → (k == a) = false → a ∈ m

theorem Std.ExtHashSet.contains_of_contains_insert' {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.mem_of_mem_insert' {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.contains_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k = true

theorem Std.ExtHashSet.mem_of_get_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : ExtHashSet α) {k v : α} {w : k ∈ m} : m.get k w = v → k ∈ m

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

@[simp]

theorem Std.ExtHashSet.size_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : ∅.size = 0

theorem Std.ExtHashSet.eq_empty_iff_size_eq_zero {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m = ∅ ↔ m.size = 0

theorem Std.ExtHashSet.size_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).size = if k ∈ m then m.size else m.size + 1

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

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

@[simp]

theorem Std.ExtHashSet.erase_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} : ∅.erase a = ∅

@[simp]

theorem Std.ExtHashSet.erase_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : m.erase k = ∅ ↔ m = ∅ ∨ m.size = 1 ∧ k ∈ m

@[simp]

theorem Std.ExtHashSet.contains_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = (!k == a && m.contains a)

@[simp]

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

theorem Std.ExtHashSet.contains_of_contains_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = true → m.contains a = true

theorem Std.ExtHashSet.mem_of_mem_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m

theorem Std.ExtHashSet.size_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size = if k ∈ m then m.size - 1 else m.size

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

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

@[simp]

theorem Std.ExtHashSet.get?_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} : ∅.get? a = none

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

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

@[simp]

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

theorem Std.ExtHashSet.mem_iff_isSome_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ (m.get? a).isSome = true

@[simp]

theorem Std.ExtHashSet.isSome_get?_iff_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {a : α} : (m.get? a).isSome = true ↔ a ∈ m

theorem Std.ExtHashSet.get?_eq_some_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k k' : α} : m.get? k = some k' ↔ ∃ (h : k ∈ m), m.get k h = k'

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

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

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

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

@[simp]

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

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

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

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

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

theorem Std.ExtHashSet.get_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.get_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} : (m.erase k).get a h' = m.get a ⋯

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

theorem Std.ExtHashSet.get_eq_get_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} {h : k ∈ m} : m.get k h = (m.get? k).get ⋯

theorem Std.ExtHashSet.get_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} {h : (m.get? k).isSome = true} : (m.get? k).get h = m.get k ⋯

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

theorem Std.ExtHashSet.getD_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : ∅.getD a fallback = fallback

theorem Std.ExtHashSet.getD_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.getD_eq_fallback_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.contains a = false → m.getD a fallback = fallback

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

theorem Std.ExtHashSet.getD_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.getD_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} : (m.erase k).getD k fallback = fallback

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

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

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

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

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

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

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

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

@[simp]

theorem Std.ExtHashSet.containsThenInsert_fst {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.containsThenInsert k).fst = m.contains k

@[simp]

theorem Std.ExtHashSet.containsThenInsert_snd {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.containsThenInsert k).snd = m.insert k

@[simp]

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

@[simp]

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

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

theorem Std.ExtHashSet.insertMany_append {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {l₁ l₂ : List α} : m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂

theorem Std.ExtHashSet.insertMany_ind {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type v} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {motive : ExtHashSet α → Prop} (m : ExtHashSet α) {l : ρ} (init : motive m) (insert : ∀ (m : ExtHashSet α) (a : α), motive m → motive (m.insert a)) : motive (m.insertMany l)

@[simp]

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

@[simp]

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

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

theorem Std.ExtHashSet.mem_insertMany_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} {ρ : Type v} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α} : k ∈ m → k ∈ m.insertMany l

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

theorem Std.ExtHashSet.get?_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.get?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) : (m.insertMany l).get? k = m.get? k

theorem Std.ExtHashSet.get_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.get_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.get!_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.get!_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.get!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (mem : k ∈ m) : (m.insertMany l).get! k = m.get! k

theorem Std.ExtHashSet.getD_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.getD_insertMany_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.getD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (mem : k ∈ m) : (m.insertMany l).getD k fallback = m.getD k fallback

theorem Std.ExtHashSet.size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [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.ExtHashSet.size_le_size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} : m.size ≤ (m.insertMany l).size

theorem Std.ExtHashSet.size_le_size_insertMany {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} {ρ : Type v} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} : m.size ≤ (m.insertMany l).size

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

@[simp]

theorem Std.ExtHashSet.insertMany_list_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} : m.insertMany l = ∅ ↔ m = ∅ ∧ l = []

theorem Std.ExtHashSet.eq_empty_of_insertMany_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} {ρ : Type v} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} : m.insertMany l = ∅ → m = ∅

theorem Std.ExtHashSet.insertMany_list_eq_foldl {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} : m.insertMany l = List.foldl (fun (acc : ExtHashSet α) (a : α) => acc.insert a) m l

@[simp]

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

@[simp]

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

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

theorem Std.ExtHashSet.ofList_eq_insertMany_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : ofList l = ∅.insertMany l

@[simp]

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

@[simp]

theorem Std.ExtHashSet.mem_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : k ∈ ofList l ↔ l.contains k = true

theorem Std.ExtHashSet.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.ExtHashSet.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.ExtHashSet.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.ExtHashSet.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.ExtHashSet.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.ExtHashSet.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.ExtHashSet.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.ExtHashSet.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.ExtHashSet.size_ofList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : (ofList l).size ≤ l.length

@[simp]

theorem Std.ExtHashSet.ofList_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : ofList l = ∅ ↔ l = []

theorem Std.ExtHashSet.ofList_eq_foldl {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : ofList l = List.foldl (fun (acc : ExtHashSet α) (a : α) => acc.insert a) ∅ l

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

theorem Std.ExtHashSet.ext_get?_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : ExtHashSet α} : m₁ = m₂ ↔ ∀ (k : α), m₁.get? k = m₂.get? k

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

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

theorem Std.ExtHashSet.ext_mem_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {m₁ m₂ : ExtHashSet α} : m₁ = m₂ ↔ ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂

theorem Std.ExtHashSet.filter_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} : filter f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = false

@[simp]

theorem Std.ExtHashSet.mem_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} : k ∈ filter f m ↔ ∃ (h : k ∈ m), f (m.get k h) = true

theorem Std.ExtHashSet.contains_of_contains_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} : (filter f m).contains k = true → m.contains k = true

theorem Std.ExtHashSet.mem_of_mem_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} : k ∈ filter f m → k ∈ m

theorem Std.ExtHashSet.size_filter_le_size {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} : (filter f m).size ≤ m.size

theorem Std.ExtHashSet.size_filter_eq_size_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} : (filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true

theorem Std.ExtHashSet.filter_eq_self_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} : filter f m = m ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true

@[simp]

theorem Std.ExtHashSet.get?_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} : (filter f m).get? k = Option.filter f (m.get? k)

@[simp]

theorem Std.ExtHashSet.get_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} {h : k ∈ filter f m} : (filter f m).get k h = m.get k ⋯

theorem Std.ExtHashSet.get!_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → Bool} {k : α} : (filter f m).get! k = (Option.filter f (m.get? k)).get!

theorem Std.ExtHashSet.getD_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} : (filter f m).getD k fallback = (Option.filter f (m.get? k)).getD fallback

@[simp]

theorem Std.ExtHashSet.union_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m₁.union m₂ = m₁ ∪ m₂

@[simp]

theorem Std.ExtHashSet.contains_union {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)

theorem Std.ExtHashSet.mem_union_of_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m₁ → k ∈ m₁ ∪ m₂

theorem Std.ExtHashSet.mem_union_of_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m₂ → k ∈ m₁ ∪ m₂

@[simp]

theorem Std.ExtHashSet.mem_union_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂

theorem Std.ExtHashSet.mem_of_mem_union_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁

theorem Std.ExtHashSet.mem_of_mem_union_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂

theorem Std.ExtHashSet.get?_union {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)

theorem Std.ExtHashSet.get?_union_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₁) : (m₁ ∪ m₂).get? k = m₂.get? k

theorem Std.ExtHashSet.get_union_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (mem : k ∈ m₂) : (m₁ ∪ m₂).get k ⋯ = m₂.get k mem

theorem Std.ExtHashSet.get_union_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₁) {h' : k ∈ m₁ ∪ m₂} : (m₁ ∪ m₂).get k h' = m₂.get k ⋯

theorem Std.ExtHashSet.get_union_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₂) {h' : k ∈ m₁ ∪ m₂} : (m₁ ∪ m₂).get k h' = m₁.get k ⋯

theorem Std.ExtHashSet.getD_union {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} : (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)

theorem Std.ExtHashSet.getD_union_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (not_mem : ¬k ∈ m₁) : (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback

theorem Std.ExtHashSet.getD_union_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (not_mem : ¬k ∈ m₂) : (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback

theorem Std.ExtHashSet.get!_union {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)

theorem Std.ExtHashSet.get!_union_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₁) : (m₁ ∪ m₂).get! k = m₂.get! k

theorem Std.ExtHashSet.get!_union_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [Inhabited α] [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₂) : (m₁ ∪ m₂).get! k = m₁.get! k

theorem Std.ExtHashSet.size_union_of_not_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size

theorem Std.ExtHashSet.size_left_le_size_union {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size

theorem Std.ExtHashSet.size_right_le_size_union {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m₂.size ≤ (m₁ ∪ m₂).size

theorem Std.ExtHashSet.size_union_le_size_add_size {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ ∪ m₂).size ≤ m₁.size + m₂.size

@[simp]

theorem Std.ExtHashSet.isEmpty_union {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)

@[simp]

theorem Std.ExtHashSet.inter_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m₁.inter m₂ = m₁ ∩ m₂

@[simp]

theorem Std.ExtHashSet.contains_inter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)

@[simp]

theorem Std.ExtHashSet.mem_inter_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂

theorem Std.ExtHashSet.not_mem_inter_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₁) : ¬k ∈ m₁ ∩ m₂

theorem Std.ExtHashSet.not_mem_inter_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₂) : ¬k ∈ m₁ ∩ m₂

theorem Std.ExtHashSet.get?_inter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none

theorem Std.ExtHashSet.get?_inter_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (mem : k ∈ m₂) : (m₁ ∩ m₂).get? k = m₁.get? k

theorem Std.ExtHashSet.get?_inter_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₁) : (m₁ ∩ m₂).get? k = none

theorem Std.ExtHashSet.get?_inter_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₂) : (m₁ ∩ m₂).get? k = none

@[simp]

theorem Std.ExtHashSet.get_inter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂} : (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯

theorem Std.ExtHashSet.getD_inter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} : (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback

theorem Std.ExtHashSet.getD_inter_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (mem : k ∈ m₂) : (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback

theorem Std.ExtHashSet.getD_inter_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (not_mem : ¬k ∈ m₂) : (m₁ ∩ m₂).getD k fallback = fallback

theorem Std.ExtHashSet.getD_inter_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (not_mem : ¬k ∈ m₁) : (m₁ ∩ m₂).getD k fallback = fallback

theorem Std.ExtHashSet.get!_inter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default

theorem Std.ExtHashSet.get!_inter_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (mem : k ∈ m₂) : (m₁ ∩ m₂).get! k = m₁.get! k

theorem Std.ExtHashSet.get!_inter_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (not_mem : ¬k ∈ m₂) : (m₁ ∩ m₂).get! k = default

theorem Std.ExtHashSet.get!_inter_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (not_mem : ¬k ∈ m₁) : (m₁ ∩ m₂).get! k = default

theorem Std.ExtHashSet.size_inter_le_size_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ ∩ m₂).size ≤ m₁.size

theorem Std.ExtHashSet.size_inter_le_size_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ ∩ m₂).size ≤ m₂.size

theorem Std.ExtHashSet.size_inter_eq_size_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : (m₁ ∩ m₂).size = m₁.size

theorem Std.ExtHashSet.size_inter_eq_size_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : (m₁ ∩ m₂).size = m₂.size

theorem Std.ExtHashSet.size_add_size_eq_size_union_add_size_inter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size

@[simp]

theorem Std.ExtHashSet.isEmpty_inter_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty = true) : (m₁ ∩ m₂).isEmpty = true

@[simp]

theorem Std.ExtHashSet.isEmpty_inter_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] (h : m₂.isEmpty = true) : (m₁ ∩ m₂).isEmpty = true

theorem Std.ExtHashSet.isEmpty_inter_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ ∩ m₂).isEmpty = true ↔ ∀ (k : α), k ∈ m₁ → ¬k ∈ m₂

theorem Std.ExtHashSet.isEmpty_inter_comm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ ∩ m₂).isEmpty = (m₂ ∩ m₁).isEmpty

theorem Std.ExtHashSet.inter_eq_empty_comm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m₁ ∩ m₂ = ∅ ↔ m₂ ∩ m₁ = ∅

@[simp]

theorem Std.ExtHashSet.diff_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : m₁.diff m₂ = m₁ \ m₂

@[simp]

theorem Std.ExtHashSet.contains_diff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)

@[simp]

theorem Std.ExtHashSet.mem_diff_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ ¬k ∈ m₂

theorem Std.ExtHashSet.not_mem_diff_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₁) : ¬k ∈ m₁ \ m₂

theorem Std.ExtHashSet.not_mem_diff_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (mem : k ∈ m₂) : ¬k ∈ m₁ \ m₂

theorem Std.ExtHashSet.get?_diff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k

theorem Std.ExtHashSet.get?_diff_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₂) : (m₁ \ m₂).get? k = m₁.get? k

theorem Std.ExtHashSet.get?_diff_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (not_mem : ¬k ∈ m₁) : (m₁ \ m₂).get? k = none

theorem Std.ExtHashSet.get?_diff_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (mem : k ∈ m₂) : (m₁ \ m₂).get? k = none

@[simp]

theorem Std.ExtHashSet.get_diff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂} : (m₁ \ m₂).get k h_mem = m₁.get k ⋯

theorem Std.ExtHashSet.getD_diff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} : (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback

theorem Std.ExtHashSet.getD_diff_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (not_mem : ¬k ∈ m₂) : (m₁ \ m₂).getD k fallback = m₁.getD k fallback

theorem Std.ExtHashSet.getD_diff_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (mem : k ∈ m₂) : (m₁ \ m₂).getD k fallback = fallback

theorem Std.ExtHashSet.getD_diff_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (not_mem : ¬k ∈ m₁) : (m₁ \ m₂).getD k fallback = fallback

theorem Std.ExtHashSet.get!_diff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k

theorem Std.ExtHashSet.get!_diff_of_not_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (not_mem : ¬k ∈ m₂) : (m₁ \ m₂).get! k = m₁.get! k

theorem Std.ExtHashSet.get!_diff_of_mem_right {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (mem : k ∈ m₂) : (m₁ \ m₂).get! k = default

theorem Std.ExtHashSet.get!_diff_of_not_mem_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (not_mem : ¬k ∈ m₁) : (m₁ \ m₂).get! k = default

theorem Std.ExtHashSet.size_diff_le_size_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ \ m₂).size ≤ m₁.size

theorem Std.ExtHashSet.size_diff_eq_size_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] (h : ∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) : (m₁ \ m₂).size = m₁.size

theorem Std.ExtHashSet.size_diff_add_size_inter_eq_size_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size

@[simp]

theorem Std.ExtHashSet.isEmpty_diff_left {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty = true) : (m₁ \ m₂).isEmpty = true

theorem Std.ExtHashSet.isEmpty_diff_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : ExtHashSet α} [EquivBEq α] [LawfulHashable α] : (m₁ \ m₂).isEmpty = true ↔ ∀ (k : α), k ∈ m₁ → k ∈ m₂