chore(ring_theory/*): Eliminate finish (#11100)

Removing uses of `finish`, as discussed in this Zulip thread (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20sat.20solvers)

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,

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,