suppress an hyptohesis

Stream: Is there code for X?

[Filippo A. E. Nuccio]

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?

[Johan Commelin]

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

[Johan Commelin]

You could replace the hxs with rfl if you want.

[Filippo A. E. Nuccio]

But this instead of the apply lemma_blabla?

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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

[Mario Carneiro]

yes

[Filippo A. E. Nuccio]

Ok, thanks!

[Johan Commelin]

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.

[Filippo A. E. Nuccio]

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...)?

[Johan Commelin]

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

[Johan Commelin]

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