mathlib

fee2dfaa - chore(analysis/calculus/fderiv): golf a lemma using new `nontriviality` (#4584)

chore(analysis/calculus/fderiv): golf a lemma using new `nontriviality` (#4584) Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>