Stream: new members

Topic: Simple calculation

Emiel Lanckriet (Jul 28 2020 at 12:31):

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 (Jul 28 2020 at 12:33):

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


Rob Lewis (Jul 28 2020 at 12:34):

Or tactically intro h, field_simp [h], ring

Mario Carneiro (Jul 28 2020 at 12:34):

library_search also finds my proof

Emiel Lanckriet (Jul 28 2020 at 12:47):

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.

Last updated: May 14 2021 at 03:27 UTC