Zulip Chat Archive

Stream: general

Topic: rw buglet (I think)


view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:56):

before : 38 hypotheses including HyT2 : y ∈ T and HTUih : T = Ui h

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:56):

Then I do rw HTUih at HyT2

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:56):

and I end up with 39 hypotheses

view this post on Zulip Kenny Lau (Apr 02 2018 at 13:56):

quite hard to confirm it if you don't have MWE

view this post on Zulip Kenny Lau (Apr 02 2018 at 13:57):

oh that isn't a bug

view this post on Zulip Kenny Lau (Apr 02 2018 at 13:57):

because that hypothesis can't be replaced

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:57):

including HyT2 : y ∈ T and HyT2 : y ∈ Ui h

view this post on Zulip Kenny Lau (Apr 02 2018 at 13:57):

because it's being used by other things

view this post on Zulip Kenny Lau (Apr 02 2018 at 13:57):

so instead it creates another hypothesis

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:57):

Oh I see...

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:58):

...with the same name?

view this post on Zulip Kenny Lau (Apr 02 2018 at 13:58):

well what other name would it be

view this post on Zulip Kenny Lau (Apr 02 2018 at 13:58):

you can do dedup if you don't like it

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:58):

revert HyT2,intro HyT

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 13:59):

It could have called it a ;-)


Last updated: May 11 2021 at 13:22 UTC