mathlib3

2a732ed5 - chore(analysis/special_functions/log/basic): golf a proof (#14898)