proving identity

Stream: new members

[Shi You]

Hi. I am new to Lean. I found that by ring is a powerful tactic to check the correctness of an algebraic identity defined in a polynomial ring. However, I cannot find a tactic to prove identities in field of fractions.(something like x / y + y / x = (x^2 + y^2) / (x * y)). I don't know if there is a similar tool.

[Eric Wieser]

Have you tried proving it manually guys rewrites?

[Rémy Degenne]

the field_simp tactic could be useful. See https://leanprover-community.github.io/mathlib_docs/tactics.html#field_simp where the following example is given:

example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
  a + b / x + c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) :=
begin
  field_simp,
  ring
end