diff --git a/Mathlib/Algebra/Polynomial/BigOperators.lean b/Mathlib/Algebra/Polynomial/BigOperators.lean
index 9c45f3aa3e918b..a0e130b1a2e14e 100644
--- a/Mathlib/Algebra/Polynomial/BigOperators.lean
+++ b/Mathlib/Algebra/Polynomial/BigOperators.lean
@@ -270,16 +270,16 @@ theorem multiset_prod_X_sub_C_coeff_card_pred (t : Multiset R) (ht : 0 < Multise
     (t.map fun x => X - C x).prod.coeff ((Multiset.card t) - 1) = -t.sum := by
   nontriviality R
   convert multiset_prod_X_sub_C_nextCoeff (by assumption)
-  rw [nextCoeff]; split_ifs with h
-  · rw [natDegree_multiset_prod_of_monic] at h
+  rw [nextCoeff, if_neg]
+  swap
+  · rw [natDegree_multiset_prod_of_monic]
     swap
     · simp only [Multiset.mem_map]
       rintro _ ⟨_, _, rfl⟩
       apply monic_X_sub_C
-    simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map] at h
-    contrapose! h
+    simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]
     obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht
-    exact ⟨_, ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩, one_ne_zero⟩
+    exact fun h => one_ne_zero <| h 1 ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩
   congr; rw [natDegree_multiset_prod_of_monic] <;> · simp [natDegree_X_sub_C, monic_X_sub_C]
 set_option linter.uppercaseLean3 false in
 #align polynomial.multiset_prod_X_sub_C_coeff_card_pred Polynomial.multiset_prod_X_sub_C_coeff_card_pred
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
index ad43cf8123b59e..43cb5061eb358c 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
@@ -1757,7 +1757,7 @@ protected def transfer {u v : V} (p : G.Walk u v)
     (H : SimpleGraph V) (h : ∀ e, e ∈ p.edges → e ∈ H.edgeSet) : H.Walk u v :=
   match p with
   | nil => nil
-  | cons' u v w a p =>
+  | cons' u v w _ p =>
     cons (h s(u, v) (by simp)) (p.transfer H fun e he => h e (by simp [he]))
 #align simple_graph.walk.transfer SimpleGraph.Walk.transfer
 
diff --git a/Mathlib/Data/List/BigOperators/Basic.lean b/Mathlib/Data/List/BigOperators/Basic.lean
index 8e6d183300afb2..76372d99864764 100644
--- a/Mathlib/Data/List/BigOperators/Basic.lean
+++ b/Mathlib/Data/List/BigOperators/Basic.lean
@@ -202,8 +202,7 @@ theorem prod_take_succ :
 @[to_additive "A list with sum not zero must have positive length."]
 theorem length_pos_of_prod_ne_one (L : List M) (h : L.prod ≠ 1) : 0 < L.length := by
   cases L
-  · contrapose h
-    simp
+  · simp at h
   · simp
 #align list.length_pos_of_prod_ne_one List.length_pos_of_prod_ne_one
 #align list.length_pos_of_sum_ne_zero List.length_pos_of_sum_ne_zero
diff --git a/Mathlib/Data/PNat/Basic.lean b/Mathlib/Data/PNat/Basic.lean
index ead7badc1ffd7d..fbbfe4308f40f0 100644
--- a/Mathlib/Data/PNat/Basic.lean
+++ b/Mathlib/Data/PNat/Basic.lean
@@ -398,13 +398,11 @@ theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ) := by
   · rcases h with ⟨_, rfl⟩
     apply dvd_mul_right
   · rcases h with ⟨a, h⟩
-    cases a with
-    | zero =>
-      contrapose h
-      apply ne_zero
-    | succ n =>
-      use ⟨n.succ, n.succ_pos⟩
-      rw [← coe_inj, h, mul_coe, mk_coe]
+    obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (n := a) <| by
+      rintro rfl
+      simp only [mul_zero, ne_zero] at h
+    use ⟨n.succ, n.succ_pos⟩
+    rw [← coe_inj, h, mul_coe, mk_coe]
 #align pnat.dvd_iff PNat.dvd_iff
 
 theorem dvd_iff' {k m : ℕ+} : k ∣ m ↔ mod m k = k := by
diff --git a/Mathlib/Mathport/Notation.lean b/Mathlib/Mathport/Notation.lean
index 760f1da9b842c8..93bcd0448f7bf2 100644
--- a/Mathlib/Mathport/Notation.lean
+++ b/Mathlib/Mathport/Notation.lean
@@ -530,7 +530,7 @@ elab (name := notation3) doc:(docComment)? attrs?:(Parser.Term.attributes)? attr
       boundIdents := boundIdents.insert lit.getId lit
       boundValues := boundValues.insert lit.getId <| lit.1.mkAntiquotNode `term
       boundNames := boundNames.push lit.getId
-    | stx => throwUnsupportedSyntax
+    | _stx => throwUnsupportedSyntax
   if hasScoped && !hasBindersItem then
     throwError "If there is a `scoped` item then there must be a `(...)` item for binders."
 
diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean
index 03d9a257e3e870..4f9b210e54203a 100644
--- a/Mathlib/NumberTheory/Divisors.lean
+++ b/Mathlib/NumberTheory/Divisors.lean
@@ -410,8 +410,7 @@ theorem sum_properDivisors_dvd (h : (∑ x in n.properDivisors, x) ∣ n) :
   cases' n with n
   · simp
   · cases' n with n
-    · contrapose! h
-      simp
+    · simp at h
     · rw [or_iff_not_imp_right]
       intro ne_n
       have hlt : ∑ x in n.succ.succ.properDivisors, x < n.succ.succ :=
diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean
index 50b9f425f01d53..13ddbb28421107 100644
--- a/Mathlib/RingTheory/HahnSeries/Summable.lean
+++ b/Mathlib/RingTheory/HahnSeries/Summable.lean
@@ -423,9 +423,7 @@ def embDomain (s : SummableFamily Γ R α) (f : α ↪ β) : SummableFamily Γ R
     · dsimp only at h
       rw [dif_pos hb] at h
       exact Set.mem_iUnion.2 ⟨Classical.choose hb, h⟩
-    · contrapose! h
-      rw [dif_neg hb]
-      simp
+    · simp [-Set.mem_range, dif_neg hb] at h
   finite_co_support' g :=
     ((s.finite_co_support g).image f).subset
       (by
diff --git a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
index 0cd8e9bbf99b32..0790a44dfd43da 100644
--- a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
+++ b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
@@ -108,7 +108,7 @@ theorem homogeneousSubmodule_mul [CommSemiring R] (m n : ℕ) :
   rw [← hde, ← hφ, ← hψ, Finset.sum_subset Finsupp.support_add, Finset.sum_subset hd',
     Finset.sum_subset he', ← Finset.sum_add_distrib]
   · congr
-  all_goals intro i hi; apply Finsupp.not_mem_support_iff.mp
+  all_goals intro _ _; apply Finsupp.not_mem_support_iff.mp
 #align mv_polynomial.homogeneous_submodule_mul MvPolynomial.homogeneousSubmodule_mul
 
 section
diff --git a/Mathlib/RingTheory/PowerSeries/Order.lean b/Mathlib/RingTheory/PowerSeries/Order.lean
index eba22872064350..0e6fc931c32ffd 100644
--- a/Mathlib/RingTheory/PowerSeries/Order.lean
+++ b/Mathlib/RingTheory/PowerSeries/Order.lean
@@ -64,9 +64,7 @@ theorem order_finite_iff_ne_zero : (order φ).Dom ↔ φ ≠ 0 := by
   simp only [order]
   constructor
   · split_ifs with h <;> intro H
-    · contrapose! H
-      simp only [← Part.eq_none_iff']
-      rfl
+    · simp only [PartENat.top_eq_none, Part.not_none_dom] at H
     · exact h
   · intro h
     simp [h]
diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
index 640dc04573bf88..73ce13b3dfec57 100644
--- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean
+++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
@@ -292,7 +292,7 @@ theorem blsub_nadd_of_mono {f : ∀ c < a ♯ b, Ordinal.{max u v}}
 
 theorem nadd_assoc (a b c) : a ♯ b ♯ c = a ♯ (b ♯ c) := by
   rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc]
-  · congr <;> ext (d hd) <;> apply nadd_assoc
+  · congr <;> ext <;> apply nadd_assoc
   · exact fun _ _ h => nadd_le_nadd_left h a
   · exact fun _ _ h => nadd_le_nadd_right h c
 termination_by (a, b, c)
diff --git a/Mathlib/Topology/Algebra/Order/Compact.lean b/Mathlib/Topology/Algebra/Order/Compact.lean
index 005959d581b80b..dad8ea79ad2437 100644
--- a/Mathlib/Topology/Algebra/Order/Compact.lean
+++ b/Mathlib/Topology/Algebra/Order/Compact.lean
@@ -109,9 +109,10 @@ instance (priority := 100) ConditionallyCompleteLinearOrder.toCompactIccSpace (
     rw [diff_subset_iff]
     exact Subset.trans Icc_subset_Icc_union_Ioc <| union_subset_union Subset.rfl <|
       Ioc_subset_Ioc_left hy.1.le
-  rcases hc.2.eq_or_lt with (rfl | hlt); · exact hcs.2
-  contrapose! hf
-  intro U hU
+  rcases hc.2.eq_or_lt with (rfl | hlt)
+  · exact hcs.2
+  exfalso
+  refine hf fun U hU => ?_
   rcases (mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset hlt).1
       (mem_nhdsWithin_of_mem_nhds hU) with
     ⟨y, hxy, hyU⟩
diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean
index e29d37685bd4f0..68949a355b1fd1 100644
--- a/Mathlib/Topology/Connected/Basic.lean
+++ b/Mathlib/Topology/Connected/Basic.lean
@@ -1035,11 +1035,9 @@ theorem isPreconnected_iff_subset_of_disjoint {s : Set α} :
     have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
     exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩
   · intro u v hu hv hs hsu hsv
-    rw [nonempty_iff_ne_empty]
-    intro H
-    specialize h u v hu hv hs H
-    contrapose H
-    apply Nonempty.ne_empty
+    by_contra H
+    specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)
+    apply H
     cases' h with h h
     · rcases hsv with ⟨x, hxs, hxv⟩
       exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩