chore(AlgebraicTopology): refactor proofs where grind? fails

Mathlib/AlgebraicTopology/SimplexCategory/DeltaZeroIter.lean

@@ -119,7 +119,7 @@ def σ₀Iter (i : ℕ) {n m : ℕ} (hi : n + i = m := by lia) : ⦋m⦌ ⟶ ⦋
   Hom.mk
     { toFun j :=
         if j.val < i then 0 else ⟨j.val - i, by lia⟩
-      monotone' _ _ _ := by grind [Fin.zero_le] }
+      monotone' a _ _ := by grind [Fin.zero_le] }
 
 lemma σ₀Iter_coe_eq_of_lt (i : ℕ) {n m : ℕ}
     (j : Fin (m + 1)) (hi : n + i = m := by lia) (hj : j.val < i := by grind) :

Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

@@ -169,7 +169,10 @@ theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : IsAdmissible (m + 1)
     IsAdmissible m <| simplicialInsert j L := by
   induction L generalizing j m with
   | nil => exact IsAdmissible.singleton hj
-  | cons a L h_rec => cases L <;> grind
+  | cons a L h_rec =>
+    cases L
+    · grind
+    · grind only [simplicialInsert, = isAdmissible_cons_cons_iff]
 
 end AdmissibleLists
 
@@ -226,8 +229,9 @@ def simplicialEvalσ (L : List ℕ) : ℕ → ℕ :=
 lemma simplicialEvalσ_of_le_mem (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) : simplicialEvalσ L j = j := by
   induction L with | nil => grind | cons _ _ _ => simp only [List.forall_mem_cons] at hj; grind
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 lemma simplicialEvalσ_monotone (L : List ℕ) : Monotone (simplicialEvalσ L) := by
-  induction L <;> grind [Monotone]
+  induction L <;> grind only [Monotone, simplicialEvalσ]
 
 variable {m}
 

Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean

@@ -67,9 +67,10 @@ lemma induction_mk {motive : X.N → Sort*}
     (mk : ∀ (n : ℕ) (x : X.nonDegenerate n), motive (mk x.1 x.2)) {n : ℕ} (s : X.nonDegenerate n) :
   induction (motive := motive) mk (N.mk s.val s.property) = mk n s := rfl
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 lemma ext_iff (x y : X.N) :
     x = y ↔ x.toS = y.toS := by
-  grind [cases SSet.N]
+  grind only [cases SSet.N]
 
 instance : Preorder X.N := Preorder.lift toS
 

Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean

@@ -53,9 +53,10 @@ lemma mk_surjective (s : A.N) :
       (hx' : x ∉ A.obj _), s = mk x hx hx' :=
   ⟨s.dim, s.simplex, s.nonDegenerate, s.notMem, rfl⟩
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 lemma ext_iff (x y : A.N) :
     x = y ↔ x.toN = y.toN := by
-  grind [cases SSet.Subcomplex.N]
+  grind only [cases SSet.Subcomplex.N]
 
 variable (A) in
 @[elab_as_elim]