Tactic for proving power multiplication equality

Stream: new members

[Anirudh Suresh]

import Mathlib

lemma t{a b j:ℕ}:2 * 2 ^ (a - 1 - b) = 2 ^ (j - b + 1) * 2 ^ (a - 1 - j):=by {

}

The lemma above seems somewhat straightforward intuitively but it is taking me a few lines of code to prove this. Is there any tactic or lemma that would help me prove trivial lemmas like this(multiplication resulting in showing the equality of powers) easily without having to inspect it too much?

[Arthur Adjedj]

This lemma looks to be wrong:

import Mathlib

lemma t{a b j:ℕ}:2 * 2 ^ (a - 1 - b) = 2 ^ (j - b + 1) * 2 ^ (a - 1 - j):=by
  plausible
/-===================
Found a counter-example!
a := 2
b := 0
j := 3
issue: 4 = 16 does not hold
(0 shrinks)
--------------------/

[Jakob von Raumer]

You probably need b < j < a or so

[Anirudh Suresh]

import Mathlib

lemma t{a b j:ℕ}(h1:b<j)(h2:j<a):2 * 2 ^ (a - 1 - b) = 2 ^ (j - b + 1) * 2 ^ (a - 1 - j):=by {

}

Fixed it.

[Jakob von Raumer]

  rw [← Nat.pow_add, ← Nat.pow_succ']
  congr
  omega

does the job, that doesn't need too much introspection except for "manually rewrite to one exponentiation on each side, then focus on exponents with congr, then let omega do the rest"

[Anirudh Suresh]

Thanks a lot!