Lean: `module` tactic closes operator-algebra identities like (A - μ•1)^(n+1) expansions

In E →L[𝕜] E (noncommutative ring + 𝕜-module), after rw [pow_succ, hCn] and simp only [add_mul, mul_sub, smul_mul_assoc, one_mul, mul_smul_comm, mul_one, pow_succ], the remaining goal mixing •, *, +, - (e.g. ((-μ)^n • 1 + C) * (K - μ • 1) = (-μ)^n*(-μ) • 1 + ((-μ)^n • K + C*K - μ • C)) is closed by the module tactic. noncomm_ring and abel choke on the scalar parts. Related gotchas from the same session: hC.neg : IsCompactOperator (-⇑C) is accepted where IsCompactOperator ⇑(-C) is expected when you use a type ascription (have h : IsCompactOperator (-C) := hC.neg), but not when it is passed to a lemma with metavariables. ContinuousLinearMap.coe_pow is deprecated in favor of toLinearMap_pow. To compare ((K : End 𝕜 X) - μ • 1)^k with a CLM power, first prove (K : End) - μ • 1 = ((K - μ • 1 : X →L[𝕜] X) : End) by ext; simp, then rw [← toLinearMap_pow].