Zulip Chat Archive

Stream: new members

Topic: Simple calculation


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 28 2020 at 12:33):

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

view this post on Zulip Rob Lewis (Jul 28 2020 at 12:34):

Or tactically intro h, field_simp [h], ring

view this post on Zulip Mario Carneiro (Jul 28 2020 at 12:34):

library_search also finds my proof

view this post on Zulip 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