Lean bug

Stream: general

[Sebastien Gouezel]

While doing the gsmul refactor, I encountered a completely mysterious behavior in one file (may I say bug here?). I worked around it, but now that everything is merged people may have a look for fun. On current master, open the file measure_theory/arithmetic.lean, and go to line 311. Replace this line

  { exact has_measurable_gpow_aux G }

with its proof

  { assume k,
    simp_rw [gpow_neg_succ_of_nat],
    exact (measurable_id.pow_const (k + 1)).inv }

It fails. The line simp_rw is not doing its job: it doesn't change anything. You can repeat this line as many times as you want, they don't fail, but they don't change the goal. Whatever I tried, I wasn't able to close this goal without using an auxiliary lemma. I guess something is messed up with the tactic state at this point, but I can't tell what (nothing looks suspicious even with pp.all).