n m k : Nat
hm : 0 < m
h : m * n = m * k
⊢ n = k
n m k : Nat
hm : 0 < m
h : n * m = k * m
⊢ n = k
rw [Nat.mul_comm n m, Nat.mul_comm k m] at h
no goals
n m k : Nat
hm : 0 < m
h : m * n = m * k
⊢ n = k
exact Nat.eq_of_mul_eq_mul_left hm h