Loogle!

Result

Found 117 declarations mentioning Finmap.

• Finmap 📋 Mathlib.Data.Finmap
  {α : Type u} (β : α → Type v) : Type (max u v)
• Finmap.instEmptyCollection 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} : EmptyCollection (Finmap β)
• Finmap.instInhabited 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} : Inhabited (Finmap β)
• Finmap.instMembership 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} : Membership α (Finmap β)
• Finmap.keys 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (s : Finmap β) : Finset α
• AList.toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (s : AList β) : Finmap β
• Finmap.instSDiff 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] : SDiff (Finmap β)
• Finmap.instUnion 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] : Union (Finmap β)
• Finmap.singleton 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (a : α) (b : β a) : Finmap β
• Finmap.Disjoint 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (s₁ s₂ : Finmap β) : Prop
• Finmap.entries 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (self : Finmap β) : Multiset (Sigma β)
• Finmap.all 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (f : (x : α) → β x → Bool) (s : Finmap β) : Bool
• Finmap.any 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (f : (x : α) → β x → Bool) (s : Finmap β) : Bool
• Finmap.erase 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap β
• Finmap.lookup 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Option (β a)
• List.toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s : List (Sigma β)) : Finmap β
• Finmap.decidableEq 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] [(a : α) → DecidableEq (β a)] : DecidableEq (Finmap β)
• Finmap.nodupKeys 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (self : Finmap β) : self.entries.NodupKeys
• Finmap.insert 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) : Finmap β
• Finmap.mk 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (entries : Multiset (Sigma β)) (nodupKeys : entries.NodupKeys) : Finmap β
• Finmap.nodup_entries 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (f : Finmap β) : f.entries.Nodup
• Finmap.replace 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) : Finmap β
• Finmap.sdiff 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s s' : Finmap β) : Finmap β
• Finmap.union 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s₁ s₂ : Finmap β) : Finmap β
• Finmap.instDecidableRelDisjoint 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] : DecidableRel Finmap.Disjoint
• Finmap.extract 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Option (β a) × Finmap β
• Finmap.disjoint_empty 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (x : Finmap β) : ∅.Disjoint x
• Finmap.Disjoint.symm 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (x y : Finmap β) (h : x.Disjoint y) : y.Disjoint x
• Finmap.induction_on 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {C : Finmap β → Prop} (s : Finmap β) (H : ∀ (a : AList β), C a.toFinmap) : C s
• Finmap.instDecidableMem 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Decidable (a ∈ s)
• Finmap.Disjoint.symm_iff 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (x y : Finmap β) : x.Disjoint y ↔ y.Disjoint x
• Finmap.keys_empty 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} : ∅.keys = ∅
• Finmap.notMem_empty 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {a : α} : a ∉ ∅
• Finmap.singleton.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (a : α) (b : β a) : Finmap.singleton a b = (AList.singleton a b).toFinmap
• Finmap.empty_toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} : ∅.toFinmap = ∅
• Finmap.toFinmap_nil 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] : [].toFinmap = ∅
• Finmap.lookup_empty 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) : Finmap.lookup a ∅ = none
• Finmap.notMem_erase_self 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : a ∉ Finmap.erase a s
• Finmap.mem_singleton 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (x y : α) (b : β y) : x ∈ Finmap.singleton y b ↔ x = y
• Finmap.keys.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (s : Finmap β) : s.keys = { val := s.entries.keys, nodup := ⋯ }
• List.toFinmap.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s : List (Sigma β)) : s.toFinmap = s.toAList.toFinmap
• Finmap.lookup_erase 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap.lookup a (Finmap.erase a s) = none
• Finmap.ext 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {s t : Finmap β} : s.entries = t.entries → s = t
• Finmap.keys_replace 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) : (Finmap.replace a b s).keys = s.keys
• Finmap.empty_union 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} : ∅ ∪ s₁ = s₁
• Finmap.ext_iff 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {s t : Finmap β} : s = t ↔ s.entries = t.entries
• Finmap.ext_iff' 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {s t : Finmap β} : s.entries = t.entries ↔ s = t
• Finmap.keys_erase 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : (Finmap.erase a s).keys = s.keys.erase a
• Finmap.mem_keys 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {a : α} {s : Finmap β} : a ∈ s.keys ↔ a ∈ s
• Finmap.union_empty 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} : s₁ ∪ ∅ = s₁
• AList.toFinmap.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (s : AList β) : s.toFinmap = { entries := ↑s.entries, nodupKeys := ⋯ }
• Finmap.insert_singleton_eq 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b b' : β a} : Finmap.insert a b (Finmap.singleton a b') = Finmap.singleton a b
• Finmap.erase_toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : Finmap.erase a s.toFinmap = (AList.erase a s).toFinmap
• Finmap.lookup_insert 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} (s : Finmap β) : Finmap.lookup a (Finmap.insert a b s) = some b
• Finmap.mem_toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {a : α} {s : AList β} : a ∈ s.toFinmap ↔ a ∈ s
• Finmap.lookup_isSome 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : (Finmap.lookup a s).isSome = true ↔ a ∈ s
• Finmap.mem_def 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {a : α} {s : Finmap β} : a ∈ s ↔ a ∈ s.entries.keys
• AList.toFinmap_eq 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {s₁ s₂ : AList β} : s₁.toFinmap = s₂.toFinmap ↔ s₁.entries.Perm s₂.entries
• Finmap.ext_lookup 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ s₂ : Finmap β} : (∀ (x : α), Finmap.lookup x s₁ = Finmap.lookup x s₂) → s₁ = s₂
• Finmap.induction_on₂ 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {C : Finmap β → Finmap β → Prop} (s₁ s₂ : Finmap β) (H : ∀ (a₁ a₂ : AList β), C a₁.toFinmap a₂.toFinmap) : C s₁ s₂
• Finmap.lookup_eq_none 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : Finmap.lookup a s = none ↔ a ∉ s
• Finmap.insert_toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : AList β) : Finmap.insert a b s.toFinmap = (AList.insert a b s).toFinmap
• Finmap.lookup_erase_ne 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {s : Finmap β} (h : a ≠ a') : Finmap.lookup a (Finmap.erase a' s) = Finmap.lookup a s
• Finmap.mem_of_lookup_eq_some 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} (h : Finmap.lookup a s = some b) : a ∈ s
• Finmap.replace_toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : AList β) : Finmap.replace a b s.toFinmap = (AList.replace a b s).toFinmap
• Finmap.erase_erase 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {s : Finmap β} : Finmap.erase a (Finmap.erase a' s) = Finmap.erase a' (Finmap.erase a s)
• Finmap.liftOn 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {γ : Type u_1} (s : Finmap β) (f : AList β → γ) (H : ∀ (a b : AList β), a.entries.Perm b.entries → f a = f b) : γ
• Finmap.lookup.congr_simp 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {inst✝ : DecidableEq α} [DecidableEq α] (a : α) (s s✝ : Finmap β) (e_s : s = s✝) : Finmap.lookup a s = Finmap.lookup a s✝
• Finmap.foldl 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {δ : Type w} (f : δ → (a : α) → β a → δ) (H : ∀ (d : δ) (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂), f (f d a₁ b₁) a₂ b₂ = f (f d a₂ b₂) a₁ b₁) (d : δ) (m : Finmap β) : δ
• Finmap.insert_insert 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b b' : β a} (s : Finmap β) : Finmap.insert a b' (Finmap.insert a b s) = Finmap.insert a b' s
• Finmap.lookup_insert_of_ne 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {b : β a} (s : Finmap β) (h : a' ≠ a) : Finmap.lookup a' (Finmap.insert a b s) = Finmap.lookup a' s
• Finmap.Disjoint.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (s₁ s₂ : Finmap β) : s₁.Disjoint s₂ = ∀ x ∈ s₁, x ∉ s₂
• Finmap.mem_iff 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : a ∈ s ↔ ∃ b, Finmap.lookup a s = some b
• Finmap.mem_replace 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {b : β a} {s : Finmap β} : a' ∈ Finmap.replace a b s ↔ a' ∈ s
• Finmap.disjoint_union_left 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (x y z : Finmap β) : (x ∪ y).Disjoint z ↔ x.Disjoint z ∧ y.Disjoint z
• Finmap.disjoint_union_right 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (x y z : Finmap β) : x.Disjoint (y ∪ z) ↔ x.Disjoint y ∧ x.Disjoint z
• Finmap.union_comm_of_disjoint 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ s₂ : Finmap β} : s₁.Disjoint s₂ → s₁ ∪ s₂ = s₂ ∪ s₁
• Finmap.keys_union 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ s₂ : Finmap β} : (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys
• Finmap.mem_erase 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {s : Finmap β} : a' ∈ Finmap.erase a s ↔ a' ≠ a ∧ a' ∈ s
• Finmap.toFinmap_cons 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)) : (⟨a, b⟩ :: xs).toFinmap = Finmap.insert a b xs.toFinmap
• Finmap.extract_eq_lookup_erase 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap.extract a s = (Finmap.lookup a s, Finmap.erase a s)
• Finmap.mk.injEq 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (entries : Multiset (Sigma β)) (nodupKeys : entries.NodupKeys) (entries✝ : Multiset (Sigma β)) (nodupKeys✝ : entries✝.NodupKeys) : ({ entries := entries, nodupKeys := nodupKeys } = { entries := entries✝, nodupKeys := nodupKeys✝ }) = (entries = entries✝)
• Finmap.erase.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap.erase a s = s.liftOn (fun t => (AList.erase a t).toFinmap) ⋯
• Finmap.mem_insert 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {b' : β a'} {s : Finmap β} : a ∈ Finmap.insert a' b' s ↔ a = a' ∨ a ∈ s
• Finmap.union_toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s₁ s₂ : AList β) : s₁.toFinmap ∪ s₂.toFinmap = (s₁ ∪ s₂).toFinmap
• Finmap.sigma_keys_lookup 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s : Finmap β) : (s.keys.sigma fun i => (Finmap.lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }
• Finmap.lookup_eq_some_iff 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s : Finmap β} {a : α} {b : β a} : Finmap.lookup a s = some b ↔ ⟨a, b⟩ ∈ s.entries
• Finmap.lookup_union_left 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} : a ∈ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁
• Finmap.induction_on₃ 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {C : Finmap β → Finmap β → Finmap β → Prop} (s₁ s₂ s₃ : Finmap β) (H : ∀ (a₁ a₂ a₃ : AList β), C a₁.toFinmap a₂.toFinmap a₃.toFinmap) : C s₁ s₂ s₃
• Finmap.insert_insert_of_ne 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {b : β a} {b' : β a'} (s : Finmap β) (h : a ≠ a') : Finmap.insert a' b' (Finmap.insert a b s) = Finmap.insert a b (Finmap.insert a' b' s)
• Finmap.lookup_union_left_of_not_in 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} (h : a ∉ s₂) : Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁
• Finmap.lookup_union_right 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} : a ∉ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₂
• Finmap.mem_list_toFinmap 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (xs : List (Sigma β)) : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
• Finmap.insert.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) : Finmap.insert a b s = s.liftOn (fun t => (AList.insert a b t).toFinmap) ⋯
• Finmap.replace.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) : Finmap.replace a b s = s.liftOn (fun t => (AList.replace a b t).toFinmap) ⋯
• Finmap.erase_union_singleton 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) (h : Finmap.lookup a s = some b) : Finmap.erase a s ∪ Finmap.singleton a b = s
• Finmap.mem_lookup_iff 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s : Finmap β} {a : α} {b : β a} : b ∈ Finmap.lookup a s ↔ ⟨a, b⟩ ∈ s.entries
• Finmap.entries_insert_of_notMem 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} : a ∉ s → (Finmap.insert a b s).entries = ⟨a, b⟩ ::ₘ s.entries
• Finmap.insert_union 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β} : Finmap.insert a b (s₁ ∪ s₂) = Finmap.insert a b s₁ ∪ s₂
• Finmap.mk.congr_simp 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} (entries entries✝ : Multiset (Sigma β)) (e_entries : entries = entries✝) (nodupKeys : entries.NodupKeys) : { entries := entries, nodupKeys := nodupKeys } = { entries := entries✝, nodupKeys := ⋯ }
• Finmap.union.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s₁ s₂ : Finmap β) : s₁.union s₂ = s₁.liftOn₂ s₂ (fun s₁ s₂ => (s₁ ∪ s₂).toFinmap) ⋯
• Finmap.mem_union 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂
• Finmap.union_cancel 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ s₂ s₃ : Finmap β} (h : s₁.Disjoint s₃) (h' : s₂.Disjoint s₃) : s₁ ∪ s₃ = s₂ ∪ s₃ ↔ s₁ = s₂
• Finmap.keysLookupEquiv 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] : Finmap β ≃ { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
• Finmap.union_assoc 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ s₂ s₃ : Finmap β} : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)
• Finmap.liftOn₂ 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {γ : Type u_1} (s₁ s₂ : Finmap β) (f : AList β → AList β → γ) (H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries.Perm a₂.entries → b₁.entries.Perm b₂.entries → f a₁ b₁ = f a₂ b₂) : γ
• Finmap.mk.sizeOf_spec 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [SizeOf α] [(a : α) → SizeOf (β a)] (entries : Multiset (Sigma β)) (nodupKeys : entries.NodupKeys) : sizeOf { entries := entries, nodupKeys := nodupKeys } = 1 + sizeOf entries + sizeOf nodupKeys
• Finmap.mem_lookup_union' 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β} : Finmap.lookup a (s₁ ∪ s₂) = some b ↔ b ∈ Finmap.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ Finmap.lookup a s₂
• Finmap.mem_lookup_union 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β} : b ∈ Finmap.lookup a (s₁ ∪ s₂) ↔ b ∈ Finmap.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ Finmap.lookup a s₂
• Finmap.mem_lookup_union_middle 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ s₃ : Finmap β} : b ∈ Finmap.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ Finmap.lookup a (s₁ ∪ s₂ ∪ s₃)
• Finmap.extract.eq_1 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap.extract a s = s.liftOn (fun t => Prod.map id AList.toFinmap (AList.extract a t)) ⋯
• Finmap.liftOn.congr_simp 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {γ : Type u_1} (s s✝ : Finmap β) (e_s : s = s✝) (f f✝ : AList β → γ) (e_f : f = f✝) (H : ∀ (a b : AList β), a.entries.Perm b.entries → f a = f b) : s.liftOn f H = s✝.liftOn f✝ ⋯
• Finmap.liftOn₂.congr_simp 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} {γ : Type u_1} (s₁ s₁✝ : Finmap β) (e_s₁ : s₁ = s₁✝) (s₂ s₂✝ : Finmap β) (e_s₂ : s₂ = s₂✝) (f f✝ : AList β → AList β → γ) (e_f : f = f✝) (H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries.Perm a₂.entries → b₁.entries.Perm b₂.entries → f a₁ b₁ = f a₂ b₂) : s₁.liftOn₂ s₂ f H = s₁✝.liftOn₂ s₂✝ f✝ ⋯
• Finmap.keysLookupEquiv_apply_coe_fst 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s : Finmap β) : (↑(Finmap.keysLookupEquiv s)).1 = s.keys
• Finmap.keysLookupEquiv_apply_coe_snd 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (s : Finmap β) (i : α) : (↑(Finmap.keysLookupEquiv s)).2 i = Finmap.lookup i s
• Finmap.keysLookupEquiv_symm_apply_keys 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) : (Finmap.keysLookupEquiv.symm f).keys = (↑f).1
• Finmap.keysLookupEquiv_symm_apply_lookup 📋 Mathlib.Data.Finmap
  {α : Type u} {β : α → Type v} [DecidableEq α] (f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) (a : α) : Finmap.lookup a (Finmap.keysLookupEquiv.symm f) = (↑f).2 a

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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 abad10c