Zulip Chat Archive

Stream: general

Topic: rw buglet (I think)


Kevin Buzzard (Apr 02 2018 at 13:56):

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

Kevin Buzzard (Apr 02 2018 at 13:56):

Then I do rw HTUih at HyT2

Kevin Buzzard (Apr 02 2018 at 13:56):

and I end up with 39 hypotheses

Kenny Lau (Apr 02 2018 at 13:56):

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

Kenny Lau (Apr 02 2018 at 13:57):

oh that isn't a bug

Kenny Lau (Apr 02 2018 at 13:57):

because that hypothesis can't be replaced

Kevin Buzzard (Apr 02 2018 at 13:57):

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

Kenny Lau (Apr 02 2018 at 13:57):

because it's being used by other things

Kenny Lau (Apr 02 2018 at 13:57):

so instead it creates another hypothesis

Kevin Buzzard (Apr 02 2018 at 13:57):

Oh I see...

Kevin Buzzard (Apr 02 2018 at 13:58):

...with the same name?

Kenny Lau (Apr 02 2018 at 13:58):

well what other name would it be

Kenny Lau (Apr 02 2018 at 13:58):

you can do dedup if you don't like it

Kevin Buzzard (Apr 02 2018 at 13:58):

revert HyT2,intro HyT

Kevin Buzzard (Apr 02 2018 at 13:59):

It could have called it a ;-)


Last updated: Dec 20 2023 at 11:08 UTC