field_simp doesn't work as well in version 4.23 as it did in

Stream: new members

[张守信(Shouxin Zhang)]

An example is here.

example : (1 / 2 : ℝ) + 1 / 2 = 1 := by
  field_simp
  ring

In 4.16, it can be easily golf by one line field_simp, i.e. ring is unnecessary. Seems really strange, because I think that simp type tactic is always better in new lean version.

[Etienne Marion]

field_simp was recently rewritten (to not rely too much on simp I believe) and this is now expected I think.

[Etienne Marion]

The PR is #28658.