diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean
index a7e58649a9011..61f58be053015 100644
--- a/src/field_theory/adjoin.lean
+++ b/src/field_theory/adjoin.lean
@@ -530,7 +530,10 @@ lemma card_alg_hom_adjoin_integral (h : is_integral F α) (h_sep : (minpoly F α
   (h_splits : (minpoly F α).splits (algebra_map F K)) :
   @fintype.card (F⟮α⟯ →ₐ[F] K) (fintype_of_alg_hom_adjoin_integral F h) =
     (minpoly F α).nat_degree :=
-by { rw alg_hom.card_of_power_basis, all_goals { rwa [adjoin.power_basis_gen, minpoly_gen h] } }
+begin
+  rw alg_hom.card_of_power_basis;
+    simp only [adjoin.power_basis_dim, adjoin.power_basis_gen, minpoly_gen h, h_sep, h_splits],
+end
 
 end adjoin_integral_element
 
diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
index 65ddce1f7d00d..ac1e1187350ee 100644
--- a/src/field_theory/intermediate_field.lean
+++ b/src/field_theory/intermediate_field.lean
@@ -208,12 +208,21 @@ end
 instance algebra : algebra K S :=
 S.to_subalgebra.algebra
 
-instance to_algebra : algebra S L :=
+instance to_algebra {R : Type*} [semiring R] [algebra L R] : algebra S R :=
 S.to_subalgebra.to_algebra
 
-instance : is_scalar_tower K S L :=
+instance is_scalar_tower_bot {R : Type*} [semiring R] [algebra L R] :
+  is_scalar_tower S L R :=
+is_scalar_tower.subalgebra _ _ _ S.to_subalgebra
+
+instance is_scalar_tower_mid {R : Type*} [semiring R] [algebra L R] [algebra K R]
+  [is_scalar_tower K L R] : is_scalar_tower K S R :=
 is_scalar_tower.subalgebra' _ _ _ S.to_subalgebra
 
+/-- Specialize `is_scalar_tower_mid` to the common case where the top field is `L` -/
+instance is_scalar_tower_mid' : is_scalar_tower K S L :=
+S.is_scalar_tower_mid
+
 variables {L' : Type*} [field L'] [algebra K L']
 
 /-- If `f : L →+* L'` fixes `K`, `S.map f` is the intermediate field between `L'` and `K`
diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean
index e1e4775ecccbb..ece57a833990b 100644
--- a/src/field_theory/polynomial_galois_group.lean
+++ b/src/field_theory/polynomial_galois_group.lean
@@ -97,6 +97,14 @@ instance [h : fact (p.splits (algebra_map F E))] : is_scalar_tower F p.splitting
 is_scalar_tower.of_algebra_map_eq
   (λ x, ((is_splitting_field.lift p.splitting_field p h.1).commutes x).symm)
 
+-- The `algebra p.splitting_field E` instance above behaves badly when
+-- `E := p.splitting_field`, since it may result in a unification problem
+-- `is_splitting_field.lift.to_ring_hom.to_algebra =?= algebra.id`,
+-- which takes an extremely long time to resolve, causing timeouts.
+-- Since we don't really care about this definition, marking it as irreducible
+-- causes that unification to error out early.
+attribute [irreducible] gal.algebra
+
 /-- Restrict from a superfield automorphism into a member of `gal p`. -/
 def restrict [fact (p.splits (algebra_map F E))] : (E ≃ₐ[F] E) →* p.gal :=
 alg_equiv.restrict_normal_hom p.splitting_field
diff --git a/src/field_theory/primitive_element.lean b/src/field_theory/primitive_element.lean
index ade36a55a1300..50efa64d8ae59 100644
--- a/src/field_theory/primitive_element.lean
+++ b/src/field_theory/primitive_element.lean
@@ -5,6 +5,7 @@ Authors: Thomas Browning, Patrick Lutz
 -/
 
 import field_theory.adjoin
+import field_theory.algebraic_closure
 import field_theory.separable
 
 /-!
@@ -194,4 +195,17 @@ let α := (exists_primitive_element F E).some,
 have e : F⟮α⟯ = ⊤ := (exists_primitive_element F E).some_spec,
 pb.map ((intermediate_field.equiv_of_eq e).trans intermediate_field.top_equiv)
 
+/-- If `E / F` is a finite separable extension, then there are finitely many
+embeddings from `E` into `K` that fix `F`, corresponding to the number of
+conjugate roots of the primitive element generating `F`. -/
+instance {K : Type*} [field K] [algebra F K] : fintype (E →ₐ[F] K) :=
+power_basis.alg_hom.fintype (power_basis_of_finite_of_separable F E)
+
 end field
+
+@[simp] lemma alg_hom.card (F E K : Type*) [field F] [field E] [field K] [is_alg_closed K]
+  [algebra F E] [finite_dimensional F E] [is_separable F E] [algebra F K] :
+  fintype.card (E →ₐ[F] K) = finrank F E :=
+(alg_hom.card_of_power_basis (field.power_basis_of_finite_of_separable F E)
+    (is_separable.separable _ _) (is_alg_closed.splits_codomain _)).trans
+  (power_basis.finrank _).symm
diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 854db31713776..0bc6f2e9738b9 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -657,12 +657,12 @@ variables [algebra K S] [algebra K L]
 
 lemma alg_hom.card_of_power_basis (pb : power_basis K S) (h_sep : (minpoly K pb.gen).separable)
   (h_splits : (minpoly K pb.gen).splits (algebra_map K L)) :
-  @fintype.card (S →ₐ[K] L) (power_basis.alg_hom.fintype pb) = (minpoly K pb.gen).nat_degree :=
+  @fintype.card (S →ₐ[K] L) (power_basis.alg_hom.fintype pb) = pb.dim :=
 begin
   let s := ((minpoly K pb.gen).map (algebra_map K L)).roots.to_finset,
   have H := λ x, multiset.mem_to_finset,
   rw [fintype.card_congr pb.lift_equiv', fintype.card_of_subtype s H,
-      nat_degree_eq_card_roots h_splits, multiset.to_finset_card_of_nodup],
+      ← pb.nat_degree_minpoly, nat_degree_eq_card_roots h_splits, multiset.to_finset_card_of_nodup],
   exact nodup_roots ((separable_map (algebra_map K L)).mpr h_sep)
 end
 
diff --git a/src/linear_algebra/free_module_pid.lean b/src/linear_algebra/free_module_pid.lean
index 7c202dddbfc12..de12faf5fe42e 100644
--- a/src/linear_algebra/free_module_pid.lean
+++ b/src/linear_algebra/free_module_pid.lean
@@ -437,9 +437,7 @@ begin
         (show (set.range (λ ψ : M →ₗ[R] R, ψ.submodule_image N)).nonempty,
          from ⟨_, set.mem_range.mpr ⟨0, rfl⟩⟩),
     obtain ⟨ϕ, rfl⟩ := set.mem_range.mp P_eq,
-    use ϕ,
-    intros ψ hψ,
-    exact P_max _ ⟨_, rfl⟩ hψ },
+    exact ⟨ϕ, λ ψ hψ, P_max _ ⟨_, rfl⟩ hψ⟩ },
   let ϕ := this.some,
   have ϕ_max := this.some_spec,
   -- Since `ϕ(N)` is a `R`-submodule of the PID `R`,
diff --git a/src/ring_theory/power_basis.lean b/src/ring_theory/power_basis.lean
index b4534d0d39f2d..bcb37d04dcdaf 100644
--- a/src/ring_theory/power_basis.lean
+++ b/src/ring_theory/power_basis.lean
@@ -329,6 +329,7 @@ noncomputable def lift_equiv (pb : power_basis A S) :
 
 /-- `pb.lift_equiv'` states that elements of the root set of the minimal
 polynomial of `pb.gen` correspond to maps sending `pb.gen` to that root. -/
+@[simps {fully_applied := ff}]
 noncomputable def lift_equiv' (pb : power_basis A S) :
   (S →ₐ[A] B) ≃ {y : B // y ∈ ((minpoly A pb.gen).map (algebra_map A B)).roots} :=
 pb.lift_equiv.trans ((equiv.refl _).subtype_equiv (λ x,
diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
index 4650912c1abe8..9be2b71913f6c 100644
--- a/src/ring_theory/trace.lean
+++ b/src/ring_theory/trace.lean
@@ -6,9 +6,10 @@ Authors: Anne Baanen
 
 import linear_algebra.bilinear_form
 import linear_algebra.char_poly.coeff
+import linear_algebra.determinant
 import linear_algebra.trace
-import field_theory.adjoin
 import field_theory.algebraic_closure
+import field_theory.primitive_element
 import ring_theory.power_basis
 
 /-!
@@ -232,20 +233,29 @@ end
 
 end intermediate_field.adjoin_simple
 
-lemma trace_eq_sum_roots [finite_dimensional K L]
-  {x : L} (hF : (minpoly K x).splits (algebra_map K F)) :
-  algebra_map K F (algebra.trace K L x) =
-    finrank K⟮x⟯ L • ((minpoly K x).map (algebra_map K _)).roots.sum :=
+open intermediate_field
+
+variables (K)
+
+lemma trace_eq_trace_adjoin [finite_dimensional K L] (x : L) :
+  algebra.trace K L x = finrank K⟮x⟯ L • trace K K⟮x⟯ (adjoin_simple.gen K x) :=
 begin
-  haveI : finite_dimensional K⟮x⟯ L := finite_dimensional.right K _ L,
   rw ← @trace_trace _ _ K K⟮x⟯ _ _ _ _ _ _ _ _ x,
   conv in x { rw ← intermediate_field.adjoin_simple.algebra_map_gen K x },
   rw [trace_algebra_map, ← is_scalar_tower.algebra_map_smul K, (algebra.trace K K⟮x⟯).map_smul,
-      smul_eq_mul, ring_hom.map_mul, ← is_scalar_tower.algebra_map_apply ℕ K _, ← smul_def,
-      intermediate_field.adjoin_simple.trace_gen_eq_sum_roots _ hF],
-  all_goals { apply_instance }
+      smul_eq_mul, algebra.smul_def],
+  apply_instance
 end
 
+variables {K}
+
+lemma trace_eq_sum_roots [finite_dimensional K L]
+  {x : L} (hF : (minpoly K x).splits (algebra_map K F)) :
+  algebra_map K F (algebra.trace K L x) =
+    finrank K⟮x⟯ L • ((minpoly K x).map (algebra_map K _)).roots.sum :=
+by rw [trace_eq_trace_adjoin K x, algebra.smul_def, ring_hom.map_mul, ← algebra.smul_def,
+    intermediate_field.adjoin_simple.trace_gen_eq_sum_roots _ hF, is_scalar_tower.algebra_map_smul]
+
 end eq_sum_roots
 
 variables {F : Type*} [field F]
@@ -268,3 +278,63 @@ begin
   { apply is_alg_closed.splits_codomain },
   { apply_instance }
 end
+
+section eq_sum_embeddings
+
+variables [algebra K F] [is_scalar_tower K L F]
+
+open algebra intermediate_field
+
+variables (F) (E : Type*) [field E] [algebra K E]
+
+lemma trace_eq_sum_embeddings_gen
+  (pb : power_basis K L)
+  (hE : (minpoly K pb.gen).splits (algebra_map K E)) (hfx : (minpoly K pb.gen).separable) :
+  algebra_map K E (algebra.trace K L pb.gen) =
+    (@@finset.univ (power_basis.alg_hom.fintype pb)).sum (λ σ, σ pb.gen) :=
+begin
+  letI := classical.dec_eq E,
+  rw [pb.trace_gen_eq_sum_roots hE, fintype.sum_equiv pb.lift_equiv', finset.sum_mem_multiset,
+      finset.sum_eq_multiset_sum, multiset.to_finset_val,
+      multiset.erase_dup_eq_self.mpr (nodup_roots ((separable_map _).mpr hfx)), multiset.map_id],
+  { intro x, refl },
+  { intro σ, rw [power_basis.lift_equiv'_apply_coe, id.def] }
+end
+
+variables [is_alg_closed E]
+
+lemma sum_embeddings_eq_finrank_mul [finite_dimensional K F] [is_separable K F]
+  (pb : power_basis K L) :
+  ∑ σ : F →ₐ[K] E, σ (algebra_map L F pb.gen) =
+    finrank L F • (@@finset.univ (power_basis.alg_hom.fintype pb)).sum
+      (λ σ : L →ₐ[K] E, σ pb.gen) :=
+begin
+  haveI : finite_dimensional L F := finite_dimensional.right K L F,
+  haveI : is_separable L F := is_separable_tower_top_of_is_separable K L F,
+  letI : fintype (L →ₐ[K] E) := power_basis.alg_hom.fintype pb,
+  letI : ∀ (f : L →ₐ[K] E), fintype (@@alg_hom L F E _ _ _ _ f.to_ring_hom.to_algebra) :=
+    _, -- will be solved by unification
+  rw [fintype.sum_equiv alg_hom_equiv_sigma (λ (σ : F →ₐ[K] E), _) (λ σ, σ.1 pb.gen),
+      ← finset.univ_sigma_univ, finset.sum_sigma, ← finset.sum_nsmul],
+  refine finset.sum_congr rfl (λ σ _, _),
+  { letI : algebra L E := σ.to_ring_hom.to_algebra,
+    simp only [finset.sum_const, finset.card_univ],
+    rw alg_hom.card L F E },
+  { intros σ,
+    simp only [alg_hom_equiv_sigma, equiv.coe_fn_mk, alg_hom.restrict_domain, alg_hom.comp_apply,
+         is_scalar_tower.coe_to_alg_hom'] }
+end
+
+lemma trace_eq_sum_embeddings [finite_dimensional K L] [is_separable K L]
+  {x : L} (hx : is_integral K x) :
+  algebra_map K E (algebra.trace K L x) = ∑ σ : L →ₐ[K] E, σ x :=
+begin
+  rw [trace_eq_trace_adjoin K x, algebra.smul_def, ring_hom.map_mul, ← adjoin.power_basis_gen hx,
+      trace_eq_sum_embeddings_gen E (adjoin.power_basis hx) (is_alg_closed.splits_codomain _),
+      ← algebra.smul_def, algebra_map_smul],
+  { exact (sum_embeddings_eq_finrank_mul L E (adjoin.power_basis hx)).symm },
+  { haveI := is_separable_tower_bot_of_is_separable K K⟮x⟯ L,
+    exact is_separable.separable K _ }
+end
+
+end eq_sum_embeddings