Zulip Chat Archive

Stream: Is there code for X?

Topic: suppress an hyptohesis


view this post on Zulip Filippo A. E. Nuccio (Sep 15 2020 at 07:52):

I am trying to prove that a certain element x in the field of fractions of a ring R actually comes from the ring, so it can be written f(x') for some x' in the ring R, where f is the localisation map. "Unfortunately" the element x' I can produce (=the lemma I am applying can produce) is not only in R but also in an ideal I < R and I am getting the following error
invalid apply tactic, failed to unify ∃ (x' : R), ⇑(localization_map.to_map f) x' = x with ∃ (x' : R) (H : x' ∈ I), ⇑(localization_map.to_map f) x' = x
I can circumvent the problem by creating some subgoal, but this looks weird: is there a tactic to "forget" a piece of information obtained by applying some lemma?

view this post on Zulip Johan Commelin (Sep 15 2020 at 07:55):

I think the easiest is obtain \<x, -, hx> := blabla, exact \<x, hx>

view this post on Zulip Johan Commelin (Sep 15 2020 at 07:55):

You could replace the hxs with rfl if you want.

view this post on Zulip Filippo A. E. Nuccio (Sep 15 2020 at 08:00):

But this instead of the apply lemma_blabla?

view this post on Zulip Johan Commelin (Sep 15 2020 at 08:02):

I guess you could also try to use exists_congr but I don't think it's worth it.

view this post on Zulip Filippo A. E. Nuccio (Sep 15 2020 at 08:03):

And the - in the middle of the obtain is really a dash?

view this post on Zulip Mario Carneiro (Sep 15 2020 at 08:04):

yes

view this post on Zulip Filippo A. E. Nuccio (Sep 15 2020 at 08:05):

Ok, thanks!

view this post on Zulip Johan Commelin (Sep 15 2020 at 08:24):

Filippo A. E. Nuccio said:

And the - in the middle of the obtain is really a dash?

It's the thing that throws away the hypothesis, like you wanted. It's been added to mathlib like 2 weeks ago.

view this post on Zulip Filippo A. E. Nuccio (Sep 15 2020 at 08:31):

ah, ok: thanks! In these cases, is there a "canonical" place where to look at for news and implementation instructions (like what the exact syntax is, etc...)?

view this post on Zulip Johan Commelin (Sep 15 2020 at 08:44):

I hope the docstring will tell you how to use it.

view this post on Zulip Johan Commelin (Sep 15 2020 at 08:44):

And for news... I think we don't have much besides the git commit log, and occasional announcements here on Zulip


Last updated: May 16 2021 at 05:21 UTC