Loogle!

Result

Found 1102 declarations whose name contains "hashset". Of these, 101 have a name containing "hashset" and "equiv".

Std.HashSet.Equiv 📋 Std.Data.HashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m₁ m₂ : Std.HashSet α) : Prop
Std.HashSet.Equiv.inner 📋 Std.Data.HashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} (self : m₁.Equiv m₂) : m₁.inner.Equiv m₂.inner
Std.HashSet.Equiv.mk 📋 Std.Data.HashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} (inner : m₁.inner.Equiv m₂.inner) : m₁.Equiv m₂
Std.HashSet.Raw.Equiv 📋 Std.Data.HashSet.Raw
{α : Type u} (m₁ m₂ : Std.HashSet.Raw α) : Prop
Std.HashSet.Raw.Equiv.inner 📋 Std.Data.HashSet.Raw
{α : Type u} {m₁ m₂ : Std.HashSet.Raw α} (self : m₁.Equiv m₂) : m₁.inner.Equiv m₂.inner
Std.HashSet.Raw.Equiv.mk 📋 Std.Data.HashSet.Raw
{α : Type u} {m₁ m₂ : Std.HashSet.Raw α} (inner : m₁.inner.Equiv m₂.inner) : m₁.Equiv m₂
Std.HashSet.Equiv.refl 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : m.Equiv m
Std.HashSet.Equiv.rfl 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} : m.Equiv m
Std.HashSet.Equiv.symm 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} : m₁.Equiv m₂ → m₂.Equiv m₁
Std.HashSet.Equiv.comm 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} : m₁.Equiv m₂ ↔ m₂.Equiv m₁
Std.HashSet.Equiv.instTrans 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} : Trans Std.HashSet.Equiv Std.HashSet.Equiv Std.HashSet.Equiv
Std.HashSet.Equiv.of_toList_perm 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} (h : m₁.toList.Perm m₂.toList) : m₁.Equiv m₂
Std.HashSet.Equiv.toList_perm 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} (h : m₁.Equiv m₂) : m₁.toList.Perm m₂.toList
Std.HashSet.Equiv.trans 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} : m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
Std.HashSet.emptyWithCapacity_equiv_iff_isEmpty 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {c : ℕ} : (Std.HashSet.emptyWithCapacity c).Equiv m ↔ m.isEmpty = true
Std.HashSet.equiv_emptyWithCapacity_iff_isEmpty 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {c : ℕ} : m.Equiv (Std.HashSet.emptyWithCapacity c) ↔ m.isEmpty = true
Std.HashSet.equiv_of_beq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α] (h : (m₁ == m₂) = true) : m₁.Equiv m₂
Std.HashSet.Equiv.congr_left 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} (h : m₁.Equiv m₂) : m₁.Equiv m₃ ↔ m₂.Equiv m₃
Std.HashSet.Equiv.congr_right 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} (h : m₁.Equiv m₂) : m₃.Equiv m₁ ↔ m₃.Equiv m₂
Std.HashSet.Equiv.filter 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} (f : α → Bool) (h : m₁.Equiv m₂) : (Std.HashSet.filter f m₁).Equiv (Std.HashSet.filter f m₂)
Std.HashSet.Equiv.of_forall_contains_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α] (h : ∀ (k : α), m₁.contains k = m₂.contains k) : m₁.Equiv m₂
Std.HashSet.Equiv.isEmpty_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (h : m₁.Equiv m₂) : m₁.isEmpty = m₂.isEmpty
Std.HashSet.Equiv.size_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (h : m₁.Equiv m₂) : m₁.size = m₂.size
Std.HashSet.empty_equiv_iff_isEmpty 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] : ∅.Equiv m ↔ m.isEmpty = true
Std.HashSet.equiv_empty_iff_isEmpty 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] : m.Equiv ∅ ↔ m.isEmpty = true
Std.HashSet.equiv_iff_toList_perm 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] : m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
Std.HashSet.Equiv.beq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (h : m₁.Equiv m₂) : (m₁ == m₂) = true
Std.HashSet.Equiv.contains_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : m₁.Equiv m₂) : m₁.contains k = m₂.contains k
Std.HashSet.Equiv.get?_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : m₁.Equiv m₂) : m₁.get? k = m₂.get? k
Std.HashSet.Equiv.of_forall_get?_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (h : ∀ (k : α), m₁.get? k = m₂.get? k) : m₁.Equiv m₂
Std.HashSet.Equiv.erase 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (k : α) (h : m₁.Equiv m₂) : (m₁.erase k).Equiv (m₂.erase k)
Std.HashSet.Equiv.insert 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (k : α) (h : m₁.Equiv m₂) : (m₁.insert k).Equiv (m₂.insert k)
Std.HashSet.Equiv.getD_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (h : m₁.Equiv m₂) : m₁.getD k fallback = m₂.getD k fallback
Std.HashSet.Equiv.get!_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (h : m₁.Equiv m₂) : m₁.get! k = m₂.get! k
Std.HashSet.Equiv.of_forall_mem_iff 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α] (h : ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) : m₁.Equiv m₂
Std.HashSet.Equiv.mem_iff 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : m₁.Equiv m₂) : k ∈ m₁ ↔ k ∈ m₂
Std.HashSet.filter_equiv_self_iff 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} : (Std.HashSet.filter f m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true
Std.HashSet.Equiv.diff_left 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv : m₁.Equiv m₂) : (m₁ \ m₃).Equiv (m₂ \ m₃)
Std.HashSet.Equiv.diff_right 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv : m₂.Equiv m₃) : (m₁ \ m₂).Equiv (m₁ \ m₃)
Std.HashSet.Equiv.inter_left 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv : m₁.Equiv m₂) : (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
Std.HashSet.Equiv.inter_right 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv : m₂.Equiv m₃) : (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
Std.HashSet.Equiv.union_left 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv : m₁.Equiv m₂) : (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
Std.HashSet.Equiv.union_right 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv : m₂.Equiv m₃) : (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
Std.HashSet.Equiv.beq_congr 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Std.HashSet α} (h₁ : m₁.Equiv m₃) (h₂ : m₂.Equiv m₄) : (m₁ == m₂) = (m₃ == m₄)
Std.HashSet.Equiv.diff_congr 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ m₄ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : (m₁ \ m₂).Equiv (m₃ \ m₄)
Std.HashSet.Equiv.inter_congr 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ m₄ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
Std.HashSet.Equiv.union_congr 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ m₃ m₄ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
Std.HashSet.Equiv.insertMany_list 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (l : List α) (h : m₁.Equiv m₂) : (m₁.insertMany l).Equiv (m₂.insertMany l)
Std.HashSet.Equiv.get_eq 📋 Std.Data.HashSet.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (hk : k ∈ m₁) (h : m₁.Equiv m₂) : m₁.get k hk = m₂.get k ⋯
Std.HashSet.Raw.Equiv.refl 📋 Std.Data.HashSet.RawLemmas
{α : Type u} (m : Std.HashSet.Raw α) : m.Equiv m
Std.HashSet.Raw.Equiv.rfl 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m : Std.HashSet.Raw α} : m.Equiv m
Std.HashSet.Raw.Equiv.symm 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m₁ m₂ : Std.HashSet.Raw α} : m₁.Equiv m₂ → m₂.Equiv m₁
Std.HashSet.Raw.Equiv.comm 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m₁ m₂ : Std.HashSet.Raw α} : m₁.Equiv m₂ ↔ m₂.Equiv m₁
Std.HashSet.Raw.Equiv.instTrans 📋 Std.Data.HashSet.RawLemmas
{α : Type u} : Trans Std.HashSet.Raw.Equiv Std.HashSet.Raw.Equiv Std.HashSet.Raw.Equiv
Std.HashSet.Raw.Equiv.of_toList_perm 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m₁ m₂ : Std.HashSet.Raw α} (h : m₁.toList.Perm m₂.toList) : m₁.Equiv m₂
Std.HashSet.Raw.Equiv.toList_perm 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m₁ m₂ : Std.HashSet.Raw α} (h : m₁.Equiv m₂) : m₁.toList.Perm m₂.toList
Std.HashSet.Raw.Equiv.trans 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m₁ m₂ m₃ : Std.HashSet.Raw α} : m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
Std.HashSet.Raw.Equiv.congr_left 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m₁ m₂ m₃ : Std.HashSet.Raw α} (h : m₁.Equiv m₂) : m₁.Equiv m₃ ↔ m₂.Equiv m₃
Std.HashSet.Raw.Equiv.congr_right 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m₁ m₂ m₃ : Std.HashSet.Raw α} (h : m₁.Equiv m₂) : m₃.Equiv m₁ ↔ m₃.Equiv m₂
Std.HashSet.Raw.equiv_iff_toList_perm 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] : m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
Std.HashSet.Raw.equiv_emptyWithCapacity_iff_isEmpty 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m : Std.HashSet.Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {c : ℕ} (h : m.WF) : m.Equiv (Std.HashSet.Raw.emptyWithCapacity c) ↔ m.isEmpty = true
Std.HashSet.Raw.equiv_empty_iff_isEmpty 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m : Std.HashSet.Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.Equiv ∅ ↔ m.isEmpty = true
Std.HashSet.Raw.equiv_of_beq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : (m₁ == m₂) = true) : m₁.Equiv m₂
Std.HashSet.Raw.Equiv.isEmpty_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.isEmpty = m₂.isEmpty
Std.HashSet.Raw.Equiv.size_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.size = m₂.size
Std.HashSet.Raw.Equiv.beq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.beq m₂ = true
Std.HashSet.Raw.Equiv.filter 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (f : α → Bool) (h : m₁.Equiv m₂) : (Std.HashSet.Raw.filter f m₁).Equiv (Std.HashSet.Raw.filter f m₂)
Std.HashSet.Raw.Equiv.of_forall_contains_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : ∀ (k : α), m₁.contains k = m₂.contains k) : m₁.Equiv m₂
Std.HashSet.Raw.Equiv.contains_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.contains k = m₂.contains k
Std.HashSet.Raw.Equiv.erase 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : α) (h : m₁.Equiv m₂) : (m₁.erase k).Equiv (m₂.erase k)
Std.HashSet.Raw.Equiv.insert 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : α) (h : m₁.Equiv m₂) : (m₁.insert k).Equiv (m₂.insert k)
Std.HashSet.Raw.Equiv.get?_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.get? k = m₂.get? k
Std.HashSet.Raw.Equiv.of_forall_get?_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : ∀ (k : α), m₁.get? k = m₂.get? k) : m₁.Equiv m₂
Std.HashSet.Raw.Equiv.getD_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k fallback : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.getD k fallback = m₂.getD k fallback
Std.HashSet.Raw.Equiv.of_forall_mem_iff 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) : m₁.Equiv m₂
Std.HashSet.Raw.Equiv.get!_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.get! k = m₂.get! k
Std.HashSet.Raw.Equiv.mem_iff 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : k ∈ m₁ ↔ k ∈ m₂
Std.HashSet.Raw.filter_equiv_self_iff 📋 Std.Data.HashSet.RawLemmas
{α : Type u} {m : Std.HashSet.Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} (h : m.WF) : (Std.HashSet.Raw.filter f m).Equiv m ↔ ∀ (a : α) (h : a ∈ m), f (m.get a h) = true
Std.HashSet.Raw.Equiv.diff_left 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) : (m₁ \ m₃).Equiv (m₂ \ m₃)
Std.HashSet.Raw.Equiv.diff_right 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) : (m₁ \ m₂).Equiv (m₁ \ m₃)
Std.HashSet.Raw.Equiv.inter_left 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) : (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
Std.HashSet.Raw.Equiv.inter_right 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) : (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
Std.HashSet.Raw.Equiv.union_left 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) : (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
Std.HashSet.Raw.Equiv.union_right 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) : (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
Std.HashSet.Raw.Equiv.beq_congr 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Std.HashSet.Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁.Equiv m₃) (w₂ : m₂.Equiv m₄) : (m₁ == m₂) = (m₃ == m₄)
Std.HashSet.Raw.Equiv.diff_congr 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ m₄ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : (m₁ \ m₂).Equiv (m₃ \ m₄)
Std.HashSet.Raw.Equiv.inter_congr 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ m₄ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
Std.HashSet.Raw.Equiv.union_congr 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ m₃ m₄ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
Std.HashSet.Raw.Equiv.insertMany_list 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (l : List α) (h : m₁.Equiv m₂) : (m₁.insertMany l).Equiv (m₂.insertMany l)
Std.HashSet.Raw.Equiv.get_eq 📋 Std.Data.HashSet.RawLemmas
{α : Type u} [BEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂) : m₁.get k hk = m₂.get k ⋯
Std.HashSet.instDecidableEquivOfLawfulBEq 📋 Std.Data.HashSet.DecidableEquiv
{α : Type u} [BEq α] [LawfulBEq α] [Hashable α] (m₁ m₂ : Std.HashSet α) : Decidable (m₁.Equiv m₂)
Std.ExtHashSet.instBEqOfEquivBEqOfLawfulHashable 📋 Std.Data.ExtHashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : BEq (Std.ExtHashSet α)
Std.ExtHashSet.instInterOfEquivBEqOfLawfulHashable 📋 Std.Data.ExtHashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Inter (Std.ExtHashSet α)
Std.ExtHashSet.instSDiffOfEquivBEqOfLawfulHashable 📋 Std.Data.ExtHashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : SDiff (Std.ExtHashSet α)
Std.ExtHashSet.instUnionOfEquivBEqOfLawfulHashable 📋 Std.Data.ExtHashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Union (Std.ExtHashSet α)
Std.ExtHashSet.instInsertOfEquivBEqOfLawfulHashable 📋 Std.Data.ExtHashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Insert α (Std.ExtHashSet α)
Std.ExtHashSet.instMembershipOfEquivBEqOfLawfulHashable 📋 Std.Data.ExtHashSet.Basic
{α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : Membership α (Std.ExtHashSet α)
Std.ExtHashSet.instSingletonOfEquivBEqOfLawfulHashable 📋 Std.Data.ExtHashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Singleton α (Std.ExtHashSet α)
Std.ExtHashSet.instBEqOfEquivBEqOfLawfulHashable.congr_simp 📋 Std.Data.ExtHashSet.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Std.ExtHashSet.instBEqOfEquivBEqOfLawfulHashable = Std.ExtHashSet.instBEqOfEquivBEqOfLawfulHashable
Std.ExtHashSet.instMembershipOfEquivBEqOfLawfulHashable.congr_simp 📋 Std.Data.ExtHashSet.Lemmas
{α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : Std.ExtHashSet.instMembershipOfEquivBEqOfLawfulHashable = Std.ExtHashSet.instMembershipOfEquivBEqOfLawfulHashable
Std.HashSet.Raw.instDecidableEquiv 📋 Std.Data.HashSet.RawDecidableEquiv
{α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Std.HashSet.Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁.Equiv m₂)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 76f94b4