fix(field_theory/intermediate_field): use a better algebra.smul def…

…inition, and generalize

Previously coe_smul was not true by `rfl`

src/field_theory/intermediate_field.lean

@@ -286,29 +286,19 @@ instance has_lift2 {F : intermediate_field K L} :
   x ∈ (↑E : intermediate_field K L) ↔ x ∈ E := iff.rfl
 
 instance lift2_alg {F : intermediate_field K L} {E : intermediate_field F L} : algebra K E :=
-{ to_fun := (algebra_map F E).comp (algebra_map K F),
-  map_zero' := ((algebra_map F E).comp (algebra_map K F)).map_zero,
-  map_one' := ((algebra_map F E).comp (algebra_map K F)).map_one,
-  map_add' := ((algebra_map F E).comp (algebra_map K F)).map_add,
-  map_mul' := ((algebra_map F E).comp (algebra_map K F)).map_mul,
-  smul := λ a b, (((algebra_map F E).comp (algebra_map K F)) a) * b,
-  smul_def' := λ _ _, rfl,
-  commutes' := λ a b, mul_comm (((algebra_map F E).comp (algebra_map K F)) a) b }
+E.to_subalgebra.algebra'
+
+lemma lift2_algebra_map {F : intermediate_field K L} {E : intermediate_field F L} (k : K) (e : E) :
+  algebra_map K E = (algebra_map F E).comp (algebra_map K F) := rfl
 
 instance lift2_tower {F : intermediate_field K L} {E : intermediate_field F L} :
   is_scalar_tower K F E :=
-⟨λ a b c, by { simp only [algebra.smul_def, ring_hom.map_mul, mul_assoc], refl }⟩
+E.to_subalgebra.is_scalar_tower
 
 /-- `lift2` is isomorphic to the original `intermediate_field`. -/
 def lift2_alg_equiv {F : intermediate_field K L} (E : intermediate_field F L) :
   (↑E : intermediate_field K L) ≃ₐ[K] E :=
-{ to_fun := λ x, x,
-  inv_fun := λ x, x,
-  left_inv := λ x, rfl,
-  right_inv := λ x, rfl,
-  map_add' := λ x y, rfl,
-  map_mul' := λ x y, rfl,
-  commutes' := λ x, rfl }
+alg_equiv.refl
 
 end tower