diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean
index 2684a748..d5edb79a 100644
--- a/FltRegular/NumberTheory/Different.lean
+++ b/FltRegular/NumberTheory/Different.lean
@@ -424,7 +424,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
   · exact aeval_derivative_minpoly_ne_zero _ (IsSeparable.separable _ _)
   have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0
   · rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
-      aeval_map_algebraMap, aeval_algebraMap] at hne₁
+      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
   rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual,
     mem_coeIdeal_conductor]
   have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0
@@ -434,7 +434,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
   rw [← traceFormDualSubmodule_span_adjoin A K L _ hx this]
   simp only [mem_traceFormDualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule,
     minpoly.isIntegrallyClosed_eq_field_fractions K L hAx,
-    derivative_map, aeval_map_algebraMap, aeval_algebraMap, mul_assoc,
+    derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply, mul_assoc,
     FractionalIdeal.mem_one_iff, forall_exists_index, forall_apply_eq_imp_iff]
   simp_rw [← IsScalarTower.toAlgHom_apply A B L x, ← Algebra.map_adjoin_singleton]
   simp only [Subalgebra.mem_map, IsScalarTower.coe_toAlgHom',
diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean
index 8db49674..bfe1e6e0 100644
--- a/FltRegular/NumberTheory/Unramified.lean
+++ b/FltRegular/NumberTheory/Unramified.lean
@@ -212,8 +212,8 @@ lemma isUnramifiedAt_of_Separable_minpoly' [IsSeparable K L]
     obtain ⟨a, b, e⟩ := this
     apply_fun (aeval (Ideal.Quotient.mk P x)) at e
     simp only [← Ideal.Quotient.algebraMap_eq, ← map_map, derivative_map, map_add, map_mul,
-      aeval_map_algebraMap, aeval_algebraMap, minpoly.aeval, map_zero, mul_zero, hxP, zero_add,
-      coe_aeval_eq_eval, eval_one] at e
+      aeval_map_algebraMap, aeval_algebraMap_apply, minpoly.aeval, map_zero, mul_zero, hxP,
+      zero_add, coe_aeval_eq_eval, eval_one] at e
     exact zero_ne_one e
   · rwa [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _
       (isMaximal_of_mem_primesOver hpbot hP).isPrime (ne_bot_of_mem_primesOver hpbot hP),