## Stream: PR reviews

### Topic: 4574 better nontriviality

#### Yury G. Kudryashov (Oct 11 2020 at 22:02):

@Scott Morrison In #4574 I'm trying to make nontriviality tactic extensible. E.g., I want nontriviality α to work if the goal is is_open s, s : set α, and for some other goals.

#### Scott Morrison (Oct 11 2020 at 22:04):

I really like it!

#### Yury G. Kudryashov (Oct 11 2020 at 22:07):

I guess my meta code is suboptimal, feel free to improve it.

#### Yury G. Kudryashov (Oct 11 2020 at 22:08):

Here are a few things I don't know how to do:

• make it accept a list of additional simp lemmas;
• given nontriviality R, make it mark semimodule.subsingleton R as an instance.

#### Yury G. Kudryashov (Oct 11 2020 at 22:14):

One more idea: if we have [inhabited α], then add unique α instead of subsingleton α to the context.

#### Yury G. Kudryashov (Oct 11 2020 at 22:22):

And I can't make https://github.com/leanprover-community/mathlib/blob/extend-nontriviality/src/analysis/calculus/times_cont_diff.lean#L2375 work with nontriviality.

Or let me try...

#### Heather Macbeth (Oct 11 2020 at 22:27):

Maybe there's nothing that needs to be done there

#### Heather Macbeth (Oct 11 2020 at 22:28):

But that lemma could be deleted after your tactic comes in, is that the idea?

#### Yury G. Kudryashov (Oct 11 2020 at 22:29):

AFAIR, subsingleton E ∨ _ is used as a technical assumption in the proof of the inverse function theorem.

#### Heather Macbeth (Oct 11 2020 at 22:29):

And the lemma's uses, in places like https://github.com/leanprover-community/mathlib/blob/952a407c2ea89c154d718aa1f92fd988f2b5d338/src/analysis/calculus/inverse.lean#L379 , replaced by uses of the tactic?

#### Heather Macbeth (Oct 11 2020 at 22:30):

Snap ... but yes, I meant that in the the inverse function where this lemma is currently used, could you use an improved nontriviality instead?

#### Yury G. Kudryashov (Oct 11 2020 at 22:32):

I did not plan to refactor analysis/calculus/inverse.

#### Yury G. Kudryashov (Oct 11 2020 at 22:34):

And I don't see how can we get rid of this this assumption in the first part of the file.

Last updated: May 09 2021 at 12:14 UTC