mathlib

f4128dc4 - chore(ring_theory/ideal/basic): Make an argument to mul_mem_{left,right} explicit (#5611)

chore(ring_theory/ideal/basic): Make an argument to mul_mem_{left,right} explicit (#5611) Before this change, the lemmas with result `a * b ∈ I` did not have enough explicit arguments to determine both `a` and `b`, such as `I.mul_mem_left hb`. This resulted in callers using `show`, `@`, or sometimes ignoring the API and using `smul_mem` which does have appropriate argument explicitness. These callers have been cleaned up accordingly.