swapping things in a lemma

Stream: new members

[Lawrence Lin]

in an earlier thread i wrote,

import tactic
import geom_sum

example (a : ℤ) (m n : ℕ) : ↑(int.gcd (a^m - 1) (a^n - 1) : ℤ) = a^(nat.gcd m n) - 1 :=
begin
  rw mul_geom_sum a m,
end

but it spits out the error

rewrite tactic failed, did not find instance of the pattern in the target expression
  (a - 1) * geom_sum a m

would this be because in the docs we have

theorem mul_geom_sum {α : Type u} [ring α] (x : α) (n : ℕ) :
(x - 1) * (finset.range n).sum (λ (i : ℕ), x ^ i) = x ^ n - 1

and lean can't handle x^n - 1 turning into the other thing?

[Michael Stoll]

You can rewrite in the reverse direction via rw ← ... (type "\l" to get the arrow).

[Lawrence Lin]

thank you!