K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
x : Module.Dual K { x // x ∈ W }
⊢ ↑1 x = x
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
x : Module.Dual K { x // x ∈ W }
⊢ ↑(comp (dualRestrict W) (dualLift W)) x = x
rw [dualRestrict_comp_dualLift]
no goals
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
x : Module.Dual K { x // x ∈ W }
⊢ ↑1 x = x
rfl