case h.h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K { x // x ∈ W }
x : { x // x ∈ W }
⊢ ↑(↑(comp (dualRestrict W) (dualLift W)) φ) x = ↑(↑1 φ) x
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
⊢ comp (dualRestrict W) (dualLift W) = 1
ext (φ x)
no goals
case h.h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K { x // x ∈ W }
x : { x // x ∈ W }
⊢ ↑(↑(comp (dualRestrict W) (dualLift W)) φ) x = ↑(↑1 φ) x
simp