What's the fastest way to prove this?

Stream: general

[Kenny Lau]

example : ∀ m n : ℕ, m = m * n → m = 0 ∨ n = 1 := sorry

[Nicholas Scheel]

I would do by_cases m = 0 and eq_of_mul_eq_mul_left

[Nicholas Scheel]

(after mul_one)

[Nicholas Scheel]

or maybe even by_cases n = 1 and eq_zero_of_mul_eq_self_right

[Nicholas Scheel]

(both of those long theorems are from integral domains https://github.com/leanprover/lean/blob/master/library/init/algebra/ring.lean#L290 )

[Kenny Lau]

but they don't apply to natural numbers

[Nicholas Scheel]

oh whoops, you’re right ... rings and all

[Nicholas Scheel]

https://github.com/leanprover/lean/blob/master/library/init/data/nat/lemmas.lean#L332

[Kenny Lau]

thanks