-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_dualAnnihilator_eq_map (W : Subspace K V) [FiniteDimensional K W] :
    W.dualAnnihilator.dualAnnihilator = W.map (Dual.eval K V)

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Tactic:
rw [eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)]

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K ↥(map (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Tactic:
exact e2.finrank_eq

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Tactic:
let e2 := (Free.chooseBasis K _).toDualEquiv ≪≫ₗ W.dualAnnihilator.dualQuotEquivDualAnnihilator

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Tactic:
let e1 := (Free.chooseBasis K W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K ↥(map (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Tactic:
rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Tactic:
haveI := LinearEquiv.finiteDimensional (V₂ := W.dualAnnihilator.dualAnnihilator) e2

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Tactic:
haveI := e1.finiteDimensional

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W