`BookProof.ChapterF6.mgT_apply_le` (k : ℕ) (T : α →₀ ℕ) (s : List α) (y : α) : (mgT k T s) y ≤ T y + s.count y

Initializing...

`BookProof.ChapterF6.mgT_apply_le` (k : ℕ) (T : α →₀ ℕ) (s : List α) (y : α) : (mgT k T s) y ≤ T y + s.count y · Prove2Me