Commit 2020-10-18 01:46 ebd2b7f2

feat(logic/nontrivial): make nontriviality work for more goals (#4574) The goal is to make nontriviality work for the following goals:

• nontriviality α if the goal is is_open s, s : set α;
• nontriviality E if the goal is is_O f g or is_o f g, where f : α → E;
• 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:
• make nontriviality accept an optional list of additional simp lemmas.