rw fails when combined?

Stream: general

[Aaron Bies]

I just came across this situation where combining two rewrites into one results in it failing to apply a rule.

Is this a bug or am I doing something wrong?

example (n : ℕ) (n_even : n % 2 = 0) : n = 2 * (n / 2) :=
begin
  --rw [nat.mul_div_cancel', nat.dvd_iff_mod_eq_zero, n_even],
  rw [nat.mul_div_cancel'],
  rw [nat.dvd_iff_mod_eq_zero, n_even],
end

[Eric Rodriguez]

The issue is that the first rw creates a subgoal, which can't then be rewritten. This doesn't look like it is the case, however, as it's then instantly solved by refl as rw tries refl afterwards, and only leaves you the goal that you were missing from mul_div_cancel'.

[Aaron Bies]

Ah, that explains it, thank you!