diff --git a/src/algebra/module.lean b/src/algebra/module.lean
index 6bf0741958dcd..416557ce7a6cc 100644
--- a/src/algebra/module.lean
+++ b/src/algebra/module.lean
@@ -8,8 +8,8 @@ Modules over a ring.
 ## Implemetation notes
 
 
-Throughout the `linear_map` section implicit `{}` brackets are often used instead of type class `[]` brackets. 
-This is done when the instances can be inferred because they are implicit arguments to the type `linear_map`. 
+Throughout the `linear_map` section implicit `{}` brackets are often used instead of type class `[]` brackets.
+This is done when the instances can be inferred because they are implicit arguments to the type `linear_map`.
 When they can be inferred from the type it is faster to use this method than to use type class inference
 
 -/
@@ -420,3 +420,17 @@ def is_add_group_hom.to_linear_map [add_comm_group α] [add_comm_group β]
   smul := λ i x, int.induction_on i (by rw [zero_smul, zero_smul, is_add_group_hom.map_zero f])
     (λ i ih, by rw [add_smul, add_smul, is_add_hom.map_add f, ih, one_smul, one_smul])
     (λ i ih, by rw [sub_smul, sub_smul, is_add_group_hom.map_sub f, ih, one_smul, one_smul]) }
+
+lemma module.smul_eq_smul {R : Type*} [ring R] {β : Type*} [add_comm_group β] [module R β]
+  (n : ℕ) (b : β) : n • b = (n : R) • b :=
+begin
+  induction n with n ih,
+  { rw [nat.cast_zero, zero_smul, zero_smul] },
+  { change (n + 1) • b = (n + 1 : R) • b,
+    rw [add_smul, add_smul, one_smul, ih, one_smul] }
+end
+
+lemma finset.sum_const' {α : Type*} (R : Type*) [ring R] {β : Type*}
+  [add_comm_group β] [module R β] {s : finset α} (b : β) :
+  finset.sum s (λ (a : α), b) = (finset.card s : R) • b :=
+by rw [finset.sum_const, ← module.smul_eq_smul]; refl
diff --git a/src/algebra/ring.lean b/src/algebra/ring.lean
index 5adb139b94215..5ab2e2cdfd4a4 100644
--- a/src/algebra/ring.lean
+++ b/src/algebra/ring.lean
@@ -56,6 +56,10 @@ theorem mul_two (n : α) : n * 2 = n + n :=
 theorem bit0_eq_two_mul (n : α) : bit0 n = 2 * n :=
 (two_mul _).symm
 
+@[simp] lemma mul_ite {α} [semiring α] (P : Prop) [decidable P] (a : α) :
+  a * (if P then 1 else 0) = if P then a else 0 :=
+by split_ifs; simp
+
 variable (α)
 
 /-- Either zero and one are nonequal in a semiring, or the semiring is the zero ring. -/
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index b9f835f4cbe6c..19161e25def65 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -75,7 +75,11 @@ theorem finite_mem_finset (s : finset α) : finite {a | a ∈ s} :=
 theorem finite.of_fintype [fintype α] (s : set α) : finite s :=
 by classical; exact ⟨set_fintype s⟩
 
-instance decidable_mem_of_fintype [decidable_eq α] (s : set α) [fintype s] (a) : decidable (a ∈ s) :=
+/-- Membership of a subset of a finite type is decidable.
+
+Using this as an instance leads to potential loops with `subtype.fintype` under certain decidability
+assumptions, so it should only be declared a local instance. -/
+def decidable_mem_of_fintype [decidable_eq α] (s : set α) [fintype s] (a) : decidable (a ∈ s) :=
 decidable_of_iff _ mem_to_finset
 
 instance fintype_empty : fintype (∅ : set α) :=
@@ -117,10 +121,16 @@ lemma card_image_of_injective (s : set α) [fintype s]
   fintype.card (f '' s) = fintype.card s :=
 card_image_of_inj_on $ λ _ _ _ _ h, H h
 
+section
+
+local attribute [instance] decidable_mem_of_fintype
+
 instance fintype_insert [decidable_eq α] (a : α) (s : set α) [fintype s] : fintype (insert a s : set α) :=
 if h : a ∈ s then by rwa [insert_eq, union_eq_self_of_subset_left (singleton_subset_iff.2 h)]
 else fintype_insert' _ h
 
+end
+
 @[simp] theorem finite_insert (a : α) {s : set α} : finite s → finite (insert a s)
 | ⟨h⟩ := ⟨@set.fintype_insert _ (classical.dec_eq α) _ _ h⟩
 
@@ -451,6 +461,19 @@ begin
     { exact ih c hcs hbc } }
 end
 
+section
+
+local attribute [instance, priority 1] classical.prop_decidable
+
+lemma to_finset_card {α : Type*} [fintype α] (H : set α) :
+  H.to_finset.card = fintype.card H :=
+multiset.card_map subtype.val finset.univ.val
+
+lemma to_finset_inter {α : Type*} [fintype α] (s t : set α) [decidable_eq α] :
+  (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
+by ext; simp
+
+end
 end set
 
 namespace finset
@@ -497,3 +520,17 @@ calc
   ... = s.prod g : by rw image_preimage
 
 end finset
+
+lemma fintype.exists_max [fintype α] [nonempty α]
+  {β : Type*} [decidable_linear_order β] (f : α → β) :
+  ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
+begin
+  obtain ⟨y, hy⟩ : ∃ y, y ∈ (set.range f).to_finset,
+  { haveI := classical.inhabited_of_nonempty ‹nonempty α›,
+    exact ⟨f (default α), set.mem_to_finset.mpr $ set.mem_range_self _⟩ },
+  rcases finset.max_of_mem hy with ⟨y₀, h⟩,
+  rcases set.mem_to_finset.1 (finset.mem_of_max h) with ⟨x₀, rfl⟩,
+  use x₀,
+  intro x,
+  apply finset.le_max_of_mem (set.mem_to_finset.mpr $ set.mem_range_self x) h
+end
diff --git a/src/linear_algebra/dual.lean b/src/linear_algebra/dual.lean
index 75d34abe35868..acc111910e917 100644
--- a/src/linear_algebra/dual.lean
+++ b/src/linear_algebra/dual.lean
@@ -2,24 +2,58 @@
 Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Fabian Glöckle
-
-Dual vector spaces, the spaces of linear functionals to the base field, including the dual basis
-isomorphism and evaluation isomorphism in the finite-dimensional case.
 -/
-import linear_algebra.dimension
+
 import linear_algebra.tensor_product
+import linear_algebra.finite_dimensional
+import tactic.apply_fun
 noncomputable theory
 
+/-!
+# Dual vector spaces
+
+The dual space of an R-module M is the R-module of linear maps `M → R`.
+
+## Main definitions
+
+* `dual R M` defines the dual space of M over R.
+* Given a basis for a K-vector space `V`, `is_basis.to_dual` produces a map from `V` to `dual K V`.
+* Given families of vectors `e` and `ε`, `dual_pair e ε` states that these families have the
+  characteristic properties of a basis and a dual.
+
+## Main results
+
+* `to_dual_equiv` : the dual space is linearly equivalent to the primal space.
+* `dual_pair.is_basis` and `dual_pair.eq_dual`: if `e` and `ε` form a dual pair, `e` is a basis and
+  `ε` is its dual basis.
+
+## Notation
+
+We sometimes use `V'` as local notation for `dual K V`.
+
+## Implementation details
+
+Because of unresolved type class issues, the following local instance can be of use:
+
+```
+private def help_tcs : has_scalar K V := mul_action.to_has_scalar _ _
+local attribute [instance] help_tcs
+```
+-/
+
 namespace module
 variables (R : Type*) (M : Type*)
 variables [comm_ring R] [add_comm_group M] [module R M]
 
+/-- The dual space of an R-module M is the R-module of linear maps `M → R`. -/
 @[derive [add_comm_group, module R]] def dual := M →ₗ[R] R
 
 namespace dual
 
 instance : has_coe_to_fun (dual R M) := ⟨_, linear_map.to_fun⟩
 
+/-- Maps a module M to the dual of the dual of M. See `vector_space.eval_range` and
+`vector_space.eval_equiv`. -/
 def eval : M →ₗ[R] (dual R (dual R M)) := linear_map.id.flip
 
 lemma eval_apply (v : M) (a : dual R M) : (eval R M v) a = a v :=
@@ -39,11 +73,13 @@ open vector_space module module.dual submodule linear_map cardinal function
 
 instance dual.vector_space : vector_space K (dual K V) := { ..module.dual.inst K V }
 
-variables [decidable_eq ι]
+variables [de : decidable_eq ι]
 variables {B : ι → V} (h : is_basis K B)
 
-include h
+include de h
 
+/-- The linear map from a vector space equipped with basis to its dual vector space,
+taking basis elements to corresponding dual basis elements. -/
 def to_dual : V →ₗ[K] module.dual K V :=
 h.constr $ λ v, h.constr $ λ w, if w = v then 1 else 0
 
@@ -53,7 +89,8 @@ lemma to_dual_apply (i j : ι) :
 
 def to_dual_flip (v : V) : (V →ₗ[K] K) := (linear_map.flip h.to_dual).to_fun v
 
-omit h
+omit de h
+/-- Evaluation of finitely supported functions at a fixed point `i`, as a `K`-linear map. -/
 def eval_finsupp_at (i : ι) : (ι →₀ K) →ₗ[K] K :=
 { to_fun := λ f, f i,
   add := by intros; rw finsupp.add_apply,
@@ -66,6 +103,8 @@ def coord_fun (i : ι) : (V →ₗ[K] K) := (eval_finsupp_at i).comp h.repr
 
 lemma coord_fun_eq_repr (v : V) (i : ι) : h.coord_fun i v = h.repr v i := rfl
 
+include de
+
 lemma to_dual_swap_eq_to_dual (v w : V) : h.to_dual_flip v w = h.to_dual w v := rfl
 
 lemma to_dual_eq_repr (v : V) (i : ι) : (h.to_dual v) (B i) = h.repr v i :=
@@ -100,7 +139,6 @@ begin
   intro f,
   rw linear_map.mem_range,
   let lin_comb : ι →₀ K := finsupp.on_finset fin.elems (λ i, f.to_fun (B i)) _,
-  --let emb := embedding.subtype B,
   { use finsupp.total ι V K B lin_comb,
     apply h.ext,
     { intros i,
@@ -112,6 +150,7 @@ begin
     apply fin.complete }
 end
 
+/-- Maps a basis for `V` to a basis for the dual space. -/
 def dual_basis : ι → dual K V := λ i, h.to_dual (B i)
 
 theorem dual_lin_independent : linear_independent K h.dual_basis :=
@@ -121,13 +160,14 @@ begin
   exact disjoint_bot_right
 end
 
+/-- A vector space is linearly equivalent to its dual space. -/
 def to_dual_equiv [fintype ι] : V ≃ₗ[K] (dual K V) :=
 linear_equiv.of_bijective h.to_dual h.to_dual_ker h.to_dual_range
 
 theorem dual_basis_is_basis [fintype ι] : is_basis K h.dual_basis :=
 h.to_dual_equiv.is_basis h
 
-@[simp] lemma to_dual_to_dual [decidable_eq (dual K (dual K V))] [fintype ι] :
+@[simp] lemma to_dual_to_dual [fintype ι] :
   (h.dual_basis_is_basis.to_dual).comp h.to_dual = eval K V :=
 begin
   apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ h,
@@ -202,7 +242,119 @@ begin
   apply_instance
 end
 
+/-- A vector space is linearly equivalent to the dual of its dual space. -/
 def eval_equiv (h : dim K V < omega) : V ≃ₗ[K] dual K (dual K V) :=
 linear_equiv.of_bijective (eval K V) eval_ker (eval_range h)
 
 end vector_space
+
+section dual_pair
+
+open vector_space module module.dual linear_map function
+
+universes u v w
+variables {K : Type u} {V : Type v} {ι : Type w} [decidable_eq ι]
+variables [discrete_field K] [add_comm_group V] [vector_space K V]
+
+local notation `V'` := dual K V
+
+/-- `e` and `ε` have characteristic properties of a basis and its dual -/
+structure dual_pair (e : ι → V) (ε : ι → V') :=
+(eval : ∀ i j : ι, ε i (e j) = if i = j then 1 else 0)
+(total : ∀ {v : V}, (∀ i, ε i v = 0) → v = 0)
+[finite : ∀ v : V, fintype {i | ε i v ≠ 0}]
+
+end dual_pair
+
+namespace dual_pair
+
+open vector_space module module.dual linear_map function
+
+universes u v w
+variables {K : Type u} {V : Type v} {ι : Type w} [dι : decidable_eq ι]
+variables [discrete_field K] [add_comm_group V] [vector_space K V]
+variables {e : ι → V} {ε : ι → dual K V} (h : dual_pair e ε)
+
+include h
+
+/-- The coefficients of `v` on the basis `e` -/
+def coeffs (v : V) : ι →₀ K :=
+{ to_fun := λ i, ε i v,
+  support := by { haveI := h.finite v, exact {i : ι | ε i v ≠ 0}.to_finset },
+  mem_support_to_fun := by {intro i, rw set.mem_to_finset, exact iff.rfl } }
+
+
+@[simp] lemma coeffs_apply (v : V) (i : ι) : h.coeffs v i = ε i v := rfl
+
+omit h
+private def help_tcs : has_scalar K V := mul_action.to_has_scalar _ _
+
+local attribute [instance] help_tcs
+
+/-- linear combinations of elements of `e`.
+This is a convenient abbreviation for `finsupp.total _ V K e l` -/
+def lc (e : ι → V) (l : ι →₀ K) : V := l.sum (λ (i : ι) (a : K), a • (e i))
+
+include h
+
+lemma dual_lc (l : ι →₀ K) (i : ι) : ε i (dual_pair.lc e l) = l i :=
+begin
+  erw linear_map.map_sum,
+  simp only [h.eval, map_smul, smul_eq_mul],
+  rw finset.sum_eq_single i,
+  { simp },
+  { intros q q_in q_ne,
+    simp [q_ne.symm] },
+  { intro p_not_in,
+    simp [finsupp.not_mem_support_iff.1 p_not_in] },
+end
+
+@[simp]
+lemma coeffs_lc (l : ι →₀ K) : h.coeffs (dual_pair.lc e l) = l :=
+by { ext i, rw [h.coeffs_apply, h.dual_lc] }
+
+/-- For any v : V n, \sum_{p ∈ Q n} (ε p v) • e p = v -/
+lemma decomposition (v : V) : dual_pair.lc e (h.coeffs v) = v :=
+begin
+  refine eq_of_sub_eq_zero (h.total _),
+  intros i,
+  simp [-sub_eq_add_neg, linear_map.map_sub, h.dual_lc, sub_eq_zero_iff_eq]
+end
+
+lemma mem_of_mem_span {H : set ι} {x : V} (hmem : x ∈ submodule.span K (e '' H)) :
+  ∀ i : ι, ε i x ≠ 0 → i ∈ H :=
+begin
+  intros i hi,
+  rcases (finsupp.mem_span_iff_total _).mp hmem with ⟨l, supp_l, sum_l⟩,
+  change dual_pair.lc e l = x at sum_l,
+  rw finsupp.mem_supported' at supp_l,
+  apply classical.by_contradiction,
+  intro i_not,
+  apply hi,
+  rw ← sum_l,
+  simpa [h.dual_lc] using supp_l i i_not
+end
+
+lemma is_basis : is_basis K e :=
+begin
+  split,
+  { rw linear_independent_iff,
+    intros l H,
+    change dual_pair.lc e l = 0 at H,
+    ext i,
+    apply_fun ε i at H,
+    simpa [h.dual_lc] using H },
+  { rw submodule.eq_top_iff',
+    intro v,
+    rw [← set.image_univ, finsupp.mem_span_iff_total],
+    exact ⟨h.coeffs v, by simp, h.decomposition v⟩ },
+end
+
+lemma eq_dual : ε = is_basis.dual_basis h.is_basis :=
+begin
+  funext i,
+  refine h.is_basis.ext (λ _, _),
+  erw [is_basis.to_dual_apply, h.eval]
+end
+
+end dual_pair
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
index 685557a179bc7..a74f217c781b9 100644
--- a/src/linear_algebra/finite_dimensional.lean
+++ b/src/linear_algebra/finite_dimensional.lean
@@ -104,6 +104,24 @@ begin
   rw [this, map_top (submodule.subtype S), range_subtype],
 end
 
+section
+
+variables {ι : Type w} [fintype ι] [decidable_eq V]
+variables {b : ι → V} (h : is_basis K b)
+include h
+
+lemma fg_of_finite_basis : submodule.fg (⊤ : submodule K V) :=
+⟨ finset.univ.image b, by {convert h.2, simp} ⟩
+
+def finite_dimensional_of_finite_basis : finite_dimensional K V :=
+finite_dimensional.of_fg $ fg_of_finite_basis h
+
+lemma dim_eq_card : dim K V = fintype.card ι :=
+by rw [←h.mk_range_eq_dim, cardinal.fintype_card,
+       set.card_range_of_injective (h.injective zero_ne_one)]
+
+end
+
 end finite_dimensional
 
 namespace linear_map
diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean
index a5b054ded5d53..644373da1bcc4 100644
--- a/src/linear_algebra/finsupp.lean
+++ b/src/linear_algebra/finsupp.lean
@@ -8,12 +8,13 @@ Linear structures on function with finite support `α →₀ M`.
 import data.finsupp linear_algebra.basic
 
 noncomputable theory
-local attribute [instance, priority 10] classical.prop_decidable
 
 open lattice set linear_map submodule
 
 namespace finsupp
 
+open_locale classical
+
 variables {α : Type*} {M : Type*} {R : Type*}
 variables [ring R] [add_comm_group M] [module R M]
 
@@ -420,3 +421,9 @@ begin
 end
 
 end finsupp
+
+lemma linear_map.map_finsupp_total {R : Type*} {β : Type*} {γ : Type*} [ring R]
+  [add_comm_group β] [module R β] [add_comm_group γ] [module R γ]
+  (f : β →ₗ[R] γ) {ι : Type*} [fintype ι] {g : ι → β} (l : ι →₀ R) :
+  f (finsupp.total ι β R g l) = finsupp.total ι γ R (f ∘ g) l :=
+by simp only [finsupp.total_apply, finsupp.total_apply, finsupp.sum, f.map_sum, f.map_smul]
diff --git a/src/ring_theory/power_series.lean b/src/ring_theory/power_series.lean
index cb0e779e29779..8d03fea7c30d7 100644
--- a/src/ring_theory/power_series.lean
+++ b/src/ring_theory/power_series.lean
@@ -164,14 +164,14 @@ end
 protected lemma mul_one : φ * 1 = φ :=
 ext $ λ n,
 begin
-  rw [coeff_mul, finset.sum_eq_single (n, (0 : σ →₀ ℕ))];
-  simp [mem_antidiagonal_support, coeff_one],
-  show ∀ (i j : σ →₀ ℕ), i + j = n → (i = n → j ≠ 0) →
-    (coeff α i) φ * (if (j = 0) then 1 else 0) = 0,
-  intros i j hij h,
-  rw [if_neg, mul_zero],
-  contrapose! h,
-  simpa [h] using hij,
+  rw [coeff_mul, finset.sum_eq_single (n, (0 : σ →₀ ℕ))],
+  rotate,
+  { rintros ⟨i, j⟩ hij h,
+    rw [coeff_one, if_neg, mul_zero],
+    rw mem_antidiagonal_support at hij,
+    contrapose! h,
+    simpa [h] using hij },
+  all_goals { simp [mem_antidiagonal_support, coeff_one] }
 end
 
 protected lemma mul_add (φ₁ φ₂ φ₃ : mv_power_series σ α) :
diff --git a/src/set_theory/cardinal.lean b/src/set_theory/cardinal.lean
index e518da2be4321..fa57a95c76ee4 100644
--- a/src/set_theory/cardinal.lean
+++ b/src/set_theory/cardinal.lean
@@ -606,7 +606,7 @@ begin
   rw [cardinal.fintype_card, fintype.card_coe]
 end
 
-@[simp, elim_cast] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
+@[simp, move_cast] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
 by induction n; simp [nat.pow_succ, -_root_.add_comm, power_add, *]
 
 @[simp, elim_cast] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=