update tests

lean-dojo · Aug 5, 2024 · ddfe9c5 · ddfe9c5
1 parent e662bc5
commit ddfe9c5
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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