ring does not fully work inside exp

Stream: new members

[Eloi]

I have found that the ring tactic does not fully work inside exp. I see that it manages to do something so I wonder if it is possible to improve it to solve this kind of goals?

import data.complex.basic
import data.real.pi
open real
open complex


example (z t: ℂ): (2:ℂ ) * pi * I * (z+1) * t  = (2:ℂ ) * pi * I * t + 2 * pi * I * z * t:=
begin
  ring,
end

example (z t: ℂ): exp ( (2:ℂ ) * pi * I * (z+1) * t ) = exp ( (2:ℂ ) * pi * I * t + 2 * pi * I * z * t ):=
  begin
    ring,
   -- ⊢ exp ((2 * t * z + 2 * t) * I * ↑pi) = exp ((2 * z + 2) * t * I * ↑pi)
    sorry
  end

[Johan Commelin]

I think the easy answer is congr' 1, ring

[Johan Commelin]

The hard answer would explain why it doesn't work right away...

[Eloi]

thanks, for now it is enough

[Johan Commelin]

congr strips away as much as possible from two sides of an =. With congr' n you can tell it to take n steps in stripping things away

[Alex J. Best]

My guess is that ring picks different variable orderings when trying to normalize the LHS and RHS so they don't end up matching, does that sound plausible to a ring expert ?