1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52

diff --git a/Mathlib/Algebra/Group/ModEq.lean b/Mathlib/Algebra/Group/ModEq.lean
index d35b844522..ba114ce43d 100644
--- a/Mathlib/Algebra/Group/ModEq.lean
+++ b/Mathlib/Algebra/Group/ModEq.lean
@@ -266,7 +266,7 @@ end ModEq
 @[simp]
 theorem zsmul_modEq_zsmul [IsAddTorsionFree G] (hn : z ≠ 0) :
     z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p] := by
-  simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm, zsmul_right_inj hn]
+  simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm p z _, zsmul_right_inj hn]
 
 alias ⟨ModEq.zsmul_cancel, _⟩ := zsmul_modEq_zsmul
 
diff --git a/Mathlib/Order/CompleteBooleanAlgebra.lean b/Mathlib/Order/CompleteBooleanAlgebra.lean
index d88e49e2b0..42e36e1eba 100644
--- a/Mathlib/Order/CompleteBooleanAlgebra.lean
+++ b/Mathlib/Order/CompleteBooleanAlgebra.lean
@@ -450,7 +450,7 @@ theorem sSup_disjoint_iff {s : Set α} : Disjoint (sSup s) a ↔ ∀ b ∈ s, Di
   simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]
 
 theorem disjoint_sSup_iff {s : Set α} : Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b := by
-  simpa only [disjoint_comm] using @sSup_disjoint_iff
+  simpa only [disjoint_comm] using @sSup_disjoint_iff α _ a
 
 theorem iSup_inf_of_monotone {ι : Type*} [Preorder ι] [IsDirectedOrder ι] {f g : ι → α}
     (hf : Monotone f) (hg : Monotone g) : ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i := by
diff --git a/Mathlib/Order/Interval/Set/Basic.lean b/Mathlib/Order/Interval/Set/Basic.lean
index 46bd529714..a086e8f643 100644
--- a/Mathlib/Order/Interval/Set/Basic.lean
+++ b/Mathlib/Order/Interval/Set/Basic.lean
@@ -595,7 +595,7 @@ theorem Icc_diff_right : Icc a b \ {b} = Ico a b :=
 
 @[simp]
 theorem Ico_diff_left : Ico a b \ {a} = Ioo a b :=
-  ext fun x => by simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]
+  ext fun x => by grind [← lt_iff_le_and_ne]
 
 @[simp]
 theorem Ioc_diff_right : Ioc a b \ {b} = Ioo a b :=
diff --git a/Mathlib/Order/Interval/Set/SuccPred.lean b/Mathlib/Order/Interval/Set/SuccPred.lean
index 9e9a0bdcff..6e76332ddf 100644
--- a/Mathlib/Order/Interval/Set/SuccPred.lean
+++ b/Mathlib/Order/Interval/Set/SuccPred.lean
@@ -67,7 +67,7 @@ lemma Ico_succ_succ_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) :
 /-! ##### Inserting into intervals -/
 
 lemma insert_Icc_succ_left_eq_Icc (h : a ≤ b) : insert a (Icc (succ a) b) = Icc a b := by
-  ext x; simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]; aesop
+  ext x; simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]; grind [← le_iff_eq_or_succ_le]
 
 lemma insert_Icc_right_eq_Icc_succ (h : a ≤ succ b) :
     insert (succ b) (Icc a b) = Icc a (succ b) := by