chore(ring_theory/finiteness): generalize module.finite.trans (#18880)

This was stated for algebras but holds more generally for modules.

This now can be used to prove `finite_dimensional.trans`.

A few downstream proofs were providing the instances arguments explicitly and consequently broke.
Passing those instances via `haveI` fixes those proofs and makes them less fragile.

src/field_theory/tower.lean

@@ -65,8 +65,7 @@ namespace finite_dimensional
 open is_noetherian
 
 theorem trans [finite_dimensional F K] [finite_dimensional K A] : finite_dimensional F A :=
-let b := basis.of_vector_space F K, c := basis.of_vector_space K A in
-of_fintype_basis $ b.smul c
+module.finite.trans K A
 
 /-- In a tower of field extensions `L / K / F`, if `L / F` is finite, so is `K / F`.
 

src/number_theory/cyclotomic/basic.lean

@@ -339,9 +339,11 @@ end
 lemma number_field [h : number_field K] [_root_.finite S] [is_cyclotomic_extension S K L] :
   number_field L :=
 { to_char_zero := char_zero_of_injective_algebra_map (algebra_map K L).injective,
-  to_finite_dimensional := @module.finite.trans _ K L _ _ _ _
-    (@algebra_rat L _ (char_zero_of_injective_algebra_map (algebra_map K L).injective)) _ _
-    h.to_finite_dimensional (finite S K L) }
+  to_finite_dimensional := begin
+    haveI := char_zero_of_injective_algebra_map (algebra_map K L).injective,
+    haveI := finite S K L,
+    exact module.finite.trans K _
+  end }
 
 localized "attribute [instance] is_cyclotomic_extension.number_field" in cyclotomic
 

src/ring_theory/finiteness.lean

@@ -522,13 +522,13 @@ of_surjective (e : M →ₗ[R] N) e.surjective
 
 section algebra
 
-lemma trans {R : Type*} (A B : Type*) [comm_semiring R] [comm_semiring A] [algebra R A]
-  [semiring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] :
-  ∀ [finite R A] [finite A B], finite R B
+lemma trans {R : Type*} (A M : Type*) [comm_semiring R] [semiring A] [algebra R A]
+  [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] :
+  ∀ [finite R A] [finite A M], finite R M
 | ⟨⟨s, hs⟩⟩ ⟨⟨t, ht⟩⟩ := ⟨submodule.fg_def.2
-  ⟨set.image2 (•) (↑s : set A) (↑t : set B),
+  ⟨set.image2 (•) (↑s : set A) (↑t : set M),
     set.finite.image2 _ s.finite_to_set t.finite_to_set,
-    by rw [set.image2_smul, submodule.span_smul_of_span_eq_top hs (↑t : set B),
+    by rw [set.image2_smul, submodule.span_smul_of_span_eq_top hs (↑t : set M),
       ht, submodule.restrict_scalars_top]⟩⟩
 
 end algebra
@@ -584,14 +584,15 @@ begin
 end
 
 lemma comp {g : B →+* C} {f : A →+* B} (hg : g.finite) (hf : f.finite) : (g.comp f).finite :=
-@module.finite.trans A B C _ _ f.to_algebra _ (g.comp f).to_algebra g.to_algebra
 begin
-  fconstructor,
-  intros a b c,
-  simp only [algebra.smul_def, ring_hom.map_mul, mul_assoc],
-  refl
+  letI := f.to_algebra,
+  letI := g.to_algebra,
+  letI := (g.comp f).to_algebra,
+  letI : is_scalar_tower A B C := restrict_scalars.is_scalar_tower A B C,
+  letI : module.finite A B := hf,
+  letI : module.finite B C := hg,
+  exact module.finite.trans B C,
 end
-hf hg
 
 lemma of_comp_finite {f : A →+* B} {g : B →+* C} (h : (g.comp f).finite) : g.finite :=
 begin