[Merged by Bors] - refactor(linear_algebra/finsupp): replace mem_span_iff_total

src/algebraic_geometry/structure_sheaf.lean

@@ -709,7 +709,7 @@ begin
     exact subset_vanishing_ideal_zero_locus {f} (set.mem_singleton f) },
 
   replace hn := ideal.mul_mem_left _ f hn,
-  erw [←pow_succ, finsupp.mem_span_iff_total] at hn,
+  erw [←pow_succ, finsupp.mem_span_image_iff_total] at hn,
   rcases hn with ⟨b, b_supp, hb⟩,
   rw finsupp.total_apply_of_mem_supported R b_supp at hb,
   dsimp at hb,

src/analysis/normed_space/inner_product.lean

@@ -2739,7 +2739,7 @@ begin
       have hxv' : (⟨x, hxu⟩ : u) ∉ (coe ⁻¹' v : set u) := by simp [huv, hxv],
       obtain ⟨l, hl, rfl⟩ :
         ∃ l ∈ finsupp.supported 𝕜 𝕜 (coe ⁻¹' v : set u), (finsupp.total ↥u E 𝕜 coe) l = y,
-      { rw ← finsupp.mem_span_iff_total,
+      { rw ← finsupp.mem_span_image_iff_total,
         simp [huv, inter_eq_self_of_subset_left, hy] },
       exact hu.inner_finsupp_eq_zero hxv' hl }
 end

src/field_theory/algebraic_closure.lean

@@ -156,7 +156,8 @@ by { rw [to_splitting_field, eval_X_self, ← alg_hom.coe_to_ring_hom, hom_eval
 
 theorem span_eval_ne_top : span_eval k ≠ ⊤ :=
 begin
-  rw [ideal.ne_top_iff_one, span_eval, ideal.span, ← set.image_univ, finsupp.mem_span_iff_total],
+  rw [ideal.ne_top_iff_one, span_eval, ideal.span, ← set.image_univ,
+    finsupp.mem_span_image_iff_total],
   rintros ⟨v, _, hv⟩,
   replace hv := congr_arg (to_splitting_field k v.support) hv,
   rw [alg_hom.map_one, finsupp.total_apply, finsupp.sum, alg_hom.map_sum, finset.sum_eq_zero] at hv,

src/field_theory/fixed.lean

@@ -78,7 +78,7 @@ begin
   rw coe_insert at hs ⊢,
   rw linear_independent_insert (mt mem_coe.1 has) at hs,
   rw linear_independent_insert' (mt mem_coe.1 has), refine ⟨ih hs.1, λ ha, _⟩,
-  rw finsupp.mem_span_iff_total at ha, rcases ha with ⟨l, hl, hla⟩,
+  rw finsupp.mem_span_image_iff_total at ha, rcases ha with ⟨l, hl, hla⟩,
   rw [finsupp.total_apply_of_mem_supported F hl] at hla,
   suffices : ∀ i ∈ s, l i ∈ fixed_points G F,
   { replace hla := (sum_apply _ _ (λ i, l i • to_fun G F i)).symm.trans (congr_fun hla 1),

src/linear_algebra/affine_space/combination.lean

@@ -537,7 +537,7 @@ begin
   by_cases hn : nonempty ι,
   { cases hn with i0,
     rw [vector_span_range_eq_span_range_vsub_right k p i0, ←set.image_univ,
-        finsupp.mem_span_iff_total,
+        finsupp.mem_span_image_iff_total,
         finset.weighted_vsub_eq_weighted_vsub_of_point_of_sum_eq_zero s w p h (p i0),
         finset.weighted_vsub_of_point_apply],
     let w' := set.indicator ↑s w,
@@ -587,7 +587,7 @@ begin
   { by_cases hn : nonempty ι,
     { cases hn with i0,
       rw [vector_span_range_eq_span_range_vsub_right k p i0, ←set.image_univ,
-          finsupp.mem_span_iff_total],
+          finsupp.mem_span_image_iff_total],
       rintros ⟨l, hl, hv⟩,
       use insert i0 l.support,
       set w := (l : ι → k) -

src/linear_algebra/basis.lean

@@ -395,7 +395,7 @@ lemma constr_range [nonempty ι] {f : ι  → M'} :
   (b.constr S f).range = span R (range f) :=
 by rw [b.constr_def S f, linear_map.range_comp, linear_map.range_comp, linear_equiv.range,
        ← finsupp.supported_univ, finsupp.lmap_domain_supported, ←set.image_univ,
-       ← finsupp.span_eq_map_total, set.image_id]
+       ← finsupp.span_image_eq_map_total, set.image_id]
 
 end constr
 

src/linear_algebra/dual.lean

@@ -388,7 +388,7 @@ lemma mem_of_mem_span {H : set ι} {x : M} (hmem : x ∈ submodule.span R (e ''
   ∀ i : ι, ε i x ≠ 0 → i ∈ H :=
 begin
   intros i hi,
-  rcases (finsupp.mem_span_iff_total _).mp hmem with ⟨l, supp_l, rfl⟩,
+  rcases (finsupp.mem_span_image_iff_total _).mp hmem with ⟨l, supp_l, rfl⟩,
   apply not_imp_comm.mp ((finsupp.mem_supported' _ _).mp supp_l i),
   rwa [← lc_def, h.dual_lc] at hi
 end

src/linear_algebra/finsupp.lean

@@ -476,7 +476,16 @@ begin
   apply total_emb_domain R ⟨f, hf⟩ l
 end
 
-theorem span_eq_map_total (s : set α):
+/-- A version of `finsupp.range_total` which is useful for going in the other direction -/
+theorem span_eq_range_total (s : set M) :
+  span R s = (finsupp.total s M R coe).range :=
+by rw [range_total, subtype.range_coe_subtype, set.set_of_mem_eq]
+
+theorem mem_span_iff_total (s : set M) (x : M) :
+  x ∈ span R s ↔ ∃ l : s →₀ R, finsupp.total s M R coe l = x :=
+(set_like.ext_iff.1 $ span_eq_range_total _ _) x
+
+theorem span_image_eq_map_total (s : set α):
   span R (v '' s) = submodule.map (finsupp.total α M R v) (supported R R s) :=
 begin
   apply span_eq_of_le,
@@ -495,9 +504,9 @@ begin
     refine sum_mem _ _, simp [this] }
 end
 
-theorem mem_span_iff_total {s : set α} {x : M} :
+theorem mem_span_image_iff_total {s : set α} {x : M} :
   x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, finsupp.total α M R v l = x :=
-by rw span_eq_map_total; simp
+by { rw span_image_eq_map_total, simp, }
 
 variables (α) (M) (v)
 
@@ -508,15 +517,15 @@ The subset is indicated by a set `s : set α` of indices.
 -/
 protected def total_on (s : set α) : supported R R s →ₗ[R] span R (v '' s) :=
 linear_map.cod_restrict _ ((finsupp.total _ _ _ v).comp (submodule.subtype (supported R R s))) $
-  λ ⟨l, hl⟩, (mem_span_iff_total _).2 ⟨l, hl, rfl⟩
+  λ ⟨l, hl⟩, (mem_span_image_iff_total _).2 ⟨l, hl, rfl⟩
 
 variables {α} {M} {v}
 
 theorem total_on_range (s : set α) : (finsupp.total_on α M R v s).range = ⊤ :=
 begin
   rw [finsupp.total_on, linear_map.range_eq_map, linear_map.map_cod_restrict,
     ← linear_map.range_le_iff_comap, range_subtype, map_top, linear_map.range_comp, range_subtype],
-  exact (span_eq_map_total _ _).le
+  exact (span_image_eq_map_total _ _).le
 end
 
 theorem total_comp (f : α' → α) :
@@ -771,7 +780,7 @@ lemma submodule.exists_finset_of_mem_supr
 begin
   obtain ⟨f, hf, rfl⟩ : ∃ f ∈ finsupp.supported R R (⋃ i, ↑(p i)), finsupp.total M M R id f = m,
   { have aux : (id : M → M) '' (⋃ (i : ι), ↑(p i)) = (⋃ (i : ι), ↑(p i)) := set.image_id _,
-    rwa [supr_eq_span, ← aux, finsupp.mem_span_iff_total R] at hm },
+    rwa [supr_eq_span, ← aux, finsupp.mem_span_image_iff_total R] at hm },
   let t : finset M := f.support,
   have ht : ∀ x : {x // x ∈ t}, ∃ i, ↑x ∈ p i,
   { intros x,
@@ -794,7 +803,7 @@ end
 
 lemma mem_span_finset {s : finset M} {x : M} :
   x ∈ span R (↑s : set M) ↔ ∃ f : M → R, ∑ i in s, f i • i = x :=
-⟨λ hx, let ⟨v, hvs, hvx⟩ := (finsupp.mem_span_iff_total _).1
+⟨λ hx, let ⟨v, hvs, hvx⟩ := (finsupp.mem_span_image_iff_total _).1
     (show x ∈ span R (id '' (↑s : set M)), by rwa set.image_id) in
   ⟨v, hvx ▸ (finsupp.total_apply_of_mem_supported _ hvs).symm⟩,
 λ ⟨f, hf⟩, hf ▸ sum_mem _ (λ i hi, smul_mem _ _ $ subset_span hi)⟩
@@ -807,7 +816,7 @@ lemma mem_span_set {m : M} {s : set M} :
 begin
   conv_lhs { rw ←set.image_id s },
   simp_rw ←exists_prop,
-  exact finsupp.mem_span_iff_total R,
+  exact finsupp.mem_span_image_iff_total R,
 end
 
 /-- If `subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/

src/linear_algebra/linear_independent.lean

@@ -186,7 +186,7 @@ family of vectors. See also `linear_independent.map'` for a special case assumin
 lemma linear_independent.map (hv : linear_independent R v) {f : M →ₗ[R] M'}
   (hf_inj : disjoint (span R (range v)) f.ker) : linear_independent R (f ∘ v) :=
 begin
-  rw [disjoint, ← set.image_univ, finsupp.span_eq_map_total, map_inf_eq_map_inf_comap,
+  rw [disjoint, ← set.image_univ, finsupp.span_image_eq_map_total, map_inf_eq_map_inf_comap,
     map_le_iff_le_comap, comap_bot, finsupp.supported_univ, top_inf_eq] at hf_inj,
   unfold linear_independent at hv ⊢,
   rw [hv, le_bot_iff] at hf_inj,
@@ -453,7 +453,7 @@ lemma linear_independent.disjoint_span_image (hv : linear_independent R v) {s t
   (hs : disjoint s t) :
   disjoint (submodule.span R $ v '' s) (submodule.span R $ v '' t) :=
 begin
-  simp only [disjoint_def, finsupp.mem_span_iff_total],
+  simp only [disjoint_def, finsupp.mem_span_image_iff_total],
   rintros _ ⟨l₁, hl₁, rfl⟩ ⟨l₂, hl₂, H⟩,
   rw [hv.injective_total.eq_iff] at H, subst l₂,
   have : l₁ = 0 := finsupp.disjoint_supported_supported hs (submodule.mem_inf.2 ⟨hl₁, hl₂⟩),
@@ -621,7 +621,7 @@ end
 lemma linear_independent_iff_not_smul_mem_span :
   linear_independent R v ↔ (∀ (i : ι) (a : R), a • (v i) ∈ span R (v '' (univ \ {i})) → a = 0) :=
 ⟨ λ hv i a ha, begin
-  rw [finsupp.span_eq_map_total, mem_map] at ha,
+  rw [finsupp.span_image_eq_map_total, mem_map] at ha,
   rcases ha with ⟨l, hl, e⟩,
   rw sub_eq_zero.1 (linear_independent_iff.1 hv (l - finsupp.single i a) (by simp [e])) at hl,
   by_contra hn,
@@ -630,7 +630,7 @@ end, λ H, linear_independent_iff.2 $ λ l hl, begin
   ext i, simp only [finsupp.zero_apply],
   by_contra hn,
   refine hn (H i _ _),
-  refine (finsupp.mem_span_iff_total _).2 ⟨finsupp.single i (l i) - l, _, _⟩,
+  refine (finsupp.mem_span_image_iff_total _).2 ⟨finsupp.single i (l i) - l, _, _⟩,
   { rw finsupp.mem_supported',
     intros j hj,
     have hij : j = i :=

src/ring_theory/adjoin/basic.lean

@@ -194,14 +194,14 @@ begin
     change r ∈ (adjoin (adjoin R s) t).to_submodule at hr,
     haveI := classical.dec_eq A,
     haveI := classical.dec_eq R,
-    rw [← hq', ← set.image_id q, finsupp.mem_span_iff_total (adjoin R s)] at hr,
+    rw [← hq', ← set.image_id q, finsupp.mem_span_image_iff_total (adjoin R s)] at hr,
     rcases hr with ⟨l, hlq, rfl⟩,
     have := @finsupp.total_apply A A (adjoin R s),
     rw [this, finsupp.sum],
     refine sum_mem _ _,
     intros z hz, change (l z).1 * _ ∈ _,
     have : (l z).1 ∈ (adjoin R s).to_submodule := (l z).2,
-    rw [← hp', ← set.image_id p, finsupp.mem_span_iff_total R] at this,
+    rw [← hp', ← set.image_id p, finsupp.mem_span_image_iff_total R] at this,
     rcases this with ⟨l2, hlp, hl⟩,
     have := @finsupp.total_apply A A R,
     rw this at hl,

src/ring_theory/integral_closure.lean

@@ -192,12 +192,12 @@ begin
   cases HS with y hy,
   obtain ⟨lx, hlx1, hlx2⟩ :
     ∃ (l : A →₀ R) (H : l ∈ finsupp.supported R R ↑y), (finsupp.total A A R id) l = x,
-  { rwa [←(@finsupp.mem_span_iff_total A A R _ _ _ id ↑y x), set.image_id ↑y, hy] },
+  { rwa [←(@finsupp.mem_span_image_iff_total A A R _ _ _ id ↑y x), set.image_id ↑y, hy] },
   have hyS : ∀ {p}, p ∈ y → p ∈ S := λ p hp, show p ∈ S.to_submodule,
     by { rw ← hy, exact subset_span hp },
   have : ∀ (jk : (↑(y.product y) : set (A × A))), jk.1.1 * jk.1.2 ∈ S.to_submodule :=
     λ jk, S.mul_mem (hyS (finset.mem_product.1 jk.2).1) (hyS (finset.mem_product.1 jk.2).2),
-  rw [← hy, ← set.image_id ↑y] at this, simp only [finsupp.mem_span_iff_total] at this,
+  rw [← hy, ← set.image_id ↑y] at this, simp only [finsupp.mem_span_image_iff_total] at this,
   choose ly hly1 hly2,
   let S₀ : set R := ring.closure ↑(lx.frange ∪ finset.bUnion finset.univ (finsupp.frange ∘ ly)),
   refine is_integral_of_subring S₀ _,

src/ring_theory/noetherian.lean

@@ -203,13 +203,13 @@ begin
       exact this.1 } },
   intros x hx,
   have : f x ∈ map f s, { rw mem_map, exact ⟨x, hx, rfl⟩ },
-  rw [← ht1,← set.image_id ↑t1, finsupp.mem_span_iff_total] at this,
+  rw [← ht1,← set.image_id ↑t1, finsupp.mem_span_image_iff_total] at this,
   rcases this with ⟨l, hl1, hl2⟩,
   refine mem_sup.2 ⟨(finsupp.total M M R id).to_fun
     ((finsupp.lmap_domain R R g : (P →₀ R) → M →₀ R) l), _,
     x - finsupp.total M M R id ((finsupp.lmap_domain R R g : (P →₀ R) → M →₀ R) l),
     _, add_sub_cancel'_right _ _⟩,
-  { rw [← set.image_id (g '' ↑t1), finsupp.mem_span_iff_total], refine ⟨_, _, rfl⟩,
+  { rw [← set.image_id (g '' ↑t1), finsupp.mem_span_image_iff_total], refine ⟨_, _, rfl⟩,
     haveI : inhabited P := ⟨0⟩,
     rw [← finsupp.lmap_domain_supported _ _ g, mem_map],
     refine ⟨l, hl1, _⟩,
@@ -578,7 +578,7 @@ begin
       exact finset.smul_sum.symm } },
   rw linear_map.range_eq_top,
   rintro ⟨n, hn⟩, change n ∈ N at hn,
-  rw [← hs, ← set.image_id ↑s, finsupp.mem_span_iff_total] at hn,
+  rw [← hs, ← set.image_id ↑s, finsupp.mem_span_image_iff_total] at hn,
   rcases hn with ⟨l, hl1, hl2⟩,
   refine ⟨λ x, l x, subtype.ext _⟩,
   change ∑ i in s.attach, l i • (i : M) = n,

src/ring_theory/power_basis.lean

@@ -81,11 +81,11 @@ begin
   { ext n,
     simp_rw [set.mem_range, set.mem_image, finset.mem_coe, finset.mem_range],
     exact ⟨λ ⟨⟨i, hi⟩, hy⟩, ⟨i, hi, hy⟩, λ ⟨i, hi, hy⟩, ⟨⟨i, hi⟩, hy⟩⟩ },
-  simp only [this, finsupp.mem_span_iff_total, degree_lt_iff_coeff_zero, exists_iff_exists_finsupp,
-    coeff, aeval, eval₂_ring_hom', eval₂_eq_sum, polynomial.sum, support, finsupp.mem_supported',
-    finsupp.total, finsupp.sum, algebra.smul_def, eval₂_zero, exists_prop, linear_map.id_coe,
-    eval₂_one, id.def, not_lt, finsupp.coe_lsum, linear_map.coe_smul_right, finset.mem_range,
-    alg_hom.coe_mk, finset.mem_coe],
+  simp only [this, finsupp.mem_span_image_iff_total, degree_lt_iff_coeff_zero,
+    exists_iff_exists_finsupp, coeff, aeval, eval₂_ring_hom', eval₂_eq_sum, polynomial.sum, support,
+    finsupp.mem_supported', finsupp.total, finsupp.sum, algebra.smul_def, eval₂_zero, exists_prop,
+    linear_map.id_coe, eval₂_one, id.def, not_lt, finsupp.coe_lsum, linear_map.coe_smul_right,
+    finset.mem_range, alg_hom.coe_mk, finset.mem_coe],
   simp_rw [@eq_comm _ y],
   exact iff.rfl
 end