chore: fix test

Some goals in the test are now closed by `grind`.
leanprover · Dec 27, 2024 · 71e1701 · 71e1701
1 parent 74bbd88
commit 71e1701
Showing 1 changed file with 0 additions and 27 deletions.
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
@@ -21,24 +21,6 @@ theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
 open Lean.Grind.Eager in
 /--
 error: `grind` failed
-a b c : Bool
-p q : Prop
-left✝ : a = true
-h✝ : b = true
-left : p
-right : q
-h : b = false
-⊢ False
-
-a b c : Bool
-p q : Prop
-left✝ : a = true
-h✝ : b = true
-left : p
-right : q
-h : a = false
-⊢ False
-
 a b c : Bool
 p q : Prop
 left✝ : a = true
@@ -47,15 +29,6 @@ left : p
 right : q
 h : b = false
 ⊢ False
-
-a b c : Bool
-p q : Prop
-left✝ : a = true
-h✝ : c = true
-left : p
-right : q
-h : a = false
-⊢ False
 -/
 #guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by