cleanup tests

leanprover-community · May 6, 2024 · 683fa0c · 683fa0c
1 parent 68ddd10
commit 683fa0c
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/test/Mathlib/test/20240209.lean b/test/Mathlib/test/20240209.lean
@@ -1,4 +1,2 @@
-import Std.Tactic.Simpa
-
 example : False := by
   simpa using show False by done
diff --git a/test/Mathlib/test/H20231214.lean b/test/Mathlib/test/H20231214.lean
@@ -27,4 +27,4 @@ theorem mathd_algebra_35
 have hQ : ∀ x, p x = 6 / x := by
   intro x
   calc p x = 6 / x * p x := h₀ (x)
-     _ = (6/2) * 6 / x * (6 / x) := sub_sub_sub_cancel sq_ne_zero
+     _ = (6/2) * 6 / x * (6 / x) := sorry