refactor(*): bundle is_basis (#7496)

This PR replaces the definition of a basis used in mathlib and fixes the usages throughout.

Rationale: Previously, `is_basis` was a predicate on a family of vectors, saying this family is linear independent and spans the whole space. We encountered many small annoyances when working with these unbundled definitions, for example complicated `is_basis` arguments being hidden in the goal view or slow elaboration when mapping a basis to a slightly different set of basis vectors. The idea to turn `basis` into a bundled structure originated in the discussion on #4949. @digama0 suggested on Zulip to identify these "bundled bases" with their map `repr : M ≃ₗ[R] (ι →₀ R)` that sends a vector to its coordinates. (In fact, that specific map used to be only a `linear_map` rather than an equiv.)

Overview of the changes:
 - The `is_basis` predicate has been replaced with the `basis` structure. 
 - Parameters of the form `{b : ι → M} (hb : is_basis R b)` become a single parameter `(b : basis ι R M)`.
 - Constructing a basis from a linear independent family spanning the whole space is now spelled `basis.mk hli hspan`, instead of `and.intro hli hspan`.
 -  You can also use `basis.of_repr` to construct a basis from an equivalence `e : M ≃ₗ[R] (ι →₀ R)`. If `ι` is a `fintype`, you can use `basis.of_equiv_fun (e : M ≃ₗ[R] (ι → R))` instead, saving you from having to work with `finsupp`s.
 - Most declaration names that used to contain `is_basis` are now spelled with `basis`, e.g. `pi.is_basis_fun` is now `pi.basis_fun`.
 - Theorems of the form `exists_is_basis K V : ∃ (s : set V) (b : s -> V), is_basis K b` and `finite_dimensional.exists_is_basis_finset K V : [finite_dimensional K V] -> ∃ (s : finset V) (b : s -> V), is_basis K b` have been replaced with (noncomputable) defs such as `basis.of_vector_space K V : basis (basis.of_vector_space_index K V) K V` and `finite_dimensional.finset_basis : basis (finite_dimensional.finset_basis_index K V) K V`; the indexing sets being a separate definition means we can declare a `fintype (basis.of_vector_space_index K V)` instance on finite dimensional spaces, rather than having to use `cases exists_is_basis_fintype K V with ...` each time.
 - Definitions of a `basis` are now, wherever practical, accompanied by `simp` lemmas giving the values of `coe_fn` and `repr` for that basis.
 - Some auxiliary results like `pi.is_basis_fun₀` have been removed since they are no longer needed.

Basic API overview:
* `basis ι R M` is the type of `ι`-indexed `R`-bases for a module `M`, represented by a linear equiv `M ≃ₗ[R] ι →₀ R`.
* the basis vectors of a basis `b` are given by `b i` for `i : ι`
* `basis.repr` is the isomorphism sending `x : M` to its coordinates `basis.repr b x : ι →₀ R`. The inverse of `b.repr` is `finsupp.total _ _ _ b`. The converse, turning this isomorphism into a basis, is called `basis.of_repr`.
* If `ι` is finite, there is a variant of `repr` called `basis.equiv_fun b : M ≃ₗ[R] ι → R`. The converse, turning this isomorphism into a basis, is called `basis.of_equiv_fun`.
* `basis.constr hv f` constructs a linear map `M₁ →ₗ[R] M₂` given the values `f : ι → M₂` at the
  basis elements `⇑b : ι → M₁`.
* `basis.mk`: a linear independent set of vectors spanning the whole module determines a basis (the converse consists of `basis.linear_independent` and `basis.span_eq`
* `basis.ext` states that two linear maps are equal if they coincide on a basis; similar results are available for linear equivs (if they coincide on the basis vectors), elements (if their coordinates coincide) and the functions `b.repr` and `⇑b`.
* `basis.of_vector_space` states that every vector space has a basis.
* `basis.reindex` uses an equiv to map a basis to a different indexing set, `basis.map` uses a linear equiv to map a basis to a different module

Zulip discussions:
 * https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Bundled.20basis
 * https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234949

Author: Vierkantor

archive/sensitivity.lean

@@ -229,11 +229,11 @@ since this cardinal is finite, as a natural number in `finrank_V` -/
 
 lemma dim_V : module.rank ℝ (V n) = 2^n :=
 have module.rank ℝ (V n) = (2^n : ℕ),
-  by { rw [dim_eq_card_basis (dual_pair_e_ε _).is_basis, Q.card]; apply_instance },
+  by { rw [dim_eq_card_basis (dual_pair_e_ε _).basis, Q.card]; apply_instance },
 by assumption_mod_cast
 
 instance : finite_dimensional ℝ (V n) :=
-finite_dimensional.of_fintype_basis (dual_pair_e_ε _).is_basis
+finite_dimensional.of_fintype_basis (dual_pair_e_ε _).basis
 
 lemma finrank_V : finrank ℝ (V n) = 2^n :=
 have _ := @dim_V n,
@@ -367,12 +367,14 @@ begin
     rw ← dim_eq_of_injective (g m) g_injective,
     apply dim_V },
   have dimW : dim W = card H,
-  { have li : linear_independent ℝ (set.restrict e H) :=
-      linear_independent.comp (dual_pair_e_ε _).is_basis.1 _ subtype.val_injective,
+  { have li : linear_independent ℝ (set.restrict e H),
+    { convert (dual_pair_e_ε _).basis.linear_independent.comp _ subtype.val_injective,
+      rw (dual_pair_e_ε _).coe_basis },
     have hdW := dim_span li,
     rw set.range_restrict at hdW,
     convert hdW,
-    rw [cardinal.mk_image_eq (dual_pair_e_ε _).is_basis.injective, cardinal.fintype_card] },
+    rw [← (dual_pair_e_ε _).coe_basis, cardinal.mk_image_eq (dual_pair_e_ε _).basis.injective,
+        cardinal.fintype_card] },
   rw ← finrank_eq_dim ℝ at ⊢ dim_le dim_add dimW,
   rw [← finrank_eq_dim ℝ, ← finrank_eq_dim ℝ] at dim_add,
   norm_cast at ⊢ dim_le dim_add dimW,
@@ -406,7 +408,7 @@ begin
         = |ε q (s • y)| :
       by rw [map_smul, smul_eq_mul, abs_mul, abs_of_nonneg (real.sqrt_nonneg _)]
     ... = |ε q (f (m+1) y)| : by rw [← f_image_g y (by simpa using y_mem_g)]
-    ... = |ε q (f (m+1) (lc _ (coeffs y)))| : by rw (dual_pair_e_ε _).decomposition y
+    ... = |ε q (f (m+1) (lc _ (coeffs y)))| : by rw (dual_pair_e_ε _).lc_coeffs y
     ... = |(coeffs y).sum (λ (i : Q (m + 1)) (a : ℝ), a • ((ε q) ∘ (f (m + 1)) ∘
             λ (i : Q (m + 1)), e i) i)| :
       by erw [(f $ m + 1).map_finsupp_total, (ε q).map_finsupp_total, finsupp.total_apply]

docs/overview.yaml

@@ -138,16 +138,16 @@ Linear algebra:
     quotient space: 'submodule.quotient'
     tensor product: 'tensor_product'
     noetherian module: 'is_noetherian'
-    basis: 'is_basis'
+    basis: 'basis'
     multilinear map: 'multilinear_map'
     alternating map: 'alternating_map'
     general linear group: 'linear_map.general_linear_group'
   Duality:
     dual vector space: 'module.dual'
-    dual basis: 'is_basis.dual_basis'
+    dual basis: 'basis.dual_basis'
   Finite-dimensional vector spaces:
     finite-dimensionality : 'finite_dimensional'
-    isomorphism with $K^n$: 'module_equiv_finsupp'
+    isomorphism with $K^n$: 'basis.equiv_fun'
     isomorphism with bidual: 'module.eval_equiv'
   Matrices:
     ring-valued matrix: 'matrix'

docs/undergrad.yaml

@@ -13,28 +13,28 @@ Linear algebra:
     complementary subspaces: 'submodule.exists_is_compl'
     linear independence: 'linear_independent'
     generating sets: 'submodule.span'
-    bases: 'is_basis'
-    existence of bases: 'exists_is_basis'
+    bases: 'basis'
+    existence of bases: 'basis.of_vector_space'
     linear map: 'linear_map'
     range of a linear map: 'linear_map.range'
     kernel of a linear map: 'linear_map.ker'
     algebra of endomorphisms of a vector space: 'module.endomorphism_algebra'
     general linear group: 'linear_map.general_linear_group'
   Duality:
     dual vector space: 'module.dual'
-    dual basis: 'is_basis.dual_basis'
+    dual basis: 'basis.dual_basis'
     transpose of a linear map: 'module.dual.transpose'
     orthogonality: ''
   Finite-dimensional vector spaces:
     finite-dimensionality : 'finite_dimensional'
-    isomorphism with $K^n$: 'module_equiv_finsupp'
+    isomorphism with $K^n$: 'basis.equiv_fun'
     rank of a linear map: 'rank'
     rank of a set of vectors: ''
     rank of a system of linear equations: ''
     isomorphism with bidual: 'module.eval_equiv'
   Multilinearity:
     multilinear map: 'multilinear_map'
-    determinant of vectors: 'is_basis.det'
+    determinant of vectors: 'basis.det'
     determinant of endomorphisms: ''
     special linear group: ''
     orientation of a $\R$-valued vector space: ''
@@ -217,7 +217,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     orthogonal complement: 'submodule.orthogonal'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
     norm: 'inner_product_space.of_core.to_has_norm'
-    orthonormal bases: 'maximal_orthonormal_iff_is_basis_of_finite_dimensional'
+    orthonormal bases: 'maximal_orthonormal_iff_basis_of_finite_dimensional'
   Endomorphisms:
     orthogonal group:
     unitary group:

src/algebra/module/basic.lean

@@ -461,9 +461,17 @@ end add_comm_group
 
 section module
 
+variables {R} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M]
+
+lemma smul_right_injective {x : M} (hx : x ≠ 0) :
+  function.injective (λ (c : R), c • x) :=
+λ c d h, sub_eq_zero.mp ((smul_eq_zero.mp
+  (calc (c - d) • x = c • x - d • x : sub_smul c d x
+                ... = 0 : sub_eq_zero.mpr h)).resolve_right hx)
+
 section nat
 
-variables {R} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [char_zero R]
+variables [char_zero R]
 
 lemma ne_neg_of_ne_zero [no_zero_divisors R] {v : R} (hv : v ≠ 0) : v ≠ -v :=
 λ h, hv (eq_zero_of_eq_neg R h)

src/algebra/module/projective.lean

@@ -134,15 +134,15 @@ section ring
 variables {R : Type u} [ring R] {P : Type v} [add_comm_group P] [module R P]
 
 /-- Free modules are projective. -/
-theorem of_free {ι : Type*} {b : ι → P} (hb : is_basis R b) : is_projective R P :=
+theorem of_free {ι : Type*} (b : basis ι R P) : is_projective R P :=
 begin
   -- need P →ₗ (P →₀ R) for definition of projective.
   -- get it from `ι → (P →₀ R)` coming from `b`.
-  use hb.constr (λ i, finsupp.single (b i) 1),
+  use b.constr ℕ (λ i, finsupp.single (b i) (1 : R)),
   intro m,
-  simp only [hb.constr_apply, mul_one, id.def, finsupp.smul_single', finsupp.total_single,
+  simp only [b.constr_apply, mul_one, id.def, finsupp.smul_single', finsupp.total_single,
     linear_map.map_finsupp_sum],
-  exact hb.total_repr m,
+  exact b.total_repr m,
 end
 
 end ring

src/analysis/normed_space/finite_dimension.lean

@@ -75,28 +75,27 @@ all norms are equivalent in finite dimension.
 
 This statement is superceded by the fact that every linear map on a finite-dimensional space is
 continuous, in `linear_map.continuous_of_finite_dimensional`. -/
-lemma continuous_equiv_fun_basis {ι : Type v} [fintype ι] (ξ : ι → E) (hξ : is_basis 𝕜 ξ) :
-  continuous hξ.equiv_fun :=
+lemma continuous_equiv_fun_basis {ι : Type v} [fintype ι] (ξ : basis ι 𝕜 E) :
+  continuous ξ.equiv_fun :=
 begin
   unfreezingI { induction hn : fintype.card ι with n IH generalizing ι E },
   { apply linear_map.continuous_of_bound _ 0 (λx, _),
-    have : hξ.equiv_fun x = 0,
+    have : ξ.equiv_fun x = 0,
       by { ext i, exact (fintype.card_eq_zero_iff.1 hn i).elim },
-    change ∥hξ.equiv_fun x∥ ≤ 0 * ∥x∥,
+    change ∥ξ.equiv_fun x∥ ≤ 0 * ∥x∥,
     rw this,
     simp [norm_nonneg] },
-  { haveI : finite_dimensional 𝕜 E := of_fintype_basis hξ,
+  { haveI : finite_dimensional 𝕜 E := of_fintype_basis ξ,
     -- first step: thanks to the inductive assumption, any n-dimensional subspace is equivalent
     -- to a standard space of dimension n, hence it is complete and therefore closed.
     have H₁ : ∀s : submodule 𝕜 E, finrank 𝕜 s = n → is_closed (s : set E),
     { assume s s_dim,
-      rcases exists_is_basis_finite 𝕜 s with ⟨b, b_basis, b_finite⟩,
-      letI : fintype b := finite.fintype b_finite,
-      have U : uniform_embedding b_basis.equiv_fun.symm.to_equiv,
-      { have : fintype.card b = n,
-          by { rw ← s_dim, exact (finrank_eq_card_basis b_basis).symm },
-        have : continuous b_basis.equiv_fun := IH (subtype.val : b → s) b_basis this,
-        exact b_basis.equiv_fun.symm.uniform_embedding (linear_map.continuous_on_pi _) this },
+      let b := basis.of_vector_space 𝕜 s,
+      have U : uniform_embedding b.equiv_fun.symm.to_equiv,
+      { have : fintype.card (basis.of_vector_space_index 𝕜 s) = n,
+          by { rw ← s_dim, exact (finrank_eq_card_basis b).symm },
+        have : continuous b.equiv_fun := IH b this,
+        exact b.equiv_fun.symm.uniform_embedding (linear_map.continuous_on_pi _) this },
       have : is_complete (s : set E),
         from complete_space_coe_iff_is_complete.1 ((complete_space_congr U).1 (by apply_instance)),
       exact this.is_closed },
@@ -105,7 +104,7 @@ begin
     { assume f,
       have : finrank 𝕜 f.ker = n ∨ finrank 𝕜 f.ker = n.succ,
       { have Z := f.finrank_range_add_finrank_ker,
-        rw [finrank_eq_card_basis hξ, hn] at Z,
+        rw [finrank_eq_card_basis ξ, hn] at Z,
         by_cases H : finrank 𝕜 f.range = 0,
         { right,
           rw H at Z,
@@ -120,14 +119,14 @@ begin
       { cases this,
         { exact H₁ _ this },
         { have : f.ker = ⊤,
-            by { apply eq_top_of_finrank_eq, rw [finrank_eq_card_basis hξ, hn, this] },
+            by { apply eq_top_of_finrank_eq, rw [finrank_eq_card_basis ξ, hn, this] },
           simp [this] } },
       exact linear_map.continuous_iff_is_closed_ker.2 this },
     -- third step: applying the continuity to the linear form corresponding to a coefficient in the
     -- basis decomposition, deduce that all such coefficients are controlled in terms of the norm
-    have : ∀i:ι, ∃C, 0 ≤ C ∧ ∀(x:E), ∥hξ.equiv_fun x i∥ ≤ C * ∥x∥,
+    have : ∀i:ι, ∃C, 0 ≤ C ∧ ∀(x:E), ∥ξ.equiv_fun x i∥ ≤ C * ∥x∥,
     { assume i,
-      let f : E →ₗ[𝕜] 𝕜 := (linear_map.proj i).comp hξ.equiv_fun,
+      let f : E →ₗ[𝕜] 𝕜 := (linear_map.proj i).comp ξ.equiv_fun,
       let f' : E →L[𝕜] 𝕜 := { cont := H₂ f, ..f },
       exact ⟨∥f'∥, norm_nonneg _, λx, continuous_linear_map.le_op_norm f' x⟩ },
     -- fourth step: combine the bound on each coefficient to get a global bound and the continuity
@@ -148,18 +147,17 @@ theorem linear_map.continuous_of_finite_dimensional [finite_dimensional 𝕜 E]
 begin
   -- for the proof, go to a model vector space `b → 𝕜` thanks to `continuous_equiv_fun_basis`, and
   -- argue that all linear maps there are continuous.
-  rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
-  letI : fintype b := finite.fintype b_finite,
-  have A : continuous b_basis.equiv_fun :=
-    continuous_equiv_fun_basis _ b_basis,
-  have B : continuous (f.comp (b_basis.equiv_fun.symm : (b → 𝕜) →ₗ[𝕜] E)) :=
+  let b := basis.of_vector_space 𝕜 E,
+  have A : continuous b.equiv_fun :=
+    continuous_equiv_fun_basis b,
+  have B : continuous (f.comp (b.equiv_fun.symm : (basis.of_vector_space_index 𝕜 E → 𝕜) →ₗ[𝕜] E)) :=
     linear_map.continuous_on_pi _,
-  have : continuous ((f.comp (b_basis.equiv_fun.symm : (b → 𝕜) →ₗ[𝕜] E))
-                      ∘ b_basis.equiv_fun) := B.comp A,
+  have : continuous ((f.comp (b.equiv_fun.symm : (basis.of_vector_space_index 𝕜 E → 𝕜) →ₗ[𝕜] E))
+                      ∘ b.equiv_fun) := B.comp A,
   convert this,
   ext x,
   dsimp,
-  rw linear_equiv.symm_apply_apply
+  rw [basis.equiv_fun_symm_apply, basis.sum_repr]
 end
 
 theorem affine_map.continuous_of_finite_dimensional {PE PF : Type*}
@@ -269,40 +267,40 @@ def continuous_linear_equiv.of_finrank_eq [finite_dimensional 𝕜 E] [finite_di
 variables {ι : Type*} [fintype ι]
 
 /-- Construct a continuous linear map given the value at a finite basis. -/
-def is_basis.constrL {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) :
+def basis.constrL (v : basis ι 𝕜 E) (f : ι → F) :
   E →L[𝕜] F :=
-by haveI : finite_dimensional 𝕜 E := finite_dimensional.of_fintype_basis hv;
-  exact (hv.constr f).to_continuous_linear_map
+by haveI : finite_dimensional 𝕜 E := finite_dimensional.of_fintype_basis v;
+  exact (v.constr 𝕜 f).to_continuous_linear_map
 
-@[simp, norm_cast] lemma is_basis.coe_constrL {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) :
-  (hv.constrL f : E →ₗ[𝕜] F) = hv.constr f := rfl
+@[simp, norm_cast] lemma basis.coe_constrL (v : basis ι 𝕜 E) (f : ι → F) :
+  (v.constrL f : E →ₗ[𝕜] F) = v.constr 𝕜 f := rfl
 
 /-- The continuous linear equivalence between a vector space over `𝕜` with a finite basis and
 functions from its basis indexing type to `𝕜`. -/
-def is_basis.equiv_funL {v : ι → E} (hv : is_basis 𝕜 v) : E ≃L[𝕜] (ι → 𝕜) :=
+def basis.equiv_funL (v : basis ι 𝕜 E) : E ≃L[𝕜] (ι → 𝕜) :=
 { continuous_to_fun := begin
-    haveI : finite_dimensional 𝕜 E := finite_dimensional.of_fintype_basis hv,
+    haveI : finite_dimensional 𝕜 E := finite_dimensional.of_fintype_basis v,
     apply linear_map.continuous_of_finite_dimensional,
   end,
   continuous_inv_fun := begin
-    change continuous hv.equiv_fun.symm.to_fun,
+    change continuous v.equiv_fun.symm.to_fun,
     apply linear_map.continuous_of_finite_dimensional,
   end,
-  ..hv.equiv_fun }
+  ..v.equiv_fun }
 
 
-@[simp] lemma is_basis.constrL_apply {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) (e : E) :
-  (hv.constrL f) e = ∑ i, (hv.equiv_fun e i) • f i :=
-hv.constr_apply_fintype _ _
+@[simp] lemma basis.constrL_apply (v : basis ι 𝕜 E) (f : ι → F) (e : E) :
+  (v.constrL f) e = ∑ i, (v.equiv_fun e i) • f i :=
+v.constr_apply_fintype 𝕜 _ _
 
-@[simp] lemma is_basis.constrL_basis {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) (i : ι) :
-  (hv.constrL f) (v i) = f i :=
-constr_basis _
+@[simp] lemma basis.constrL_basis (v : basis ι 𝕜 E) (f : ι → F) (i : ι) :
+  (v.constrL f) (v i) = f i :=
+v.constr_basis 𝕜 _ _
 
-lemma is_basis.sup_norm_le_norm {v : ι → E} (hv : is_basis 𝕜 v) :
-  ∃ C > (0 : ℝ), ∀ e : E, ∑ i, ∥hv.equiv_fun e i∥ ≤ C * ∥e∥ :=
+lemma basis.sup_norm_le_norm (v : basis ι 𝕜 E) :
+  ∃ C > (0 : ℝ), ∀ e : E, ∑ i, ∥v.equiv_fun e i∥ ≤ C * ∥e∥ :=
 begin
-  set φ := hv.equiv_funL.to_continuous_linear_map,
+  set φ := v.equiv_funL.to_continuous_linear_map,
   set C := ∥φ∥ * (fintype.card ι),
   use [max C 1, lt_of_lt_of_le (zero_lt_one) (le_max_right C 1)],
   intros e,
@@ -315,23 +313,23 @@ begin
   ... ≤ max C 1 * ∥e∥ :  mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _)
 end
 
-lemma is_basis.op_norm_le  {ι : Type*} [fintype ι] {v : ι → E} (hv : is_basis 𝕜 v) :
+lemma basis.op_norm_le  {ι : Type*} [fintype ι] (v : basis ι 𝕜 E) :
   ∃ C > (0 : ℝ), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥u (v i)∥ ≤ M) → ∥u∥ ≤ C*M :=
 begin
-  obtain ⟨C, C_pos, hC⟩ : ∃ C > (0 : ℝ), ∀ (e : E), ∑ i, ∥hv.equiv_fun e i∥ ≤ C * ∥e∥,
-    from hv.sup_norm_le_norm,
+  obtain ⟨C, C_pos, hC⟩ : ∃ C > (0 : ℝ), ∀ (e : E), ∑ i, ∥v.equiv_fun e i∥ ≤ C * ∥e∥,
+    from v.sup_norm_le_norm,
   use [C, C_pos],
   intros u M hM hu,
   apply u.op_norm_le_bound (mul_nonneg (le_of_lt C_pos) hM),
   intros e,
   calc
-  ∥u e∥ = ∥u (∑ i, hv.equiv_fun e i • v i)∥ :  by conv_lhs { rw ← hv.equiv_fun_total e }
-  ... = ∥∑ i, (hv.equiv_fun e i) • (u $ v i)∥ :  by simp [u.map_sum, linear_map.map_smul]
-  ... ≤ ∑ i, ∥(hv.equiv_fun e i) • (u $ v i)∥ : norm_sum_le _ _
-  ... = ∑ i, ∥hv.equiv_fun e i∥ * ∥u (v i)∥ : by simp only [norm_smul]
-  ... ≤ ∑ i, ∥hv.equiv_fun e i∥ * M : finset.sum_le_sum (λ i hi,
+  ∥u e∥ = ∥u (∑ i, v.equiv_fun e i • v i)∥ :   by rw [v.sum_equiv_fun]
+  ... = ∥∑ i, (v.equiv_fun e i) • (u $ v i)∥ : by simp [u.map_sum, linear_map.map_smul]
+  ... ≤ ∑ i, ∥(v.equiv_fun e i) • (u $ v i)∥ : norm_sum_le _ _
+  ... = ∑ i, ∥v.equiv_fun e i∥ * ∥u (v i)∥ :   by simp only [norm_smul]
+  ... ≤ ∑ i, ∥v.equiv_fun e i∥ * M : finset.sum_le_sum (λ i hi,
                                                   mul_le_mul_of_nonneg_left (hu i) (norm_nonneg _))
-  ... = (∑ i, ∥hv.equiv_fun e i∥) * M : finset.sum_mul.symm
+  ... = (∑ i, ∥v.equiv_fun e i∥) * M : finset.sum_mul.symm
   ... ≤ C * ∥e∥ * M : mul_le_mul_of_nonneg_right (hC e) hM
   ... = C * M * ∥e∥ : by ring
 end
@@ -346,13 +344,13 @@ begin
     (λ ε ε_pos, ⟨fin d → ℕ, by apply_instance, this ε ε_pos⟩),
   intros ε ε_pos,
   obtain ⟨u : ℕ → F, hu : dense_range u⟩ := exists_dense_seq F,
-  obtain ⟨v : fin d → E, hv : is_basis 𝕜 v⟩ := finite_dimensional.fin_basis 𝕜 E,
+  let v := finite_dimensional.fin_basis 𝕜 E,
   obtain ⟨C : ℝ, C_pos : 0 < C,
           hC : ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥φ (v i)∥ ≤ M) → ∥φ∥ ≤ C * M⟩ :=
-    hv.op_norm_le,
+    v.op_norm_le,
   have h_2C : 0 < 2*C := mul_pos zero_lt_two C_pos,
   have hε2C : 0 < ε/(2*C) := div_pos ε_pos h_2C,
-  have : ∀ φ : E →L[𝕜] F, ∃ n : fin d → ℕ, ∥φ - (hv.constrL $ u ∘ n)∥ ≤ ε/2,
+  have : ∀ φ : E →L[𝕜] F, ∃ n : fin d → ℕ, ∥φ - (v.constrL $ u ∘ n)∥ ≤ ε/2,
   { intros φ,
     have : ∀ i, ∃ n, ∥φ (v i) - u n∥ ≤ ε/(2*C),
     { simp only [norm_sub_rev],
@@ -365,14 +363,14 @@ begin
       exact ⟨n, le_of_lt hn⟩ },
     choose n hn using this,
     use n,
-    replace hn : ∀ i : fin d, ∥(φ - (hv.constrL $ u ∘ n)) (v i)∥ ≤ ε / (2 * C), by simp [hn],
+    replace hn : ∀ i : fin d, ∥(φ - (v.constrL $ u ∘ n)) (v i)∥ ≤ ε / (2 * C), by simp [hn],
     have : C * (ε / (2 * C)) = ε/2,
     { rw [eq_div_iff (two_ne_zero : (2 : ℝ) ≠ 0), mul_comm, ← mul_assoc,
           mul_div_cancel' _ (ne_of_gt h_2C)] },
     specialize hC (le_of_lt hε2C) hn,
     rwa this at hC },
   choose n hn using this,
-  set Φ := λ φ : E →L[𝕜] F, (hv.constrL $ u ∘ (n φ)),
+  set Φ := λ φ : E →L[𝕜] F, (v.constrL $ u ∘ (n φ)),
   change ∀ z, dist z (Φ z) ≤ ε/2 at hn,
   use n,
   intros x y hxy,
@@ -465,8 +463,8 @@ begin
   refine ⟨summable_of_summable_norm, λ hf, _⟩,
   -- First we use a finite basis to reduce the problem to the case `E = fin N → ℝ`
   suffices : ∀ {N : ℕ} {g : α → fin N → ℝ}, summable g → summable (λ x, ∥g x∥),
-  { rcases fin_basis ℝ E with ⟨v, hv⟩,
-    set e := hv.equiv_funL,
+  { obtain v := fin_basis ℝ E,
+    set e := v.equiv_funL,
     have : summable (λ x, ∥e (f x)∥) := this (e.summable.2 hf),
     refine summable_of_norm_bounded _ (this.mul_left
       ↑(nnnorm (e.symm : (fin (finrank ℝ E) → ℝ) →L[ℝ] E))) (λ i, _),