chore: adaptations for nightly-2025-11-23

Author: mathlib4-bot

Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

@@ -540,7 +540,7 @@ lemma liftCochain_descCochain :
 lemma liftCochain_v_descCochain_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + n' = p₃)
     (q : ℤ) (hq : p₁ + m = q) :
     (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (descCochain φ α' β' h').v p₂ p₃ h₂₃ =
-      α.v p₁ q hq ≫ α'.v q p₃ (by grind +revert) + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃ := by
+      α.v p₁ q hq ≫ α'.v q p₃ (by grind) + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃ := by
   have eq := Cochain.congr_v (liftCochain_descCochain φ α β α' β' h h' p hp) p₁ p₃ (by cutsat)
   simpa only [Cochain.comp_v _ _ hp p₁ p₂ p₃ h₁₂ h₂₃, Cochain.add_v,
     Cochain.comp_v _ _ _ _ _ _ hq (show q + m' = p₃ by cutsat)] using eq

Mathlib/Algebra/Ring/GeomSum.lean

@@ -65,7 +65,7 @@ lemma op_geom_sum₂ (x y : R) (n : ℕ) : ∑ i ∈ range n, op y ^ (n - 1 - i)
     ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i) := by
   rw [← sum_range_reflect]
   refine sum_congr rfl fun j j_in => ?_
-  grind +revert
+  grind
 
 lemma geom_sum₂_with_one (x : R) (n : ℕ) :
     ∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ range n, x ^ i :=

Mathlib/Data/List/Sigma.lean

@@ -180,7 +180,7 @@ theorem dlookup_cons_ne (l) {a} : ∀ s : Sigma β, a ≠ s.1 → dlookup a (s :
 theorem dlookup_isSome {a : α} {l : List (Sigma β)} : (dlookup a l).isSome ↔ a ∈ l.keys := by
   induction l with
   | nil => simp
-  | cons s _ _ => by_cases a = s.fst <;> grind +revert
+  | cons s _ _ => by_cases a = s.fst <;> grind
 
 theorem dlookup_eq_none {a : α} {l : List (Sigma β)} : dlookup a l = none ↔ a ∉ l.keys := by
   simp [← dlookup_isSome, Option.isNone_iff_eq_none]
@@ -189,7 +189,7 @@ theorem of_mem_dlookup {a : α} {b : β a} {l : List (Sigma β)} :
     b ∈ dlookup a l → Sigma.mk a b ∈ l := by
   induction l with
   | nil => grind
-  | cons s _ _ => by_cases a = s.fst <;> grind +revert
+  | cons s _ _ => by_cases a = s.fst <;> grind
 
 theorem mem_dlookup {a} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : Sigma.mk a b ∈ l) :
     b ∈ dlookup a l := by
@@ -201,7 +201,7 @@ theorem map_dlookup_eq_find (a : α) (l : List (Sigma β)) :
     (dlookup a l).map (Sigma.mk a) = find? (fun s => a = s.1) l := by
   induction l with
   | nil => grind
-  | cons s _ _ => by_cases s.fst = a <;> grind +revert
+  | cons s _ _ => by_cases s.fst = a <;> grind
 
 theorem mem_dlookup_iff {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) :
     b ∈ dlookup a l ↔ Sigma.mk a b ∈ l :=
@@ -223,7 +223,7 @@ theorem dlookup_map (l : List (Sigma β))
   | nil => grind
   | cons s _ _ =>
     have (h : a ≠ s.fst) : ¬ f a = (⟨f s.fst, g s.fst s.snd⟩ : Sigma β').fst := fun he => h <| hf he
-    by_cases a = s.fst <;> grind +revert [Sigma.map]
+    by_cases a = s.fst <;> grind [Sigma.map]
 
 theorem dlookup_map₁ {β : Type v} (l : List (Σ _ : α, β))
     {f : α → α'} (hf : Function.Injective f) (a : α) :
@@ -261,7 +261,7 @@ theorem dlookup_append (l₁ l₂ : List (Sigma β)) (a : α) :
     (l₁ ++ l₂).dlookup a = (l₁.dlookup a).or (l₂.dlookup a) := by
   induction l₁ with
   | nil => rfl
-  | cons s _ _ => by_cases a = s.fst <;> grind +revert
+  | cons s _ _ => by_cases a = s.fst <;> grind
 
 theorem sublist_dlookup {l₁ l₂ : List (Sigma β)} {a : α} {b : β a}
     (nd₂ : l₂.NodupKeys) (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) : b ∈ l₂.dlookup a := by

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -545,7 +545,7 @@ theorem descFactorial_eq_descFactorialBinary : descFactorial = descFactorialBina
   split_ifs with h
   · rw [descFactorial_of_lt h]
   · rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']
-    grind +revert
+    grind
 
 /-!
 We are now limited by time, not stack space,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-11-22
+leanprover/lean4:nightly-2025-11-23