feat(ring_theory/ideal/operations): strengthen a lemma to iff and golf (

#15777)

+ Strengthen `exists_sum_of_mem_ideal_smul_span` to iff and rename it to `mem_ideal_smul_span_iff_exists_sum'`.

+ Introduce a more general version `mem_ideal_smul_span_iff_exists_sum` (without the prime) that applies to any type, not just types coerced from a set; this version is stated using `set.range` instead of `set.image`.

+ Use the general version to golf down `finsupp_total_apply_eq_of_fintype` in the same file (this comes from reviewing PR # 15460 after it's approved) and slightly golf `ideal.finrank_quotient_map.span_eq_top` in another file (the only place in mathlib this lemma is used previously).



Co-authored-by: erd1 <the.erd.one@gmail.com>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/number_theory/ramification_inertia.lean

@@ -311,13 +311,12 @@ begin
   -- we can write the elements of `a` as `p`-linear combinations of other elements of `a`.
   have exists_sum : ∀ x : (S ⧸ M), ∃ a' : fin n → R, (∀ i, a' i ∈ p) ∧ ∑ i, a' i • a i = x,
   { intro x,
-    obtain ⟨a'', ha'', hx⟩ := submodule.exists_sum_of_mem_ideal_smul_span p set.univ a x _,
-    refine ⟨λ i, a'' ⟨i, set.mem_univ _⟩, λ i, ha'' _, _⟩,
-    rwa [finsupp.sum_fintype, fintype.sum_equiv (equiv.set.univ (fin n))] at hx,
-    { intros, simp only [eq_self_iff_true, subtype.coe_eta, equiv.set.univ_apply] },
-    { intros, simp only [zero_smul] },
-    rw [set.image_univ, ha, smul_top_eq],
-    exact submodule.mem_top },
+    obtain ⟨a'', ha'', hx⟩ := (submodule.mem_ideal_smul_span_iff_exists_sum p a x).1 _,
+    { refine ⟨λ i, a'' i, λ i, ha'' _, _⟩,
+      rw [← hx, finsupp.sum_fintype],
+      exact λ _, zero_smul _ _ },
+    { rw [ha, smul_top_eq],
+      exact submodule.mem_top } },
   choose A' hA'p hA' using λ i, exists_sum (a i),
   -- This gives us a(n invertible) matrix `A` such that `det A ∈ (M = span R b)`,
   let A : matrix (fin n) (fin n) R := A' - 1,

src/ring_theory/ideal/operations.lean

@@ -228,17 +228,20 @@ variables (I)
 
 /-- If `x` is an `I`-multiple of the submodule spanned by `f '' s`,
 then we can write `x` as an `I`-linear combination of the elements of `f '' s`. -/
-lemma exists_sum_of_mem_ideal_smul_span {ι : Type*} (s : set ι) (f : ι → M) (x : M)
-  (hx : x ∈ I • span R (f '' s)) :
-  ∃ (a : s →₀ R) (ha : ∀ i, a i ∈ I), a.sum (λ i c, c • f i) = x :=
+lemma mem_ideal_smul_span_iff_exists_sum {ι : Type*} (f : ι → M) (x : M) :
+  x ∈ I • span R (set.range f) ↔
+  ∃ (a : ι →₀ R) (ha : ∀ i, a i ∈ I), a.sum (λ i c, c • f i) = x :=
 begin
-  refine span_induction (mem_smul_span.mp hx) _ _ _ _,
+  split, swap,
+  { rintro ⟨a, ha, rfl⟩,
+    exact submodule.sum_mem _ (λ c _, smul_mem_smul (ha c) $ subset_span $ set.mem_range_self _) },
+  refine λ hx, span_induction (mem_smul_span.mp hx) _ _ _ _,
   { simp only [set.mem_Union, set.mem_range, set.mem_singleton_iff],
-    rintros x ⟨y, hy, x, ⟨i, hi, rfl⟩, rfl⟩,
-    refine ⟨finsupp.single ⟨i, hi⟩ y, λ j, _, _⟩,
-    { letI := classical.dec_eq s,
+    rintros x ⟨y, hy, x, ⟨i, rfl⟩, rfl⟩,
+    refine ⟨finsupp.single i y, λ j, _, _⟩,
+    { letI := classical.dec_eq ι,
       rw finsupp.single_apply, split_ifs, { assumption }, { exact I.zero_mem } },
-    refine @finsupp.sum_single_index s R M _ _ ⟨i, hi⟩ _ (λ i y, y • f i) _,
+    refine @finsupp.sum_single_index ι R M _ _ i _ (λ i y, y • f i) _,
     simp },
   { exact ⟨0, λ i, I.zero_mem, finsupp.sum_zero_index⟩ },
   { rintros x y ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩,
@@ -250,6 +253,11 @@ begin
       intros; simp only [zero_smul, mul_smul] },
 end
 
+theorem mem_ideal_smul_span_iff_exists_sum' {ι : Type*} (s : set ι) (f : ι → M) (x : M) :
+  x ∈ I • span R (f '' s) ↔
+  ∃ (a : s →₀ R) (ha : ∀ i, a i ∈ I), a.sum (λ i c, c • f i) = x :=
+by rw [← submodule.mem_ideal_smul_span_iff_exists_sum, ← set.image_eq_range]
+
 @[simp] lemma smul_comap_le_comap_smul (f : M →ₗ[R] M') (S : submodule R M') (I : ideal R) :
   I • S.comap f ≤ (I • S).comap f :=
 begin
@@ -1423,40 +1431,20 @@ end
 
 lemma finsupp_total_apply_eq_of_fintype [fintype ι] (f : ι →₀ I) :
   finsupp_total ι M I v f = ∑ i, (f i : R) • v i :=
-begin
-  rw finsupp_total_apply,
-  apply finset.sum_subset (finset.subset_univ _),
-  intros x _ hx,
-  rw finsupp.not_mem_support_iff.mp hx,
-  exact zero_smul _ _
-end
+by { rw [finsupp_total_apply, finsupp.sum_fintype], exact λ _, zero_smul _ _ }
 
 lemma range_finsupp_total :
   (finsupp_total ι M I v).range = I • (submodule.span R (set.range v)) :=
 begin
-  apply le_antisymm,
-  { rintros x ⟨f, rfl⟩,
-    rw finsupp_total_apply,
-    apply submodule.sum_mem _ _,
-    intros c _,
-    apply submodule.smul_mem_smul (f c).2,
-    apply submodule.subset_span,
-    exact set.mem_range_self c },
-  { rw submodule.smul_le,
-    rintros r hr m hm,
-    rw ← set.image_univ at hm,
-    obtain ⟨l, hl, rfl⟩ := (finsupp.mem_span_image_iff_total _).mp hm,
-    let l' : ι →₀ I := finsupp.map_range (λ x : R, (⟨x * r, I.mul_mem_left _ hr⟩ : I))
-      (subtype.ext $ zero_mul _) l,
-    use l',
-    rw [finsupp_total_apply, finsupp.total_apply, finsupp.sum, finsupp.sum, finset.smul_sum],
-    dsimp,
-    simp only [← mul_smul, mul_comm r],
-    apply finset.sum_subset,
-    { exact finsupp.support_map_range },
-    { intros x hx hx',
-      have : l x * r = 0 := by injection finsupp.not_mem_support_iff.mp hx',
-      rw [this, zero_smul] } }
+  ext,
+  rw submodule.mem_ideal_smul_span_iff_exists_sum,
+  refine ⟨λ ⟨f, h⟩, ⟨finsupp.map_range.linear_map I.subtype f, λ i, (f i).2, h⟩, _⟩,
+  rintro ⟨a, ha, rfl⟩,
+  classical,
+  refine ⟨a.map_range (λ r, if h : r ∈ I then ⟨r, h⟩ else 0) (by split_ifs; refl), _⟩,
+  rw [finsupp_total_apply, finsupp.sum_map_range_index],
+  { apply finsupp.sum_congr, intros i _, rw dif_pos (ha i), refl },
+  { exact λ _, zero_smul _ _ },
 end
 
 end total