4574 better `nontriviality`

Stream: PR reviews

[Yury G. Kudryashov]

@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]

I really like it!

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

Or let me try...

[Heather Macbeth]

What about https://github.com/leanprover-community/mathlib/blob/73f119e04c35a4ab10eae68345472d78e5c4f6c7/src/analysis/normed_space/operator_norm.lean#L835 ?

[Heather Macbeth]

Maybe there's nothing that needs to be done there

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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?

[Yury G. Kudryashov]

E.g., in https://github.com/leanprover-community/mathlib/blob/952a407c2ea89c154d718aa1f92fd988f2b5d338/src/analysis/calculus/inverse.lean#L158

[Heather Macbeth]

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]

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

[Yury G. Kudryashov]

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