chore(Tactic/ComputeAsymptotics): avoid defeq abuse in destruct_eq_cons (leanprover-community#37459)

vasnesterov · vasnesterov · commit 35638f90bcb5 · 2026-04-01T02:16:40.000Z
Avoid defeq abuse in the proof of `ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_eq_cons`.
diff --git a/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean b/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean
@@ -221,8 +221,8 @@ theorem destruct_eq_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : Multi
     {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl}
     (h : destruct ms = some (exp, coef, tl)) : ms = cons exp coef tl := by
   apply Stream'.Seq.destruct_eq_cons
-  simp [destruct] at h
-  grind
+  rw [destruct_eq_destruct_map, h]
+  rfl
 
 @[simp]
 theorem head_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} :
