tactics to prove an equality of reals

Stream: Is there code for X?

[Rémy Degenne]

I had to prove this goal, and I proved it in the very manual way you see below because I failed to use more advanced tactics.

import data.real.basic -- this is a minimal import, but feel free to import anything else you like

example (n : ℕ) (c ε : ℝ) :
  -(↑n.succ * ε) ^ 2 / (2 * c * ↑n.succ) = -↑n.succ * ε ^ 2 / (2 * c) :=
begin
  rw [mul_pow, pow_two, mul_assoc, mul_comm, ← neg_mul, ← neg_mul, ← mul_div,
    mul_comm ((2 : ℝ) * c), div_eq_mul_inv, inv_mul', mul_div, mul_inv_cancel, mul_div, mul_one],
  exact (nat.cast_pos.mpr n.succ_pos).ne',
end

I tried to throw various tactics at it, like simp, ring, field_simp, norm_num. They all failed to make meaningful progress. Do we have another tool I did not think about, that would have helped here?

[Alex J. Best]

A somewhat principled way to go for such goals is to use field_simp and then ring (or linarith), unfortunately field_simp needs a bit of help

import data.real.basic -- this is a minimal import, but feel free to import anything else you like

example (n : ℕ) (c ε : ℝ) :
  -(↑n.succ * ε) ^ 2 / (2 * c * ↑n.succ) = -↑n.succ * ε ^ 2 / (2 * c) :=
begin
  by_cases hc : c = 0,
  { simp [hc], },
  field_simp [n.cast_add_one_ne_zero],
  ring,
end

[Rémy Degenne]

Thanks! I knew about the general idea of field_simp then ring, but I did not inspect very much the result of that to see what went wrong. I will keep in mind that telling field_simp that some things are not zero can help.