From ddfe9c5bdb772c808634265c345e9cad6d71c0bf Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@meta.com>
Date: Mon, 5 Aug 2024 20:08:20 +0000
Subject: [PATCH] update tests

---
 tests/interaction/test_tactics.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/interaction/test_tactics.py b/tests/interaction/test_tactics.py
index 66a347a..1aba648 100644
--- a/tests/interaction/test_tactics.py
+++ b/tests/interaction/test_tactics.py
@@ -130,10 +130,10 @@ def test_example_length_le(batteries_repo: LeanGitRepo) -> None:
     thm = Theorem(
         batteries_repo,
         "Batteries/Data/List/Lemmas.lean",
-        "List.IsSuffix.length_le",
+        "List.disjoint_of_disjoint_append_right_right",
     )
     with Dojo(thm) as (dojo, s0):
-        s1 = dojo.run_tac(s0, "exact h.sublist.length_le")
+        s1 = dojo.run_tac(s0, "exact (disjoint_append_right.1 d).2")
         assert isinstance(s1, ProofFinished)
         assert dojo.is_successful