From 2dda33ddb2d14afd4e949b96f488f14a9d9c0e7b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Aug 2025 08:18:17 -0700 Subject: [PATCH] chore: remove workaround (#10156) --- src/Init/Grind/AC.lean | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/Init/Grind/AC.lean b/src/Init/Grind/AC.lean index d177b2433e..77e62e6aab 100644 --- a/src/Init/Grind/AC.lean +++ b/src/Init/Grind/AC.lean @@ -270,17 +270,11 @@ theorem Seq.eraseDup_k_eq_eraseDup (s : Seq) : s.eraseDup_k = s.eraseDup := by attribute [local simp] Seq.eraseDup_k_eq_eraseDup --- theorem Seq.denote_eraseDup {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (s : Seq) --- : s.eraseDup.denote ctx = s.denote ctx := by --- fun_induction eraseDup s -- FAILED - theorem Seq.denote_eraseDup {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (s : Seq) : s.eraseDup.denote ctx = s.denote ctx := by - induction s <;> simp [eraseDup] <;> split <;> split - next ih _ _ h₁ h₂ => simp [← ih, h₁, h₂, Std.IdempotentOp.idempotent] - next ih _ _ h₁ _ => simp [← ih, h₁] - next ih _ _ _ h₁ h₂ => simp [← ih, h₁, h₂, ← Std.Associative.assoc (self := inst₁), Std.IdempotentOp.idempotent] - next ih _ _ _ h₁ _ => simp [← ih, h₁] + fun_induction eraseDup s <;> simp_all +zetaDelta + next ih => simp [← ih, Std.IdempotentOp.idempotent] + next ih => simp [← ih, ← Std.Associative.assoc (self := inst₁), Std.IdempotentOp.idempotent] attribute [local simp] Seq.denote_eraseDup