mathlib

b1ab3107 - chore(analysis/normed_space/inner_product): add {bilin,sesq}_form_of_inner_apply simp lemmas (#5982)