From a0706e71004618aaf7167bdd147bc95b85d3fe52 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 11 Jul 2026 08:03:06 +0300
Subject: [PATCH] chore(Data/Seq/Computation): golf using `grind`

---
 Mathlib/Data/Seq/Computation.lean | 113 ++++++++----------------------
 1 file changed, 28 insertions(+), 85 deletions(-)

diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
index 07b1fbbd784efd..85f752b5add4da 100644
--- a/Mathlib/Data/Seq/Computation.lean
+++ b/Mathlib/Data/Seq/Computation.lean
@@ -880,29 +880,14 @@ theorem lift_eq_iff_equiv (c₁ c₂ : Computation α) : LiftRel (· = ·) c₁
      fun a2 => by let ⟨b, b1, ab⟩ := h2 a2; rwa [← ab]⟩,
     fun e => ⟨fun {a} a1 => ⟨a, (e _).1 a1, rfl⟩, fun {a} a2 => ⟨a, (e _).2 a2, rfl⟩⟩⟩
 
-instance LiftRel.refl (R : α → α → Prop) [Std.Refl R] : Std.Refl (LiftRel R) where
-  refl _ := ⟨fun {a} as => ⟨a, as, refl_of R a⟩, fun {b} bs => ⟨b, bs, refl_of R b⟩⟩
-
-instance LiftRel.symm (R : α → α → Prop) [Std.Symm R] : Std.Symm (LiftRel R) where
-  symm _ _ := fun ⟨l, r⟩ ↦ {
-    left a2 :=
-      let ⟨b, b1, ab⟩ := r a2
-      ⟨b, b1, symm_of R ab⟩
-    right a1 :=
-      let ⟨b, b2, ab⟩ := l a1
-      ⟨b, b2, symm_of R ab⟩
-  }
-
-instance LiftRel.trans (R : α → α → Prop) [IsTrans α R] : IsTrans _ (LiftRel R) :=
-  ⟨fun _ _ _ ⟨l1, r1⟩ ⟨l2, r2⟩ =>
-  ⟨fun {_a} a1 =>
-    let ⟨_b, b2, ab⟩ := l1 a1
-    let ⟨c, c3, bc⟩ := l2 b2
-    ⟨c, c3, trans_of R ab bc⟩,
-    fun {_c} c3 =>
-    let ⟨_b, b2, bc⟩ := r2 c3
-    let ⟨a, a1, ab⟩ := r1 b2
-    ⟨a, a1, trans_of R ab bc⟩⟩⟩
+instance LiftRel.refl (R : α → α → Prop) [Std.Refl R] : Std.Refl (LiftRel R) := by
+  grind [refl_def, LiftRel]
+
+instance LiftRel.symm (R : α → α → Prop) [Std.Symm R] : Std.Symm (LiftRel R) := by
+  grind [symm_def, LiftRel]
+
+instance LiftRel.trans (R : α → α → Prop) [IsTrans α R] : IsTrans _ (LiftRel R) := by
+  grind [isTrans_def, LiftRel]
 
 theorem LiftRel.equiv (R : α → α → Prop) (H : Equivalence R) : Equivalence (LiftRel R) where
   refl := @LiftRel.refl α R H.stdRefl |>.refl
@@ -910,35 +895,20 @@ theorem LiftRel.equiv (R : α → α → Prop) (H : Equivalence R) : Equivalence
   trans := @LiftRel.trans α R H.isTrans |>.trans _ _ _
 
 theorem LiftRel.imp {R S : α → β → Prop} (H : ∀ {a b}, R a b → S a b) (s t) :
-    LiftRel R s t → LiftRel S s t
-  | ⟨l, r⟩ =>
-    ⟨fun {_} as =>
-      let ⟨b, bt, ab⟩ := l as
-      ⟨b, bt, H ab⟩,
-      fun {_} bt =>
-      let ⟨a, as, ab⟩ := r bt
-      ⟨a, as, H ab⟩⟩
+    LiftRel R s t → LiftRel S s t := by
+  grind [LiftRel]
 
 theorem terminates_of_liftRel {R : α → β → Prop} {s t} :
-    LiftRel R s t → (Terminates s ↔ Terminates t)
-  | ⟨l, r⟩ =>
-    ⟨fun ⟨⟨_, as⟩⟩ =>
-      let ⟨b, bt, _⟩ := l as
-      ⟨⟨b, bt⟩⟩,
-      fun ⟨⟨_, bt⟩⟩ =>
-      let ⟨a, as, _⟩ := r bt
-      ⟨⟨a, as⟩⟩⟩
+    LiftRel R s t → (Terminates s ↔ Terminates t) := by
+  grind [LiftRel, Terminates]
 
 theorem rel_of_liftRel {R : α → β → Prop} {ca cb} :
-    LiftRel R ca cb → ∀ {a b}, a ∈ ca → b ∈ cb → R a b
-  | ⟨l, _⟩, a, b, ma, mb => by
-    let ⟨b', mb', ab'⟩ := l ma
-    rw [mem_unique mb mb']; exact ab'
+    LiftRel R ca cb → ∀ {a b}, a ∈ ca → b ∈ cb → R a b := by
+  grind [LiftRel, mem_unique]
 
 theorem liftRel_of_mem {R : α → β → Prop} {a b ca cb} (ma : a ∈ ca) (mb : b ∈ cb) (ab : R a b) :
-    LiftRel R ca cb :=
-  ⟨fun {a'} ma' => by rw [mem_unique ma' ma]; exact ⟨b, mb, ab⟩, fun {b'} mb' => by
-    rw [mem_unique mb' mb]; exact ⟨a, ma, ab⟩⟩
+    LiftRel R ca cb := by
+  grind [LiftRel, mem_unique]
 
 theorem exists_of_liftRel_left {R : α → β → Prop} {ca cb} (H : LiftRel R ca cb) {a} (h : a ∈ ca) :
     ∃ b, b ∈ cb ∧ R a b :=
@@ -949,42 +919,19 @@ theorem exists_of_liftRel_right {R : α → β → Prop} {ca cb} (H : LiftRel R
   H.right h
 
 theorem liftRel_def {R : α → β → Prop} {ca cb} :
-    LiftRel R ca cb ↔ (Terminates ca ↔ Terminates cb) ∧ ∀ {a b}, a ∈ ca → b ∈ cb → R a b :=
-  ⟨fun h =>
-    ⟨terminates_of_liftRel h, fun {a b} ma mb => by
-      let ⟨b', mb', ab⟩ := h.left ma
-      rwa [mem_unique mb mb']⟩,
-    fun ⟨l, r⟩ =>
-    ⟨fun {_} ma =>
-      let ⟨⟨b, mb⟩⟩ := l.1 ⟨⟨_, ma⟩⟩
-      ⟨b, mb, r ma mb⟩,
-      fun {_} mb =>
-      let ⟨⟨a, ma⟩⟩ := l.2 ⟨⟨_, mb⟩⟩
-      ⟨a, ma, r ma mb⟩⟩⟩
+    LiftRel R ca cb ↔ (Terminates ca ↔ Terminates cb) ∧ ∀ {a b}, a ∈ ca → b ∈ cb → R a b := by
+  grind [LiftRel, Terminates, terminates_of_liftRel, mem_unique]
 
 theorem liftRel_bind {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
     {s2 : Computation β} {f1 : α → Computation γ} {f2 : β → Computation δ} (h1 : LiftRel R s1 s2)
-    (h2 : ∀ {a b}, R a b → LiftRel S (f1 a) (f2 b)) : LiftRel S (bind s1 f1) (bind s2 f2) :=
-  let ⟨l1, r1⟩ := h1
-  ⟨fun {_} cB =>
-    let ⟨_, a1, c₁⟩ := exists_of_mem_bind cB
-    let ⟨_, b2, ab⟩ := l1 a1
-    let ⟨l2, _⟩ := h2 ab
-    let ⟨_, d2, cd⟩ := l2 c₁
-    ⟨_, mem_bind b2 d2, cd⟩,
-    fun {_} dB =>
-    let ⟨_, b1, d1⟩ := exists_of_mem_bind dB
-    let ⟨_, a2, ab⟩ := r1 b1
-    let ⟨_, r2⟩ := h2 ab
-    let ⟨_, c₂, cd⟩ := r2 d1
-    ⟨_, mem_bind a2 c₂, cd⟩⟩
+    (h2 : ∀ {a b}, R a b → LiftRel S (f1 a) (f2 b)) : LiftRel S (bind s1 f1) (bind s2 f2) where
+  left cB := by grind [exists_of_mem_bind cB, mem_bind, LiftRel]
+  right dB := by grind [exists_of_mem_bind dB, mem_bind, LiftRel]
 
 @[simp]
 theorem liftRel_pure_left (R : α → β → Prop) (a : α) (cb : Computation β) :
-    LiftRel R (pure a) cb ↔ ∃ b, b ∈ cb ∧ R a b :=
-  ⟨fun ⟨l, _⟩ => l (ret_mem _), fun ⟨b, mb, ab⟩ =>
-    ⟨fun {a'} ma' => by rw [eq_of_pure_mem ma']; exact ⟨b, mb, ab⟩, fun {b'} mb' =>
-      ⟨_, ret_mem _, by rw [mem_unique mb' mb]; exact ab⟩⟩⟩
+    LiftRel R (pure a) cb ↔ ∃ b, b ∈ cb ∧ R a b := by
+  grind [LiftRel, eq_of_pure_mem, ret_mem, mem_unique]
 
 @[simp]
 theorem liftRel_pure_right (R : α → β → Prop) (ca : Computation α) (b : β) :
@@ -996,10 +943,8 @@ theorem liftRel_pure (R : α → β → Prop) (a : α) (b : β) :
 
 @[simp]
 theorem liftRel_think_left (R : α → β → Prop) (ca : Computation α) (cb : Computation β) :
-    LiftRel R (think ca) cb ↔ LiftRel R ca cb :=
-  and_congr (forall_congr' fun _ => imp_congr ⟨of_think_mem, think_mem⟩ Iff.rfl)
-    (forall_congr' fun _ =>
-      imp_congr Iff.rfl <| exists_congr fun _ => and_congr ⟨of_think_mem, think_mem⟩ Iff.rfl)
+    LiftRel R (think ca) cb ↔ LiftRel R ca cb := by
+  grind [LiftRel, of_think_mem, think_mem]
 
 @[simp]
 theorem liftRel_think_right (R : α → β → Prop) (ca : Computation α) (cb : Computation β) :
@@ -1011,10 +956,8 @@ theorem liftRel_mem_cases {R : α → β → Prop} {ca cb} (Ha : ∀ a ∈ ca, L
   ⟨fun {_} ma => (Ha _ ma).left ma, fun {_} mb => (Hb _ mb).right mb⟩
 
 theorem liftRel_congr {R : α → β → Prop} {ca ca' : Computation α} {cb cb' : Computation β}
-    (ha : ca ~ ca') (hb : cb ~ cb') : LiftRel R ca cb ↔ LiftRel R ca' cb' :=
-  and_congr
-    (forall_congr' fun _ => imp_congr (ha _) <| exists_congr fun _ => and_congr (hb _) Iff.rfl)
-    (forall_congr' fun _ => imp_congr (hb _) <| exists_congr fun _ => and_congr (ha _) Iff.rfl)
+    (ha : ca ~ ca') (hb : cb ~ cb') : LiftRel R ca cb ↔ LiftRel R ca' cb' := by
+  grind [Equiv, LiftRel]
 
 theorem liftRel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
     {s2 : Computation β} {f1 : α → γ} {f2 : β → δ} (h1 : LiftRel R s1 s2)
@@ -1054,7 +997,7 @@ theorem LiftRelAux.ret_left (R : α → β → Prop) (C : Computation α → Com
   induction cb using recOn with
   | pure b =>
     exact
-      ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
+      ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rwa [mem_unique (ret_mem _) mb]⟩
   | think cb =>
     rw [destruct_think]
     exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩