diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean
index c5c315d056190..e4083a18aa8a1 100644
--- a/src/ring_theory/ideal/basic.lean
+++ b/src/ring_theory/ideal/basic.lean
@@ -574,7 +574,7 @@ lemma bot_lt_of_maximal (M : ideal R) [hm : M.is_maximal] (non_field : ¬ is_fie
 begin
   rcases (ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top.1 non_field)
     with ⟨I, Ibot, Itop⟩,
-  split, finish,
+  split, { simp },
   intro mle,
   apply @irrefl _ (<) _ (⊤ : ideal R),
   have : M = ⊥ := eq_bot_iff.mpr mle,
diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean
index 946feecc9b76d..b1023ddab47f4 100644
--- a/src/ring_theory/principal_ideal_domain.lean
+++ b/src/ring_theory/principal_ideal_domain.lean
@@ -168,7 +168,8 @@ instance euclidean_domain.to_principal_ideal_domain : is_principal_ideal_ring R
         have (x % (well_founded.min wf {x : R | x ∈ S ∧ x ≠ 0} h) ∉ {x : R | x ∈ S ∧ x ≠ 0}),
           from λ h₁, well_founded.not_lt_min wf _ h h₁ (mod_lt x hmin.2),
         have x % well_founded.min wf {x : R | x ∈ S ∧ x ≠ 0} h = 0,
-          by finish [(mod_mem_iff hmin.1).2 hx],
+          by { simp only [not_and_distrib, set.mem_set_of_eq, not_ne_iff] at this,
+               cases this, cases this ((mod_mem_iff hmin.1).2 hx), exact this },
         by simp *),
       λ hx, let ⟨y, hy⟩ := ideal.mem_span_singleton.1 hx in hy.symm ▸ S.mul_mem_right _ hmin.1⟩⟩
     else ⟨0, submodule.ext $ λ a,