mathlib3

7348f1b7 - Adding a matching TODO back (#10506)

Adding a matching TODO back (#10506) Because we were careless and removed it too early: https://github.com/leanprover-community/mathlib/pull/10210#discussion_r757640946