## Stream: new members

### Topic: mul_left_cancel

#### toc (Sep 03 2020 at 15:22):

So if I have

m n a : ℤ,
ha : a ≠ 0,
k : ℤ,
h : a * (m * k) = a * n


how on earth do I get m * k = n... I suspect it involves mul_left_cancel or similar but I can't find any straughtforward examples of that in mathlib.

#### Bryan Gin-ge Chen (Sep 03 2020 at 15:24):

tactic#library_search is good at finding things like this:

import tactic

example (m n a : ℤ) (ha : a ≠ 0) (k : ℤ) (h : a * (m * k) = a * n) :
m * k = n := by library_search
-- Try this: exact (mul_right_inj' ha).mp h

example (m n a : ℤ) (ha : a ≠ 0) (k : ℤ) (h : a * (m * k) = a * n) :
m * k = n := (mul_right_inj' ha).mp h -- it works!


If you're using VS Code, an interactive suggestion should pop up too.

#### toc (Sep 03 2020 at 15:26):

Well that is just 10 kinds of fantastic. I've been using the live editor. Thanks!

Last updated: May 08 2021 at 03:17 UTC