feat: heterogeneous `(k : Nat) * (a : R)` support in grind linarith#8773

leodemoura merged 3 commits intomasterleanprover/lean4:masterfrom

grind_linarith_hmul_natleanprover/lean4:grind_linarith_hmul_natCopy head branch name to clipboard