Adding exponents of same base

Stream: new members

[Divya Ranjan]

I'm not able to get this simple exponent reduction in Lean4:
$a \cdot b^{x} \cdot b$ I need this to be $a \cdot b^{x+1}$. I have tried to convert $b$ to $b^{1}$ by pow_one and then try pow_add but for some reason this is not recognizing the pattern, probably because there's another multiplicand ($a$).

[Mario Carneiro]

try rewriting with mul_assoc first

[Divya Ranjan]

Mario Carneiro said:

try rewriting with mul_assoc first

It refuses to accept the pattern, the succ case is where I'm at:

import Mathlib

open Finset BigOperators
open Ring
open Real

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
  induction n with
  | zero =>
    nth_rw 1 [sum_range_one, pow_zero, mul_one]
    rw [zero_add, pow_one]
    nth_rw 3 [← mul_one a]
    rw [← mul_sub, ← mul_div, div_self]
    simp
    exact sub_ne_zero_of_ne h
  | succ n ih =>
    rw [sum_range_succ]
    rw [ih]
    rw [div_add']
    rw [mul_sub]
    field_simp
    nth_rw 2 [← rpow_one r]
    -- have hp := pow_add r (n+1) 1
    rw [mul_assoc]
    rw [← pow_add r (n+1) 1]
    sorry

[Mario Carneiro]

the previous rpow_one line is introducing an rpow in the expression where you need a pow to work with pow_add. Use pow_one instead

[Julian Berman]

Or get rid of everything after the field_simp and you can use rw [show a * r ^ (n + 1) * r - a = a * r ^ (n + 2) - a by ring]

[Julian Berman]

Why does field_simp not get a bit further there and try that itself, and then change the n + 1 + 1 to n + 2 on the RHS (or vice versa)?

[Divya Ranjan]

Mario Carneiro said:

the previous rpow_one line is introducing an rpow in the expression where you need a pow to work with pow_add. Use pow_one instead

Yep that was it.

[Mario Carneiro]

I think the use of field_simp is unnecessary here, you can just use congr 1 to clear divisions

[Julian Berman]

Ah, field_simp is really only supposed to be "clear denominators" right? Replacing field_simp entirely with ring seems to basically..

[Julian Berman]

Yeah

[Divya Ranjan]

Oh wait, I could do that?

[Divya Ranjan]

I thought if you have exponents unresolved

[Mario Carneiro]

ring knows how to handle x ^ (n+1) type expressions

[Divya Ranjan]

Ah

[Divya Ranjan]

That's tricky.

[Julian Berman]

import Mathlib

open Finset BigOperators
open Ring
open Real

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
  induction n with
  | zero =>
    nth_rw 1 [sum_range_one, pow_zero, mul_one]
    rw [zero_add, pow_one]
    nth_rw 3 [← mul_one a]
    rw [← mul_sub, ← mul_div, div_self]
    simp
    exact sub_ne_zero_of_ne h
  | succ n ih =>
    rw [sum_range_succ, ih, div_add']
    ring_nf
    exact sub_ne_zero_of_ne h

FWIW is what I ended up with.

[Divya Ranjan]

Yeah I was going to put the rewrites into one line

[Divya Ranjan]

Julian Berman said:

import Mathlib

open Finset BigOperators
open Ring
open Real

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
  induction n with
  | zero =>
    nth_rw 1 [sum_range_one, pow_zero, mul_one]
    rw [zero_add, pow_one]
    nth_rw 3 [← mul_one a]
    rw [← mul_sub, ← mul_div, div_self]
    simp
    exact sub_ne_zero_of_ne h
  | succ n ih =>
    rw [sum_range_succ, ih, div_add']
    ring_nf
    exact sub_ne_zero_of_ne h

FWIW is what I ended up with.

What does ring_nf do here, beyond ring?

[Julian Berman]

(I'm sure there's a more technical answer which the docstring probably says) but It's ring but you're allowed to use stuff after it (whereas ring is supposed to be the last line of your proof, and it seems it cannot do the \ne one part, though you could do that rewrite before and then ring will finish the proof)

[Julian Berman]

Oh, actually looking again it seems the ne one is a side goal.

[Mario Carneiro]

ring_nf is like a rewrite tactic

[Divya Ranjan]

Yeah one can do it after

Julian Berman said:

Oh, actually looking again it seems the ne one is a side goal.

Yeah one can do it after ring, as it seems.

[Mario Carneiro]

it normalizes subterms which are ring expressions instead of trying to prove the goal

[Mario Carneiro]

in this case I think you don't need it