fixes

Author: kim-em

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -225,7 +225,10 @@ end Fewnomials
 theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
     coeff (p * Polynomial.X ^ n) (d + n) = coeff p d := by
   rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-  all_goals grind [mem_antidiagonal, mul_zero]
+  · rintro ⟨i, j⟩ h1 h2
+    rw [coeff_X_pow, if_neg, mul_zero]
+    grind [mem_antidiagonal]
+  · grind [mem_antidiagonal]
 
 @[simp]
 theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) :

Mathlib/Data/ENNReal/Inv.lean

@@ -231,9 +231,11 @@ protected theorem div_le_iff' {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ 
 protected theorem mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) :
     (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
   cases b
-  case top => grind [mul_top, mul_zero, inv_top, ENNReal.inv_eq_zero]
+  case top => simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true,
+    or_true, mul_top, inv_top, mul_zero]
   cases a
-  case top => grind [top_mul, zero_mul, inv_top, ENNReal.inv_eq_zero]
+  case top => simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self,
+    not_true_eq_false, coe_eq_zero, false_or, top_mul, inv_top, zero_mul]
   grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero,
     =_ coe_inv, zero_mul, = mul_eq_zero, mul_top, mul_zero, top_mul]
 

Mathlib/Data/List/Cycle.lean

@@ -300,7 +300,7 @@ theorem next_eq_getElem {l : List α} {a : α} (ha : a ∈ l) :
 
 theorem next_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
     l.next l[i] (get_mem ..) = l[(i + 1) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt hi)) := by
-  grind [next_eq_getElem, idxOf_getElem]
+  grind [next_eq_getElem]
 
 theorem prev_eq_getElem?_idxOf_pred_of_ne_head {l : List α} {a : α} (ha : a ∈ l)
     (ha₀ : a ≠ l.head (ne_nil_of_mem ha)) : l.prev a ha = l[l.idxOf a - 1]? := by
@@ -338,7 +338,7 @@ theorem prev_eq_getElem {l : List α} {a : α} (ha : a ∈ l) :
 
 theorem prev_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
     l.prev l[i] (get_mem ..) = l[(i + (l.length - 1)) % l.length]'(Nat.mod_lt _ (by lia)) := by
-  grind [prev_eq_getElem, idxOf_getElem]
+  grind [prev_eq_getElem]
 
 @[simp]
 theorem next_getLast_eq_head (l : List α) (h : l ≠ []) (hn : l.Nodup) :