case h.h.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
x✝¹ : Dual K V₁
x✝ : { x // x ∈ W }
⊢ ↑(↑(LinearMap.comp (Submodule.dualPairing W) (mkQ (dualAnnihilator W))) x✝¹) x✝ =
    ↑(↑(LinearMap.comp (↑(quotAnnihilatorEquiv W)) (mkQ (dualAnnihilator W))) x✝¹) x✝
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ Submodule.dualPairing W = ↑(quotAnnihilatorEquiv W)
ext
no goals
case h.h.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
x✝¹ : Dual K V₁
x✝ : { x // x ∈ W }
⊢ ↑(↑(LinearMap.comp (Submodule.dualPairing W) (mkQ (dualAnnihilator W))) x✝¹) x✝ =
    ↑(↑(LinearMap.comp (↑(quotAnnihilatorEquiv W)) (mkQ (dualAnnihilator W))) x✝¹) x✝
rfl