Keefer Rowan (Jun 03 2020 at 12:56):
field_simp * to the somewhat complicated expression (where we have
(innerc y y).re \ne 0 in the local context):
((innerc y y).re)⁻¹ * ∥innerc x y∥ * (((innerc y y).re)⁻¹ * ∥innerc x y∥) * (innerc y y).re = ((innerc y y).re)⁻¹ * ∥innerc x y∥ * ∥innerc x y∥
leaves the almost solved goal:
(innerc x y).abs * (innerc x y).abs * (innerc y y).re * (innerc y y).re = (innerc x y).abs * (innerc x y).abs * ((innerc y y).re * (innerc y y).re)
A few call to
mul_assoc would solve the goal, but for some reason
field_simp doesn't finish it.
ring does the trick from here, but I'm wondering why
field_simp can't just finish it off.
Note that everything has type .
Sebastien Gouezel (Jun 03 2020 at 13:12):
The goal of
field_simp is to clear off denominators, so that
ring can finish it. So the standard invocation is really
field_simp [h], ring.
Bryan Gin-ge Chen (Jun 03 2020 at 13:15):
The fact that
field_simp should be used as preparation for
ring is mentioned in tactic#field_simp and the docstring, but maybe it needs more emphasis?
Keefer Rowan (Jun 03 2020 at 13:17):
@Bryan Gin-ge Chen Looking at it now, it's pretty well emphasized. I just didn't look at it well enough.
Yury G. Kudryashov (Jun 04 2020 at 04:20):
BTW, can we reassign
@[simp] tags so that
simp works as
Johan Commelin (Jun 04 2020 at 04:47):
I think we can, why not?
Last updated: May 10 2021 at 23:11 UTC