diff --git a/Mathlib/Algebra/Star/Pointwise.lean b/Mathlib/Algebra/Star/Pointwise.lean
index bc239ea5648a27..4281e51260644a 100644
--- a/Mathlib/Algebra/Star/Pointwise.lean
+++ b/Mathlib/Algebra/Star/Pointwise.lean
@@ -129,6 +129,5 @@ end Set
 @[simp]
 lemma StarMemClass.star_coe_eq {S α : Type*} [InvolutiveStar α] [SetLike S α]
     [StarMemClass S α] (s : S) : star (s : Set α) = s := by
-  ext x
-  simp only [Set.mem_star, SetLike.mem_coe]
-  exact ⟨by simpa only [star_star] using star_mem (s := s) (r := star x), star_mem⟩
+  ext
+  simpa using star_mem_iff
diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
index 17975d77882dc0..4cf086096ef549 100644
--- a/Mathlib/Data/Set/Function.lean
+++ b/Mathlib/Data/Set/Function.lean
@@ -159,11 +159,8 @@ theorem MapsTo.iterate {f : α → α} {s : Set α} (h : MapsTo f s s) : ∀ n,
 
 theorem MapsTo.iterate_restrict {f : α → α} {s : Set α} (h : MapsTo f s s) (n : ℕ) :
     (h.restrict f s s)^[n] = (h.iterate n).restrict _ _ _ := by
-  funext x
-  rw [Subtype.ext_iff, MapsTo.val_restrict_apply]
-  induction n generalizing x with
-  | zero => rfl
-  | succ n ihn => simp [Nat.iterate, ihn]
+  ext
+  simpa using coe_iterate_restrict _ _ _
 
 lemma mapsTo_of_subsingleton' [Subsingleton β] (f : α → β) (h : s.Nonempty → t.Nonempty) :
     MapsTo f s t :=
diff --git a/Mathlib/Order/Atoms/Finite.lean b/Mathlib/Order/Atoms/Finite.lean
index c49b9b64753089..584e8d50da5a0b 100644
--- a/Mathlib/Order/Atoms/Finite.lean
+++ b/Mathlib/Order/Atoms/Finite.lean
@@ -54,10 +54,8 @@ open scoped _root_.IsSimpleOrder
 variable [LE α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α]
 
 theorem univ : (Finset.univ : Finset α) = {⊤, ⊥} := by
-  change Finset.map _ (Finset.univ : Finset Bool) = _
-  rw [Fintype.univ_bool]
-  simp only [Finset.map_insert, Function.Embedding.coeFn_mk, Finset.map_singleton]
-  rfl
+  ext
+  simpa using (eq_bot_or_eq_top _).symm
 
 theorem card : Fintype.card α = 2 :=
   (Fintype.ofEquiv_card _).trans Fintype.card_bool
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
index 4fadf5188c8b9a..098f6091048606 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
@@ -278,12 +278,8 @@ theorem ciSup_mem_iInter_Icc_of_antitone_Icc [SemilatticeSup β] {f g : β → 
 
 lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) :
     Iic (⨅ i, f i) = ⋂ i, Iic (f i) := by
-  apply Subset.antisymm
-  · rintro x hx - ⟨i, rfl⟩
-    exact hx.trans (ciInf_le hf _)
-  · rintro x hx
-    apply le_ciInf
-    simpa using hx
+  ext
+  simpa using le_ciInf_iff hf
 
 lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) :
     Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
index c7136f0544c354..3b96d35d8acc4e 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
@@ -1008,12 +1008,8 @@ variable {A : Type*} [CommRing A] {p : Ideal A} (hpb : p ≠ ⊥) [hpm : p.IsMax
 
 include hpb in
 theorem coe_primesOverFinset : primesOverFinset p B = primesOver p B := by
-  classical
-  ext P
-  rw [primesOverFinset, factors_eq_normalizedFactors, Finset.mem_coe, Multiset.mem_toFinset]
-  exact (P.mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hpb)).trans <| Iff.intro
-    (fun ⟨hPp, h⟩ => ⟨hPp, ⟨hpm.eq_of_le (comap_ne_top _ hPp.ne_top) (le_comap_of_map_le h)⟩⟩)
-    (fun ⟨hPp, h⟩ => ⟨hPp, map_le_of_le_comap h.1.le⟩)
+  ext
+  simpa using (mem_primesOver_iff_mem_normalizedFactors _ hpb).symm
 
 include hpb in
 theorem mem_primesOverFinset_iff {P : Ideal B} : P ∈ primesOverFinset p B ↔ P ∈ primesOver p B := by