2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1

Stream: new members

[Julian Berman]

What tactic can prove 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1 for me? hint is suggesting ring, but when I use it lean says it didn't make progress.

[Alex J. Best]

The most tactical proof I can find is

example (d : ℕ) : 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1 :=
begin
  zify [nat.one_le_pow'],
  change d.succ with d + 1,
  ring_exp,
end

[Alex J. Best]

The problem, as always :smile:, is nat subtraction so we need some user input to find the lemma one_le_pow' here I guess.

[Julian Berman]

hm, thanks, I found both zify and ring_exp but figured there'd be something more sledgehammery

[Alex J. Best]

I just made #5157 because i noticed ring works as a finisher here without the middle line, but ring_exp doesnt

example (d : ℕ) : 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1 :=
begin
zify [nat.one_le_pow'],
ring,
end

[Alex J. Best]

Maybe @Anne Baanen has some ideas :smile:?

[Anne Baanen]

Created #5166 to rewrite nat.succ d to d + 1 automatically, thanks for reporting! :grinning_face_with_smiling_eyes: