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 : { x // x ∈ W }
⊢ ↑(↑(inl K (Module.Dual K { x // x ∈ W })
                ({ x // x ∈ ↑(Classical.indefiniteDescription (fun x => IsCompl W x) (_ : ∃ q, IsCompl W q)) } →ₗ[K] K))
            φ).fst
      w =
    ↑φ w
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 : { x // x ∈ W }
⊢ ↑(↑(dualLift W) φ) ↑w = ↑φ w
erw [ofIsCompl_left_apply _ w]
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 : { x // x ∈ W }
⊢ ↑(↑(inl K (Module.Dual K { x // x ∈ W })
                ({ x // x ∈ ↑(Classical.indefiniteDescription (fun x => IsCompl W x) (_ : ∃ q, IsCompl W q)) } →ₗ[K] K))
            φ).fst
      w =
    ↑φ w
rfl