cont_diff): add missing lemmas and golfs (#17233)

Commit

3 years ago

chore(analysis/calculus/cont_diff): add missing lemmas and golfs (#17233) Adds two trivial lemmas. Moreover, we golf a few proofs and remove non-terminal simps.

Author

mcdoll

Parents

ae714fd5

mathlib 2423ed87 - chore(analysis/calculus/cont_diff): add missing lemmas and golfs (#17233)

mathlib
2423ed87 - chore(analysis/calculus/cont_diff): add missing lemmas and golfs (#17233)