chore(analysis/analytic/basic): golf (#12965)
chore(analysis/analytic/basic): golf (#12965)

Golf a 1-line proof, drop an unneeded assumption.





leanprover-community/mathlib,leanprover-community/mathlib