ring failure

Stream: mathlib4

[Patrick Massot]

The whole file https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group_power/identities.lean is beyond the reach of our current mathlib4 ring tactic.

[Alex J. Best]

see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/status.20of.20.60ring.60/near/303965507

[Yaël Dillies]

Here is an example of ring failing on a simple goal which should be within its reach. This is a real example from APAP:

import Mathlib

example {m : ℕ} : (2 : ℝ) ^ (m * 2) * 8 ^ m = 32 ^ m := by ring

[Yaël Dillies]

(whoops, that thread already existed :graveyard:)

[Eric Wieser]

This doesn't look in scope for ring to me

[Eric Wieser]

Here's a perhaps more minimal example:

example {m : ℕ} : 2 ^ (m * 2) * 2 ^ (m * 3) = (2 ^ 5) ^ m := by
  ring_nf

[Sébastien Gouëzel]

There is rpow_ring in PFR that is extremely helpful in this kind of situation...

[Yaël Dillies]

Here is an even more minimal example that shows that it should be in scope for ring:

import Mathlib

example {m : ℕ} : (2 : ℝ) ^ m * 3 ^ m = (2 * 3) ^ m := by ring

[Yaël Dillies]

The issue is that ring simplifies numerals under a single power, but doesn't combine numerals outside different powers

[Yaël Dillies]

If it didn't do the former or did do the latter, then my example would work