mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (terminationBy?? : Option Lean.Syntax) (terminationBy? : Option Lean.Elab.TerminationBy)
  (partialFixpoint? : Option Lean.Elab.PartialFixpoint) (decreasingBy? : Option Lean.Elab.DecreasingBy)
  (extraParams : ℕ),
  sizeOf
      { ref := ref, terminationBy?? := terminationBy??, terminationBy? := terminationBy?,
        partialFixpoint? := partialFixpoint?, decreasingBy? := decreasingBy?, extraParams := extraParams } =
    1 + sizeOf ref + sizeOf terminationBy?? + sizeOf terminationBy? + sizeOf partialFixpoint? + sizeOf decreasingBy? +
      sizeOf extraParams
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_filter_eq_size_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool},
  m.WF → ((Std.DHashMap.Raw.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = true)