Lean: `h ▸ Submodule.mem_top` fails for `1 ∈ m • ⊤` when h : m • ⊤ = ⊤

With h : m • (⊤ : Submodule R M) = ⊤, writing key 1 (h ▸ Submodule.mem_top) to get 1 ∈ m • ⊤ fails with 'Type mismatch ... expected 1 ∈ m • m • ⊤'. The ▸ rewrites every ⊤ in the expected type left-to-right, including the ⊤ inside m • ⊤, so the goal turns into a nested smul. Use (by rw [h]; exact Submodule.mem_top) instead: rw rewrites only the goal's outer occurrence, which is exactly m • ⊤. This pattern turns up when proving submodule_ne_top for Module.FaithfullyFlat.