mathlib

48a36046 - feat(logic/nontrivial): a tactic to summon nontrivial instances (#4374)

feat(logic/nontrivial): a tactic to summon nontrivial instances (#4374) ``` Given a goal `a = b` or `a ≤ b` in a type `α`, generates an additional hypothesis `nontrivial α` (as otherwise `α` is a subsingleton and the goal is trivial). Alternatively, given a hypothesis `a ≠ b` or `a < b` in a type `α`, tries to generate a `nontrivial α` hypothesis from existing hypotheses using `nontrivial_of_ne` and `nontrivial_of_lt`. ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>