Stream: new members
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.
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