feat: simplify cooper case-split proof (#7370)

This PR simplifies the proof term due to the Cooper's conflict
resolution in cutsat.

src/Init/Data/Int/Linear.lean

@@ -1102,6 +1102,16 @@ theorem orOver_resolve {n p} : OrOver (n+1) p → ¬ p n → OrOver n p := by
   · contradiction
   · assumption
 
+def OrOver_cases_type (n : Nat) (p : Nat → Prop) : Prop :=
+  match n with
+  | 0 => p 0
+  | n+1 => ¬ p (n+1) → OrOver_cases_type n p
+
+theorem orOver_cases {n p} : OrOver (n+1) p → OrOver_cases_type n p := by
+  induction n <;> simp [OrOver_cases_type]
+  next => exact orOver_one
+  next n ih => intro h₁ h₂; exact ih (orOver_resolve h₁ h₂)
+
 private theorem orOver_of_p {i n p} (h₁ : i < n) (h₂ : p i) : OrOver n p := by
   induction n
   next => simp at h₁

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -186,16 +186,16 @@ partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s
     -- `pred` is an expressions of the form `cooper_*_split ...` with type `Nat → Prop`
     let mut k := n
     let mut result := base -- `OrOver k (cooper_*_splti)
-    -- `result` is of the form `OrOver k pred`, we resolve it using `hs`
+    result := mkApp3 (mkConst ``Int.Linear.orOver_cases) (toExpr (n-1)) pred result
     for (fvarId, c) in hs do
       let type := mkApp pred (toExpr (k-1))
       let h ← c.toExprProofCore -- proof of `False`
       -- `hNotCase` is a proof for `¬ pred (k-1)`
       let hNotCase := mkLambda `h .default type (h.abstract #[mkFVar fvarId])
-      result := mkApp4 (mkConst ``Int.Linear.orOver_resolve) (toExpr (k-1)) pred result hNotCase
+      result := mkApp result hNotCase
       k := k - 1
-    -- `result` is now a proof of `OrOver 1 pred`
-    return mkApp2 (mkConst ``Int.Linear.orOver_one) pred result
+    -- `result` is now a proof of `p 0`
+    return result
 
 partial def UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr := do
   match h with