rw not working when it obviously should

Stream: maths

[Mark Andrew Gerads]

In lemma ruesDiffRotationallySymmetric, I get an error when trying rw h6, just above the sorry.
Looking at the tactic state makes me wonder if this is a bug. Help appreciated.
image.png

import analysis.special_functions.trigonometric.basic
import analysis.special_functions.exponential
import analysis.special_functions.complex.log
import algebra.group_with_zero.defs
import algebra.big_operators.basic

open classical complex asymptotics real normed_space
open_locale classical big_operators nat

def ruesDiff (n : ℕ) (m : ℤ) : ℂ → ℂ := sorry

lemma ruesDiffTsumForm (n:ℕ) (m:ℤ) (z:ℂ) : ruesDiff n m z = tsum (λ (k:ℕ), if ((k:ℤ)+m)%n=0 then z ^ k / k.factorial else 0) :=
begin
  sorry,
end

instance : group ℂ := -- needed for zpow_add to work
begin
  exact multiplicative.group,
end

lemma ruesDiffRotationallySymmetric (n:ℕ) (h₀:0<n) (m:ℤ) (z rou:ℂ) (h₁:rou ^ n = 1) : ruesDiff n m (z * rou) = rou ^ -m * ruesDiff n m z :=
begin
  simp_rw ruesDiffTsumForm,
  rw tsum_mul_left.symm,
  {
    congr' 1,
    ext1,
    simp only [euclidean_domain.mod_eq_zero, zpow_neg, mul_ite, mul_zero],
    have h0 := classical.em (↑n ∣ ↑x + m),
    cases h0,
    {
      rw [if_pos h0,if_pos h0],
      rw mul_pow z rou x,
      have h1 : rou ^ x = (rou ^ m)⁻¹,
      {
        let k := (x:ℤ) + m,
        have h2 : (x:ℤ) + m = k,
        exact rfl,
        rw h2 at h0,
        clear_value k,
        obtain ⟨k1, rfl⟩ := h0,
        have h3 : rou ^ ((x:ℤ) + m) = 1,
        {
          rw h2,
          rw zpow_mul rou ↑n k1,
          have h4 : rou ^ (n:ℤ) = 1,
          {
            exact_mod_cast h₁,
          },
          rw h4,
          simp only [one_zpow],
        },
        have h5 := congr_arg (λ (z₀:ℂ),z₀*(rou ^ m)⁻¹) h3.symm,
        clear h3,
        simp only [one_mul] at h5,
        rw h5,
        clear h5,
        have h6 := zpow_add rou x m,
        -- rw h6, -- fails, but should work
        sorry,
      },
      rw h1,
      ring_nf,
    },
    {
      rw [if_neg h0,if_neg h0],
    },
  },
  exact topological_ring.mk,
  exact t2_5_space.t2_space,
end

[Johan Commelin]

@Mark Andrew Gerads If you click on those ↑ appearing in the goal and in h6 you should get little pop-ups.

[Johan Commelin]

Do they say the same thing?

[Ruben Van de Velde]

That instance looks like it will give you trouble, and probably exactly at this point

[Ruben Van de Velde]

Do you now have two multiplications on the complex numbers?

[Johan Commelin]

Ooh, that instance is certainly bad. ℂ is not a multiplicative group.

[Johan Commelin]

zpow_add isn't working for a reason. There's probably a lemma zpow_add₀ that can be used here.

[Ruben Van de Velde]

I'm guessing that zpow_add is false for 0^0

[Mark Andrew Gerads]

The pop-ups that usually say what type a chunk of code is (that show tiny 'copy' buttons) is not working.
Because zpow_add appears to work when it should not (before the rw attempt), does that mean randomly claiming the instance broke the consistency of Lean, and if so, what advice should I follow to avoid such errors in the future? I am wondering where exactly my bug is, and how to generalize it to similar sets of bugs so that I could avoid similar mistakes in the future.
How does

        have h6 := zpow_add rou x m,

not throw any error in the first place, unless the 'theorem' is correct?
Also, I noticed I was missing a noncomputable, but my problem persists.

[Kevin Buzzard]

The issue is that after defining the group C instance you have two different multiplications on C so you are in hell. You don't want to do that, whatever you think it "fixes".

[Kevin Buzzard]

(deleted)

[Johan Commelin]

What you did certainly doesn't amount to "breaking the consistency of Lean" in the literal sense.

[Johan Commelin]

I guess the confusing thing is that mathlib is very picky about notation. + and * are not treated as "arbitrary binary operations".

[Johan Commelin]

You told Lean, please treat ℂ as a group with multiplicative notation. And you told it to do that by turning all +s into * (when you set up that instance).

[Johan Commelin]

So now x * y is new notation for x + y.

[Johan Commelin]

Which is probably not what you intended.

[Johan Commelin]

And the lemma zpow_add is now a new way of saying n * (x + y) = n * x + n * y.

[Mark Andrew Gerads]

By focusing on the line,

        have h6 := zpow_add rou x m,

I discovered both up arrows were, as I suspected, Int.
I am interested in the possibility of a zpow_add₀ which does not need the instance.

[Johan Commelin]

Let's try: docs#zpow_add₀

[Johan Commelin]

https://leanprover-community.github.io/mathlib_docs/algebra/group_with_zero/power.html#zpow_add%E2%82%80

[Mark Andrew Gerads]

Thank you. That looks like it will solve my problem nicely.