feat: improve grind case-split on Iff (#6940)

This PR improves how the `grind` tactic performs case splits on `p <->
q`.

src/Init/Grind/Lemmas.lean

@@ -101,9 +101,9 @@ theorem Bool.false_of_not_eq_self {a : Bool} (h : (!a) = a) : False := by
   by_cases a <;> simp_all
 
 /- The following two helper theorems are used to case-split `a = b` representing `iff`. -/
-theorem of_eq_eq_true {a b : Prop} (h : (a = b) = True) : (¬a ∨ b) ∧ (¬b ∨ a) := by
+theorem of_eq_eq_true {a b : Prop} (h : (a = b) = True) : (a ∧ b) ∨ (¬ a ∧ ¬ b) := by
   by_cases a <;> by_cases b <;> simp_all
-theorem of_eq_eq_false {a b : Prop} (h : (a = b) = False) : (¬a ∨ ¬b) ∧ (b ∨ a) := by
+theorem of_eq_eq_false {a b : Prop} (h : (a = b) = False) : (a ∧ ¬b) ∨ (¬ a ∧ b) := by
   by_cases a <;> by_cases b <;> simp_all
 
 /-! Forall -/

tests/lean/run/grind_pre.lean

@@ -157,31 +157,24 @@ p q r : Prop
 h₁ : HEq p a
 h₂ : HEq q a
 h₃ : p = r
-left : ¬p ∨ r
-h : ¬r
+left : p
+right : r
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
     [prop] HEq p a
     [prop] HEq q a
     [prop] p = r
-    [prop] ¬p ∨ r
-    [prop] ¬r ∨ p
-    [prop] ¬r
+    [prop] p
+    [prop] r
   [eqc] True propositions
     [prop] p = r
-    [prop] ¬p ∨ r
-    [prop] ¬r ∨ p
-    [prop] ¬p
-    [prop] ¬r
-  [eqc] False propositions
     [prop] a
     [prop] p
     [prop] q
     [prop] r
   [cases] Case analyses
-    [cases] [1/1]: p = r
-    [cases] [1/2]: ¬r ∨ p
+    [cases] [1/2]: p = r
 [grind] Issues
   [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/