Simple calculation

Stream: new members

[Emiel Lanckriet]

Have shown the following equality:

example {a b : ℝ} : b ≠ 0 → a = b * (a / b) :=
begin
    rw mul_div_comm,
    intro h,
    rw div_self h,
    ring,
end

However, I feel like there have to be shorter ways of doing this using some tactic, because this looks trivial. Does anyone have any advice?

[Mario Carneiro]

example {a b : ℝ} (h : b ≠ 0) : a = b * (a / b) := (mul_div_cancel' _ h).symm

[Rob Lewis]

Or tactically intro h, field_simp [h], ring

[Mario Carneiro]

library_search also finds my proof

[Emiel Lanckriet]

Thank you, I tried library_search, but apparently it gives no suggestion when I don't use intro first, that's why I missed it. The tactics are also very usefull.