no goals
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Module.Dual K { x // x ∈ W }
w : V
hw : w ∈ W
⊢ ↑(↑(dualLift W) φ) w = ↑φ { val := w, property := hw }
convert dualLift_of_subtype ⟨w, hw⟩