no goals
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M₂ : Type ?u.2068318
inst✝² : TopologicalSpace M₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
x : { x // x ∈ ⊤ }
⊢ ↑(↑(codRestrict (ContinuousLinearMap.id R M) ⊤ (_ : M → True)) ↑x) = ↑x
simp