mathlib3

065a7081 - refactor(analysis/inner_product_space/projection): speedup proof (#9804)

refactor(analysis/inner_product_space/projection): speedup proof (#9804) Speed up slow proof that caused a timeout on another branch. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>