mathlib3

2258b40d - chore(analysis/inner_product_space/basic): golf proofs (#18043)