case left
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₁
⊢ LinearMap.SeparatingLeft (dualCopairing W)

case right
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₁
⊢ LinearMap.SeparatingRight (dualCopairing W)
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₁
⊢ LinearMap.Nondegenerate (dualCopairing W)
constructor
case left
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₁
⊢ LinearMap.ker ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) = ⊥
case left
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₁
⊢ LinearMap.SeparatingLeft (dualCopairing W)
rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualCopairing_eq]
no goals
case left
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₁
⊢ LinearMap.ker ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) = ⊥
apply LinearEquiv.ker
case right.mk
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₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : { x // x ∈ dualAnnihilator W }), ↑(↑(dualCopairing W) x_1) (Quot.mk Setoid.r x) = 0) →
    Quot.mk Setoid.r x = 0
case right
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₁
⊢ LinearMap.SeparatingRight (dualCopairing W)
rintro ⟨x⟩
case right.mk
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₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : { x // x ∈ dualAnnihilator W }), ↑x_1 x = 0) → x ∈ W
case right.mk
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₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : { x // x ∈ dualAnnihilator W }), ↑(↑(dualCopairing W) x_1) (Quot.mk Setoid.r x) = 0) →
    Quot.mk Setoid.r x = 0
simp only [Quotient.quot_mk_eq_mk, dualCopairing_apply, Quotient.mk_eq_zero]
case right.mk
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₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W), ↑{ val := x_1, property := h } x = 0) →
    ∀ (φ : Dual K V₁), φ ∈ dualAnnihilator W → ↑φ x = 0
case right.mk
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₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : { x // x ∈ dualAnnihilator W }), ↑x_1 x = 0) → x ∈ W
rw [← forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall]
no goals
case right.mk
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₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W), ↑{ val := x_1, property := h } x = 0) →
    ∀ (φ : Dual K V₁), φ ∈ dualAnnihilator W → ↑φ x = 0
exact id