chore(algebra/algebra/basic): remove a duplicate lemma (#18415)

This combines `submodule.span_eq_restrict_scalars` (which was stated backwards and added in #6098) with `algebra.span_restrict_scalars_eq_span_of_surjective` (which was in an odd namespace, and added in #13042).
The two lemmas were identical modulo argument order and explicitness.

This also has the bonus of reducing the imports of `algebra.algebra.basic`.

src/algebra/algebra/basic.lean

@@ -6,10 +6,11 @@ Authors: Kenny Lau, Yury Kudryashov
 import algebra.module.basic
 import algebra.module.ulift
 import algebra.ne_zero
+import algebra.punit_instances
 import algebra.ring.aut
 import algebra.ring.ulift
 import algebra.char_zero.lemmas
-import linear_algebra.span
+import linear_algebra.basic
 import ring_theory.subring.basic
 import tactic.abel
 
@@ -812,25 +813,6 @@ rfl
 
 end module
 
-namespace submodule
-
-variables (R A M : Type*)
-variables [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M]
-variables [module R M] [module A M] [is_scalar_tower R A M]
-
-/-- If `A` is an `R`-algebra such that the induced morhpsim `R →+* A` is surjective, then the
-`R`-module generated by a set `X` equals the `A`-module generated by `X`. -/
-lemma span_eq_restrict_scalars (X : set M) (hsur : function.surjective (algebra_map R A)) :
-  span R X = restrict_scalars R (span A X) :=
-begin
-  apply (span_le_restrict_scalars R A X).antisymm (λ m hm, _),
-  refine span_induction hm subset_span (zero_mem _) (λ _ _, add_mem) (λ a m hm, _),
-  obtain ⟨r, rfl⟩ := hsur a,
-  simpa [algebra_map_smul] using smul_mem _ r hm
-end
-
-end submodule
-
 example {R A} [comm_semiring R] [semiring A]
   [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] : algebra R A :=
 algebra.of_module smul_mul_assoc mul_smul_comm

src/algebra/algebra/tower.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Anne Baanen
 -/
 
 import algebra.algebra.equiv
+import linear_algebra.span
 
 /-!
 # Towers of algebras
@@ -190,32 +191,29 @@ end alg_equiv
 
 end homs
 
-namespace algebra
+namespace submodule
 
-variables {R A} [comm_semiring R] [semiring A] [algebra R A]
-variables {M} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M]
+variables (R A) {M}
+variables [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M]
+variables [module R M] [module A M] [is_scalar_tower R A M]
 
-lemma span_restrict_scalars_eq_span_of_surjective
-  (h : function.surjective (algebra_map R A)) (s : set M) :
-  (submodule.span A s).restrict_scalars R = submodule.span R s :=
+/-- If `A` is an `R`-algebra such that the induced morphism `R →+* A` is surjective, then the
+`R`-module generated by a set `X` equals the `A`-module generated by `X`. -/
+lemma restrict_scalars_span (hsur : function.surjective (algebra_map R A)) (X : set M) :
+  restrict_scalars R (span A X) = span R X :=
 begin
-  refine le_antisymm (λ x hx, _) (submodule.span_subset_span _ _ _),
-  refine submodule.span_induction hx _ _ _ _,
-  { exact λ x hx, submodule.subset_span hx },
-  { exact submodule.zero_mem _ },
-  { exact λ x y, submodule.add_mem _ },
-  { intros c x hx,
-    obtain ⟨c', rfl⟩ := h c,
-    rw is_scalar_tower.algebra_map_smul,
-    exact submodule.smul_mem _ _ hx },
+  refine ((span_le_restrict_scalars R A X).antisymm (λ m hm, _)).symm,
+  refine span_induction hm subset_span (zero_mem _) (λ _ _, add_mem) (λ a m hm, _),
+  obtain ⟨r, rfl⟩ := hsur a,
+  simpa [algebra_map_smul] using smul_mem _ r hm
 end
 
 lemma coe_span_eq_span_of_surjective
   (h : function.surjective (algebra_map R A)) (s : set M) :
   (submodule.span A s : set M) = submodule.span R s :=
-congr_arg coe (algebra.span_restrict_scalars_eq_span_of_surjective h s)
+congr_arg coe (submodule.restrict_scalars_span R A h s)
 
-end algebra
+end submodule
 
 section semiring
 

src/algebra/category/Module/tannaka.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.category.Module.basic
+import linear_algebra.span
 
 /-!
 # Tannaka duality for rings

src/number_theory/ramification_inertia.lean

@@ -417,8 +417,8 @@ begin
     have mem_span_b :
       ((submodule.mkq (map (algebra_map R S) p)) x :
         S ⧸ map (algebra_map R S) p) ∈ submodule.span (R ⧸ p) (set.range b) := b.mem_span _,
-    rw [← @submodule.restrict_scalars_mem R, algebra.span_restrict_scalars_eq_span_of_surjective
-        (show function.surjective (algebra_map R (R ⧸ p)), from ideal.quotient.mk_surjective) _,
+    rw [← @submodule.restrict_scalars_mem R,
+        submodule.restrict_scalars_span R (R ⧸ p) ideal.quotient.mk_surjective,
         b_eq_b', set.range_comp, ← submodule.map_span]
       at mem_span_b,
     obtain ⟨y, y_mem, y_eq⟩ := submodule.mem_map.mp mem_span_b,

src/ring_theory/derivation.lean

@@ -1004,7 +1004,7 @@ lemma kaehler_differential.ker_total_map (h : function.surjective (algebra_map A
     (kaehler_differential.ker_total S B).restrict_scalars _  :=
 begin
   rw [kaehler_differential.ker_total, submodule.map_span, kaehler_differential.ker_total,
-    ← submodule.span_eq_restrict_scalars _ _ _ _ h],
+    submodule.restrict_scalars_span _ _ h],
   simp_rw [set.image_union, submodule.span_union, ← set.image_univ, set.image_image,
     set.image_univ, map_sub, map_add],
   simp only [linear_map.comp_apply, finsupp.map_range.linear_map_apply, finsupp.map_range_single,
@@ -1070,7 +1070,7 @@ lemma kaehler_differential.map_surjective_of_surjective
   function.surjective (kaehler_differential.map R S A B) :=
 begin
   rw [← linear_map.range_eq_top, _root_.eq_top_iff, ← @submodule.restrict_scalars_top B A,
-    ← kaehler_differential.span_range_derivation, ← submodule.span_eq_restrict_scalars _ _ _ _ h,
+    ← kaehler_differential.span_range_derivation, submodule.restrict_scalars_span _ _ h,
     submodule.span_le],
   rintros _ ⟨x, rfl⟩,
   obtain ⟨y, rfl⟩ := h x,

src/ring_theory/finiteness.lean

@@ -284,7 +284,7 @@ lemma fg_restrict_scalars {R S M : Type*} [comm_semiring R] [semiring S] [algebr
 begin
   obtain ⟨X, rfl⟩ := hfin,
   use X,
-  exact submodule.span_eq_restrict_scalars R S M X h
+  exact (submodule.restrict_scalars_span R S h ↑X).symm
 end
 
 lemma fg.stablizes_of_supr_eq {M' : submodule R M} (hM' : M'.fg)