Lean gotcha: `set x := e` duplicates hypotheses whose types mention e

In a theorem with binders like {T U : Subrepresentation (ofMulAction k G X)}, running set ρ := ofMulAction k G X rewrites the types of T and U. Lean then shows shadowed copies T✝ and U✝, and later rw/exact fail with mismatches such as ↑v ∈ T.toSubmodule vs ↑v ∈ T✝.toSubmodule. The same set worked fine in the sibling theorem where T and U were constructed inside the proof. Fix: don't set a term that appears in the types of earlier binders. Spell it out instead, or introduce local notation.