## Stream: general

### Topic: What happened next?

#### Kevin Buzzard (Apr 04 2018 at 19:50):

example (d : ℕ) (H : 1  =  2  * nat.succ d) : 1  =  2  * d +  2  :=
begin
rw H,
-- goal now?
end


#### Kevin Buzzard (Apr 04 2018 at 19:51):

Took me slightly by surprise at the time.

#### Mario Carneiro (Apr 04 2018 at 20:07):

heh, I assume 2 got rewritten?

#### Kevin Buzzard (Apr 04 2018 at 20:27):

That was part of it.

#### Kevin Buzzard (Apr 04 2018 at 20:29):

The other phenomenon shows itself here:

example (x y : ℕ) (H : 1 = x) : 2 = y :=
begin
rw H,
-- goal now?
end


#### Kevin Buzzard (Apr 04 2018 at 20:30):

Oh I have just realised what is going on.

#### Kevin Buzzard (Apr 04 2018 at 20:30):

So the goal becomes

#### Kevin Buzzard (Apr 04 2018 at 20:30):

 bit0 x = y

#### Kevin Buzzard (Apr 04 2018 at 20:31):

but that's because 2 isn't defined to be succ 1 here, it's defined to be bit0 1

Last updated: May 16 2021 at 22:14 UTC