mathlib

ebd2b7f2 - feat(logic/nontrivial): make `nontriviality` work for more goals (#4574)

feat(logic/nontrivial): make `nontriviality` work for more goals (#4574) The goal is to make `nontriviality` work for the following goals: * [x] `nontriviality α` if the goal is `is_open s`, `s : set α`; * [x] `nontriviality E` if the goal is `is_O f g` or `is_o f g`, where `f : α → E`; * [x] `nontriviality R` if the goal is `linear_independent R _`; * [ ] `nontriviality R` if the goal is `is_O f g` or `is_o f g`, where `f : α → E`, `[semimodule R E]`; in this case `nontriviality` should add a local instance `semimodule.subsingleton R`. The last case was never needed in `mathlib`, and there is a workaround: run `nontriviality E`, then deduce `nontrivial R` from `nontrivial E`. Misc feature: * [x] make `nontriviality` accept an optional list of additional `simp` lemmas. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>