refactor(linear_algebra, analysis/inner_product_space): use ⊤ ≤ ins…

…tead of `= ⊤` in bases constructors (#15697)

All the existing proof just need a `.ge` to be fixed, and this allows to remove a lot of `rw [eq_top_iff]`, and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors

src/analysis/fourier.lean

@@ -215,7 +215,7 @@ section fourier
 /-- We define `fourier_series` to be a `ℤ`-indexed Hilbert basis for `Lp ℂ 2 haar_circle`, which by
 definition is an isometric isomorphism from `Lp ℂ 2 haar_circle` to `ℓ²(ℤ, ℂ)`. -/
 def fourier_series : hilbert_basis ℤ ℂ (Lp ℂ 2 haar_circle) :=
-hilbert_basis.mk orthonormal_fourier (span_fourier_Lp_closure_eq_top (by norm_num))
+hilbert_basis.mk orthonormal_fourier (span_fourier_Lp_closure_eq_top (by norm_num)).ge
 
 /-- The elements of the Hilbert basis `fourier_series` for `Lp ℂ 2 haar_circle` are the functions
 `fourier_Lp 2`, the monomials `λ z, z ^ n` on the circle considered as elements of `L2`. -/

src/analysis/inner_product_space/gram_schmidt_ortho.lean

@@ -202,7 +202,7 @@ linear_independent_of_ne_zero_of_inner_eq_zero
 noncomputable def gram_schmidt_basis (b : basis ι 𝕜 E) : basis ι 𝕜 E :=
 basis.mk
   (gram_schmidt_linear_independent 𝕜 b b.linear_independent)
-  ((span_gram_schmidt 𝕜 b).trans b.span_eq)
+  ((span_gram_schmidt 𝕜 b).trans b.span_eq).ge
 
 lemma coe_gram_schmidt_basis (b : basis ι 𝕜 E) :
   (gram_schmidt_basis 𝕜 b : ι → E) = gram_schmidt 𝕜 b := basis.coe_mk _ _
@@ -259,4 +259,4 @@ noncomputable def gram_schmidt_orthonormal_basis [fintype ι] (b : basis ι 𝕜
   orthonormal_basis ι 𝕜 E :=
 orthonormal_basis.mk
   (gram_schmidt_orthonormal 𝕜 b b.linear_independent)
-  (((span_gram_schmidt_normed_range 𝕜 b).trans (span_gram_schmidt 𝕜 b)).trans b.span_eq)
+  (((span_gram_schmidt_normed_range 𝕜 b).trans (span_gram_schmidt 𝕜 b)).trans b.span_eq).ge

src/analysis/inner_product_space/l2_space.lean

@@ -247,38 +247,36 @@ a isometric isomorphism from E to `lp 2` of the subspaces.
 
 Note that this goes in the opposite direction from `orthogonal_family.linear_isometry`. -/
 noncomputable def linear_isometry_equiv [Π i, complete_space (G i)]
-  (hV' : (⨆ i, (V i).to_linear_map.range).topological_closure = ⊤) :
+  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) :
   E ≃ₗᵢ[𝕜] lp G 2 :=
 linear_isometry_equiv.symm $
 linear_isometry_equiv.of_surjective
 hV.linear_isometry
 begin
   rw [←linear_isometry.coe_to_linear_map],
-  refine linear_map.range_eq_top.mp _,
-  rw ← hV',
-  rw hV.range_linear_isometry,
+  exact linear_map.range_eq_top.mp (eq_top_iff.mpr $ hV'.trans_eq hV.range_linear_isometry.symm)
 end
 
 /-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an orthogonal family `G`,
 a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`. -/
 protected lemma linear_isometry_equiv_symm_apply [Π i, complete_space (G i)]
-  (hV' : (⨆ i, (V i).to_linear_map.range).topological_closure = ⊤) (w : lp G 2) :
+  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (w : lp G 2) :
   (hV.linear_isometry_equiv hV').symm w = ∑' i, V i (w i) :=
 by simp [orthogonal_family.linear_isometry_equiv, orthogonal_family.linear_isometry_apply]
 
 /-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an orthogonal family `G`,
 a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`, and this
 sum indeed converges. -/
 protected lemma has_sum_linear_isometry_equiv_symm [Π i, complete_space (G i)]
-  (hV' : (⨆ i, (V i).to_linear_map.range).topological_closure = ⊤) (w : lp G 2) :
+  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (w : lp G 2) :
   has_sum (λ i, V i (w i)) ((hV.linear_isometry_equiv hV').symm w) :=
 by simp [orthogonal_family.linear_isometry_equiv, orthogonal_family.has_sum_linear_isometry]
 
 /-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an `ι`-indexed orthogonal
 family `G`, an "elementary basis vector" in `lp G 2` supported at `i : ι` is the image of the
 associated element in `E`. -/
 @[simp] protected lemma linear_isometry_equiv_symm_apply_single [Π i, complete_space (G i)]
-  (hV' : (⨆ i, (V i).to_linear_map.range).topological_closure = ⊤) {i : ι} (x : G i) :
+  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) {i : ι} (x : G i) :
   (hV.linear_isometry_equiv hV').symm (lp.single 2 i x) = V i x :=
 by simp [orthogonal_family.linear_isometry_equiv, orthogonal_family.linear_isometry_apply_single]
 
@@ -287,7 +285,7 @@ family `G`, a finitely-supported vector in `lp G 2` is the image of the associat
 elements of `E`. -/
 @[simp] protected lemma linear_isometry_equiv_symm_apply_dfinsupp_sum_single
   [Π i, complete_space (G i)]
-  (hV' : (⨆ i, (V i).to_linear_map.range).topological_closure = ⊤) (W₀ : Π₀ (i : ι), G i) :
+  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (W₀ : Π₀ (i : ι), G i) :
   (hV.linear_isometry_equiv hV').symm (W₀.sum (lp.single 2)) = (W₀.sum (λ i, V i)) :=
 by simp [orthogonal_family.linear_isometry_equiv,
   orthogonal_family.linear_isometry_apply_dfinsupp_sum_single]
@@ -297,7 +295,7 @@ family `G`, a finitely-supported vector in `lp G 2` is the image of the associat
 elements of `E`. -/
 @[simp] protected lemma linear_isometry_equiv_apply_dfinsupp_sum_single
   [Π i, complete_space (G i)]
-  (hV' : (⨆ i, (V i).to_linear_map.range).topological_closure = ⊤) (W₀ : Π₀ (i : ι), G i) :
+  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (W₀ : Π₀ (i : ι), G i) :
   (hV.linear_isometry_equiv hV' (W₀.sum (λ i, V i)) : Π i, G i) = W₀ :=
 begin
   rw ← hV.linear_isometry_equiv_symm_apply_dfinsupp_sum_single hV',
@@ -411,6 +409,7 @@ protected def to_orthonormal_basis [fintype ι] (b : hilbert_basis ι 𝕜 E) :
   orthonormal_basis ι 𝕜 E :=
 orthonormal_basis.mk b.orthonormal
 begin
+  refine eq.ge _,
   have := (span 𝕜 (finset.univ.image b : set E)).closed_of_finite_dimensional,
   simpa only [finset.coe_image, finset.coe_univ, set.image_univ, hilbert_basis.dense_span] using
     this.submodule_topological_closure_eq.symm
@@ -424,7 +423,7 @@ variables {v : ι → E} (hv : orthonormal 𝕜 v)
 include hv cplt
 
 /-- An orthonormal family of vectors whose span is dense in the whole module is a Hilbert basis. -/
-protected def mk (hsp : (span 𝕜 (set.range v)).topological_closure = ⊤) :
+protected def mk (hsp : ⊤ ≤ (span 𝕜 (set.range v)).topological_closure) :
   hilbert_basis ι 𝕜 E :=
 hilbert_basis.of_repr $
 hv.orthogonal_family.linear_isometry_equiv
@@ -438,15 +437,15 @@ lemma _root_.orthonormal.linear_isometry_equiv_symm_apply_single_one (h i) :
 by rw [orthogonal_family.linear_isometry_equiv_symm_apply_single,
   linear_isometry.to_span_singleton_apply, one_smul]
 
-@[simp] protected lemma coe_mk (hsp : (span 𝕜 (set.range v)).topological_closure = ⊤) :
+@[simp] protected lemma coe_mk (hsp : ⊤ ≤ (span 𝕜 (set.range v)).topological_closure) :
   ⇑(hilbert_basis.mk hv hsp) = v :=
 funext $ orthonormal.linear_isometry_equiv_symm_apply_single_one hv _
 
 /-- An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert
 basis. -/
 protected def mk_of_orthogonal_eq_bot (hsp : (span 𝕜 (set.range v))ᗮ = ⊥) : hilbert_basis ι 𝕜 E :=
 hilbert_basis.mk hv
-(by rw [← orthogonal_orthogonal_eq_closure, orthogonal_eq_top_iff, hsp])
+(by rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp])
 
 @[simp] protected lemma coe_of_orthogonal_eq_bot_mk (hsp : (span 𝕜 (set.range v))ᗮ = ⊥) :
   ⇑(hilbert_basis.mk_of_orthogonal_eq_bot hv hsp) = v :=

src/analysis/inner_product_space/pi_L2.lean

@@ -386,12 +386,12 @@ calc (v.to_orthonormal_basis hv : ι → E) = ((v.to_orthonormal_basis hv).to_ba
 variable {v : ι → E}
 
 /-- A finite orthonormal set that spans is an orthonormal basis -/
-protected def mk (hon : orthonormal 𝕜 v) (hsp: submodule.span 𝕜 (set.range v) = ⊤):
+protected def mk (hon : orthonormal 𝕜 v) (hsp: ⊤ ≤ submodule.span 𝕜 (set.range v)):
   orthonormal_basis ι 𝕜 E :=
 (basis.mk (orthonormal.linear_independent hon) hsp).to_orthonormal_basis (by rwa basis.coe_mk)
 
 @[simp]
-protected lemma coe_mk (hon : orthonormal 𝕜 v) (hsp: submodule.span 𝕜 (set.range v) = ⊤) :
+protected lemma coe_mk (hon : orthonormal 𝕜 v) (hsp: ⊤ ≤ submodule.span 𝕜 (set.range v)) :
   ⇑(orthonormal_basis.mk hon hsp) = v :=
 by classical; rw [orthonormal_basis.mk, _root_.basis.coe_to_orthonormal_basis, basis.coe_mk]
 
@@ -405,7 +405,7 @@ let
       convert orthonormal_span (h.comp (coe : s → ι') subtype.coe_injective),
       ext,
       simp [e₀', basis.span_apply],
-    end e₀'.span_eq,
+    end e₀'.span_eq.ge,
   φ : span 𝕜 (s.image v' : set E) ≃ₗᵢ[𝕜] span 𝕜 (range (v' ∘ (coe : s → ι'))) :=
     linear_isometry_equiv.of_eq _ _
     begin
@@ -429,6 +429,7 @@ protected def mk_of_orthogonal_eq_bot (hon : orthonormal 𝕜 v) (hsp : (span 
   orthonormal_basis ι 𝕜 E :=
 orthonormal_basis.mk hon
 begin
+  refine eq.ge _,
   haveI : finite_dimensional 𝕜 (span 𝕜 (range v)) :=
     finite_dimensional.span_of_finite 𝕜 (finite_range v),
   haveI : complete_space (span 𝕜 (range v)) := finite_dimensional.complete 𝕜 _,

src/analysis/inner_product_space/projection.lean

@@ -1143,7 +1143,7 @@ begin
   have hv_coe : range (coe : v → E) = v := by simp,
   split,
   { refine λ h, ⟨basis.mk hv.linear_independent _, basis.coe_mk _ _⟩,
-    convert h },
+    convert h.ge },
   { rintros ⟨h, coe_h⟩,
     rw [← h.span_eq, coe_h, hv_coe] }
 end

src/linear_algebra/affine_space/basis.lean

@@ -76,7 +76,7 @@ basis.mk ((affine_independent_iff_linear_independent_vsub k b.points i).mp b.ind
 begin
   suffices : submodule.span k (range (λ (j : {x // x ≠ i}), b.points ↑j -ᵥ b.points i)) =
              vector_span k (range b.points),
-  { rw [this, ← direction_affine_span, b.tot, affine_subspace.direction_top], },
+  { rw [this, ← direction_affine_span, b.tot, affine_subspace.direction_top], exact le_rfl },
   conv_rhs { rw ← image_univ, },
   rw vector_span_image_eq_span_vsub_set_right_ne k b.points (mem_univ i),
   congr,

src/linear_algebra/basis.lean

@@ -898,18 +898,18 @@ end
 
 section mk
 
-variables (hli : linear_independent R v) (hsp : span R (range v) = ⊤)
+variables (hli : linear_independent R v) (hsp : ⊤ ≤ span R (range v))
 
 /-- A linear independent family of vectors spanning the whole module is a basis. -/
 protected noncomputable def mk : basis ι R M :=
 basis.of_repr
 { inv_fun := finsupp.total _ _ _ v,
   left_inv := λ x, hli.total_repr ⟨x, _⟩,
   right_inv := λ x, hli.repr_eq rfl,
-  .. hli.repr.comp (linear_map.id.cod_restrict _ (λ h, hsp.symm ▸ submodule.mem_top)) }
+  .. hli.repr.comp (linear_map.id.cod_restrict _ (λ h, hsp submodule.mem_top)) }
 
 @[simp] lemma mk_repr :
-  (basis.mk hli hsp).repr x = hli.repr ⟨x, hsp.symm ▸ submodule.mem_top⟩ :=
+  (basis.mk hli hsp).repr x = hli.repr ⟨x, hsp submodule.mem_top⟩ :=
 rfl
 
 lemma mk_apply (i : ι) : basis.mk hli hsp i = v i :=
@@ -954,7 +954,6 @@ variables (hli : linear_independent R v)
 protected noncomputable def span : basis ι R (span R (range v)) :=
 basis.mk (linear_independent_span hli) $
 begin
-  rw eq_top_iff,
   intros x _,
   have h₁ : (coe : span R (range v) → M) '' set.range (λ i, subtype.mk (v i) _) = range v,
   { rw ← set.range_comp,
@@ -996,13 +995,13 @@ def group_smul {G : Type*} [group G] [distrib_mul_action G R] [distrib_mul_actio
   [is_scalar_tower G R M] [smul_comm_class G R M] (v : basis ι R M) (w : ι → G) :
   basis ι R M :=
 @basis.mk ι R M (w • v) _ _ _
-  (v.linear_independent.group_smul w) (group_smul_span_eq_top v.span_eq)
+  (v.linear_independent.group_smul w) (group_smul_span_eq_top v.span_eq).ge
 
 lemma group_smul_apply {G : Type*} [group G] [distrib_mul_action G R] [distrib_mul_action G M]
   [is_scalar_tower G R M] [smul_comm_class G R M] {v : basis ι R M} {w : ι → G} (i : ι) :
   v.group_smul w i = (w • v : ι → M) i :=
 mk_apply
-  (v.linear_independent.group_smul w) (group_smul_span_eq_top v.span_eq) i
+  (v.linear_independent.group_smul w) (group_smul_span_eq_top v.span_eq).ge i
 
 lemma units_smul_span_eq_top {v : ι → M} (hv : submodule.span R (set.range v) = ⊤)
   {w : ι → Rˣ} : submodule.span R (set.range (w • v)) = ⊤ :=
@@ -1013,12 +1012,12 @@ provides the basis corresponding to `w • v`. -/
 def units_smul (v : basis ι R M) (w : ι → Rˣ) :
   basis ι R M :=
 @basis.mk ι R M (w • v) _ _ _
-  (v.linear_independent.units_smul w) (units_smul_span_eq_top v.span_eq)
+  (v.linear_independent.units_smul w) (units_smul_span_eq_top v.span_eq).ge
 
 lemma units_smul_apply {v : basis ι R M} {w : ι → Rˣ} (i : ι) :
   v.units_smul w i = w i • v i :=
 mk_apply
-  (v.linear_independent.units_smul w) (units_smul_span_eq_top v.span_eq) i
+  (v.linear_independent.units_smul w) (units_smul_span_eq_top v.span_eq).ge i
 
 /-- A version of `smul_of_units` that uses `is_unit`. -/
 def is_unit_smul (v : basis ι R M) {w : ι → R} (hw : ∀ i, is_unit (w i)):
@@ -1043,8 +1042,7 @@ have span_b : submodule.span R (set.range (N.subtype ∘ b)) = N,
 @basis.mk _ _ _ (fin.cons y (N.subtype ∘ b) : fin (n + 1) → M) _ _ _
   ((b.linear_independent.map' N.subtype (submodule.ker_subtype _)) .fin_cons' _ _ $
     by { rintros c ⟨x, hx⟩ hc, rw span_b at hx, exact hli c x hx hc })
-  (eq_top_iff.mpr (λ x _,
-    by { rw [fin.range_cons, submodule.mem_span_insert', span_b], exact hsp x }))
+  (λ x _, by { rw [fin.range_cons, submodule.mem_span_insert', span_b], exact hsp x })
 
 @[simp] lemma coe_mk_fin_cons {n : ℕ} {N : submodule R M} (y : M) (b : basis (fin n) R N)
   (hli : ∀ (c : R) (x ∈ N), c • y + x = 0 → c = 0)
@@ -1151,8 +1149,7 @@ noncomputable def extend (hs : linear_independent K (coe : s → V)) :
   basis _ K V :=
 basis.mk
   (@linear_independent.restrict_of_comp_subtype _ _ _ id _ _ _ _ (hs.linear_independent_extend _))
-  (eq_top_iff.mpr $ set_like.coe_subset_coe.mp $
-    by simpa using hs.subset_span_extend (subset_univ s))
+  (set_like.coe_subset_coe.mp $ by simpa using hs.subset_span_extend (subset_univ s))
 
 lemma extend_apply_self (hs : linear_independent K (coe : s → V))
   (x : hs.extend _) :

src/linear_algebra/determinant.lean

@@ -464,7 +464,7 @@ lemma is_basis_iff_det {v : ι → M} :
 begin
   split,
   { rintro ⟨hli, hspan⟩,
-    set v' := basis.mk hli hspan with v'_eq,
+    set v' := basis.mk hli hspan.ge with v'_eq,
     rw e.det_apply,
     convert linear_equiv.is_unit_det (linear_equiv.refl _ _) v' e using 2,
     ext i j,
@@ -535,7 +535,7 @@ end
 /-- If we fix a background basis `e`, then for any other basis `v`, we can characterise the
 coordinates provided by `v` in terms of determinants relative to `e`. -/
 lemma basis.det_smul_mk_coord_eq_det_update {v : ι → M}
-  (hli : linear_independent R v) (hsp : span R (range v) = ⊤) (i : ι) :
+  (hli : linear_independent R v) (hsp : ⊤ ≤ span R (range v)) (i : ι) :
   (e.det v) • (basis.mk hli hsp).coord i = e.det.to_multilinear_map.to_linear_map v i :=
 begin
   apply (basis.mk hli hsp).ext,