diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean
index 6a6a571abb8a..af289da274d8 100644
--- a/src/Init/Grind/Lemmas.lean
+++ b/src/Init/Grind/Lemmas.lean
@@ -12,6 +12,9 @@ import Init.Grind.Util
 
 namespace Lean.Grind
 
+theorem rfl_true : true = true :=
+  rfl
+
 theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
   fun hp => h (he.mp hp)
 
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 657543d536c5..26d333ee796d 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -11,14 +11,14 @@ import Lean.Meta.DecLevel
 
 namespace Lean.Meta
 
-/-- Return `id e` -/
+/-- Returns `id e` -/
 def mkId (e : Expr) : MetaM Expr := do
   let type ← inferType e
   let u    ← getLevel type
   return mkApp2 (mkConst ``id [u]) type e
 
 /--
-  Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, return
+  Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, returns
   term `@id expectedType e`. -/
 def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
   let u ← getLevel expectedType
@@ -38,13 +38,13 @@ def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
   let u2 ← getLevel ety
   return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]
 
-/-- Return `a = b`. -/
+/-- Returns `a = b`. -/
 def mkEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getLevel aType
   return mkApp3 (mkConst ``Eq [u]) aType a b
 
-/-- Return `HEq a b`. -/
+/-- Returns `HEq a b`. -/
 def mkHEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let bType ← inferType b
@@ -52,7 +52,7 @@ def mkHEq (a b : Expr) : MetaM Expr := do
   return mkApp4 (mkConst ``HEq [u]) aType a bType b
 
 /--
-  If `a` and `b` have definitionally equal types, return `Eq a b`, otherwise return `HEq a b`.
+  If `a` and `b` have definitionally equal types, returns `Eq a b`, otherwise returns `HEq a b`.
 -/
 def mkEqHEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
@@ -63,25 +63,25 @@ def mkEqHEq (a b : Expr) : MetaM Expr := do
   else
     return mkApp4 (mkConst ``HEq [u]) aType a bType b
 
-/-- Return a proof of `a = a`. -/
+/-- Returns a proof of `a = a`. -/
 def mkEqRefl (a : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getLevel aType
   return mkApp2 (mkConst ``Eq.refl [u]) aType a
 
-/-- Return a proof of `HEq a a`. -/
+/-- Returns a proof of `HEq a a`. -/
 def mkHEqRefl (a : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getLevel aType
   return mkApp2 (mkConst ``HEq.refl [u]) aType a
 
-/-- Given `hp : P` and `nhp : Not P` returns an instance of type `e`. -/
+/-- Given `hp : P` and `nhp : Not P`, returns an instance of type `e`. -/
 def mkAbsurd (e : Expr) (hp hnp : Expr) : MetaM Expr := do
   let p ← inferType hp
   let u ← getLevel e
   return mkApp4 (mkConst ``absurd [u]) p e hp hnp
 
-/-- Given `h : False`, return an instance of type `e`. -/
+/-- Given `h : False`, returns an instance of type `e`. -/
 def mkFalseElim (e : Expr) (h : Expr) : MetaM Expr := do
   let u ← getLevel e
   return mkApp2 (mkConst ``False.elim [u]) e h
@@ -108,7 +108,7 @@ def mkEqSymm (h : Expr) : MetaM Expr := do
       return mkApp4 (mkConst ``Eq.symm [u]) α a b h
     | none => throwAppBuilderException ``Eq.symm ("equality proof expected" ++ hasTypeMsg h hType)
 
-/-- Given `h₁ : a = b` and `h₂ : b = c` returns a proof of `a = c`. -/
+/-- Given `h₁ : a = b` and `h₂ : b = c`, returns a proof of `a = c`. -/
 def mkEqTrans (h₁ h₂ : Expr) : MetaM Expr := do
   if h₁.isAppOf ``Eq.refl then
     return h₂
@@ -185,7 +185,7 @@ def mkHEqOfEq (h : Expr) : MetaM Expr := do
   return mkApp4 (mkConst ``heq_of_eq [u]) α a b h
 
 /--
-If `e` is `@Eq.refl α a`, return `a`.
+If `e` is `@Eq.refl α a`, returns `a`.
 -/
 def isRefl? (e : Expr) : Option Expr := do
   if e.isAppOfArity ``Eq.refl 2 then
@@ -194,7 +194,7 @@ def isRefl? (e : Expr) : Option Expr := do
     none
 
 /--
-If `e` is `@congrArg α β a b f h`, return `α`, `f` and `h`.
+If `e` is `@congrArg α β a b f h`, returns `α`, `f` and `h`.
 Also works if `e` can be turned into such an application (e.g. `congrFun`).
 -/
 def congrArg? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
@@ -336,13 +336,14 @@ private def withAppBuilderTrace [ToMessageData α] [ToMessageData β]
       throw ex
 
 /--
-  Return the application `constName xs`.
+  Returns the application `constName xs`.
   It tries to fill the implicit arguments before the last element in `xs`.
 
   Remark:
   ``mkAppM `arbitrary #[α]`` returns `@arbitrary.{u} α` without synthesizing
   the implicit argument occurring after `α`.
-  Given a `x : ([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]`` returns `@Prod.fst ([Decidable p] → Bool) Nat x`.
+  Given a `x : ([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]``,
+  returns `@Prod.fst ([Decidable p] → Bool) Nat x`.
 -/
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := do
   withAppBuilderTrace constName xs do withNewMCtxDepth do
@@ -465,8 +466,9 @@ def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=
   mkAppOptM ``Pure.pure #[monad, none, none, e]
 
 /--
-  `mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
-  Remark: `fieldName` may be a subfield of `s`. -/
+`mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
+Remark: `fieldName` may be a subfield of `s`.
+-/
 partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
   let type ← inferType s
   let type ← whnf type
@@ -520,11 +522,11 @@ def mkSome (type value : Expr) : MetaM Expr := do
   let u ← getDecLevel type
   return mkApp2 (mkConst ``Option.some [u]) type value
 
-/-- Return `Decidable.decide p` -/
+/-- Returns `Decidable.decide p` -/
 def mkDecide (p : Expr) : MetaM Expr :=
   mkAppOptM ``Decidable.decide #[p, none]
 
-/-- Return a proof for `p : Prop` using `decide p` -/
+/-- Returns a proof for `p : Prop` using `decide p` -/
 def mkDecideProof (p : Expr) : MetaM Expr := do
   let decP      ← mkDecide p
   let decEqTrue ← mkEq decP (mkConst ``Bool.true)
@@ -532,63 +534,75 @@ def mkDecideProof (p : Expr) : MetaM Expr := do
   let h         ← mkExpectedTypeHint h decEqTrue
   mkAppM ``of_decide_eq_true #[h]
 
-/-- Return `a < b` -/
+/-- Returns `a < b` -/
 def mkLt (a b : Expr) : MetaM Expr :=
   mkAppM ``LT.lt #[a, b]
 
-/-- Return `a <= b` -/
+/-- Returns `a <= b` -/
 def mkLe (a b : Expr) : MetaM Expr :=
   mkAppM ``LE.le #[a, b]
 
-/-- Return `Inhabited.default α` -/
+/-- Returns `Inhabited.default α` -/
 def mkDefault (α : Expr) : MetaM Expr :=
   mkAppOptM ``Inhabited.default #[α, none]
 
-/-- Return `@Classical.ofNonempty α _` -/
+/-- Returns `@Classical.ofNonempty α _` -/
 def mkOfNonempty (α : Expr) : MetaM Expr := do
   mkAppOptM ``Classical.ofNonempty #[α, none]
 
-/-- Return `funext h` -/
+/-- Returns `funext h` -/
 def mkFunExt (h : Expr) : MetaM Expr :=
   mkAppM ``funext #[h]
 
-/-- Return `propext h` -/
+/-- Returns `propext h` -/
 def mkPropExt (h : Expr) : MetaM Expr :=
   mkAppM ``propext #[h]
 
-/-- Return `let_congr h₁ h₂` -/
+/-- Returns `let_congr h₁ h₂` -/
 def mkLetCongr (h₁ h₂ : Expr) : MetaM Expr :=
   mkAppM ``let_congr #[h₁, h₂]
 
-/-- Return `let_val_congr b h` -/
+/-- Returns `let_val_congr b h` -/
 def mkLetValCongr (b h : Expr) : MetaM Expr :=
   mkAppM ``let_val_congr #[b, h]
 
-/-- Return `let_body_congr a h` -/
+/-- Returns `let_body_congr a h` -/
 def mkLetBodyCongr (a h : Expr) : MetaM Expr :=
   mkAppM ``let_body_congr #[a, h]
 
-/-- Return `of_eq_true h` -/
+/-- Returns `@of_eq_true p h` -/
+def mkOfEqTrueCore (p : Expr) (h : Expr) : Expr :=
+  match_expr h with
+  | eq_true _ h => h
+  | _ => mkApp2 (mkConst ``of_eq_true) p h
+
+/-- Returns `of_eq_true h` -/
 def mkOfEqTrue (h : Expr) : MetaM Expr := do
   match_expr h with
   | eq_true _ h => return h
   | _ => mkAppM ``of_eq_true #[h]
 
-/-- Return `eq_true h` -/
+/-- Returns `eq_true h` -/
+def mkEqTrueCore (p : Expr) (h : Expr) : Expr :=
+  match_expr h with
+  | of_eq_true _ h => h
+  | _ => mkApp2 (mkConst ``eq_true) p h
+
+/-- Returns `eq_true h` -/
 def mkEqTrue (h : Expr) : MetaM Expr := do
   match_expr h with
   | of_eq_true _ h => return h
   | _ => return mkApp2 (mkConst ``eq_true) (← inferType h) h
 
 /--
-  Return `eq_false h`
+  Returns `eq_false h`
   `h` must have type definitionally equal to `¬ p` in the current
   reducibility setting. -/
 def mkEqFalse (h : Expr) : MetaM Expr :=
   mkAppM ``eq_false #[h]
 
 /--
-  Return `eq_false' h`
+  Returns `eq_false' h`
   `h` must have type definitionally equal to `p → False` in the current
   reducibility setting. -/
 def mkEqFalse' (h : Expr) : MetaM Expr :=
@@ -606,7 +620,7 @@ def mkImpDepCongrCtx (h₁ h₂ : Expr) : MetaM Expr :=
 def mkForallCongr (h : Expr) : MetaM Expr :=
   mkAppM ``forall_congr #[h]
 
-/-- Return instance for `[Monad m]` if there is one -/
+/-- Returns instance for `[Monad m]` if there is one -/
 def isMonad? (m : Expr) : MetaM (Option Expr) :=
   try
     let monadType ← mkAppM `Monad #[m]
@@ -617,52 +631,52 @@ def isMonad? (m : Expr) : MetaM (Option Expr) :=
   catch _ =>
     pure none
 
-/-- Return `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
+/-- Returns `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
 def mkNumeral (type : Expr) (n : Nat) : MetaM Expr := do
   let u ← getDecLevel type
   let inst ← synthInstance (mkApp2 (mkConst ``OfNat [u]) type (mkRawNatLit n))
   return mkApp3 (mkConst ``OfNat.ofNat [u]) type (mkRawNatLit n) inst
 
 /--
-  Return `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
-  This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
-  Examples of supported classes: `HAdd`, `HSub`, `HMul`.
-  We use heterogeneous operators to ensure we have a uniform representation.
-  -/
+Returns `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
+This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
+Examples of supported classes: `HAdd`, `HSub`, `HMul`.
+We use heterogeneous operators to ensure we have a uniform representation.
+-/
 private def mkBinaryOp (className : Name) (opName : Name) (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getDecLevel aType
   let inst ← synthInstance (mkApp3 (mkConst className [u, u, u]) aType aType aType)
   return mkApp6 (mkConst opName [u, u, u]) aType aType aType inst a b
 
-/-- Return `a + b` using a heterogeneous `+`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a + b` using a heterogeneous `+`. This method assumes `a` and `b` have the same type. -/
 def mkAdd (a b : Expr) : MetaM Expr := mkBinaryOp ``HAdd ``HAdd.hAdd a b
 
-/-- Return `a - b` using a heterogeneous `-`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a - b` using a heterogeneous `-`. This method assumes `a` and `b` have the same type. -/
 def mkSub (a b : Expr) : MetaM Expr := mkBinaryOp ``HSub ``HSub.hSub a b
 
-/-- Return `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type. -/
 def mkMul (a b : Expr) : MetaM Expr := mkBinaryOp ``HMul ``HMul.hMul a b
 
 /--
-  Return `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
-  This method assumes `a` and `b` have the same type.
-  Examples of supported classes: `LE` and `LT`.
-  We use heterogeneous operators to ensure we have a uniform representation.
-  -/
+Returns `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
+This method assumes `a` and `b` have the same type.
+Examples of supported classes: `LE` and `LT`.
+We use heterogeneous operators to ensure we have a uniform representation.
+-/
 private def mkBinaryRel (className : Name) (rName : Name) (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getDecLevel aType
   let inst ← synthInstance (mkApp (mkConst className [u]) aType)
   return mkApp4 (mkConst rName [u]) aType inst a b
 
-/-- Return `a ≤ b`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a ≤ b`. This method assumes `a` and `b` have the same type. -/
 def mkLE (a b : Expr) : MetaM Expr := mkBinaryRel ``LE ``LE.le a b
 
-/-- Return `a < b`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a < b`. This method assumes `a` and `b` have the same type. -/
 def mkLT (a b : Expr) : MetaM Expr := mkBinaryRel ``LT ``LT.lt a b
 
-/-- Given `h : a = b`, return a proof for `a ↔ b`. -/
+/-- Given `h : a = b`, returns a proof for `a ↔ b`. -/
 def mkIffOfEq (h : Expr) : MetaM Expr := do
   if h.isAppOfArity ``propext 3 then
     return h.appArg!
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean b/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
index e281f2b813ab..602814cbdfd6 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Offset
+import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Grind.Types
 
 namespace Lean.Meta.Grind.Arith
@@ -15,8 +16,8 @@ Helper functions for constructing proof terms in the arithmetic procedures.
 
 namespace Offset
 
-/-- `Eq.refl true` -/
-def rfl_true : Expr := mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
+/-- Returns a proof for `true = true` -/
+def rfl_true : Expr := mkConst ``Grind.rfl_true
 
 open Lean.Grind in
 /--
diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
index cca14b85ebe4..dbf0f234cbd7 100644
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -24,7 +24,7 @@ def propagateForallPropUp (e : Expr) : GoalM Unit := do
     unless (← isEqTrue p) do return
     trace_goal[grind.debug.forallPropagator] "isEqTrue, {e}"
     let h₁ ← mkEqTrueProof p
-    let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
+    let qh₁ := q.instantiate1 (mkOfEqTrueCore p h₁)
     let r ← simp qh₁
     let q := mkLambda n bi p q
     let q' := r.expr
@@ -65,7 +65,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   else
     let idx ← modifyGet fun s => (s.nextThmIdx, { s with nextThmIdx := s.nextThmIdx + 1 })
     pure <| .local ((`local).appendIndexAfter idx)
-  let proof := mkApp2 (mkConst ``of_eq_true) e proof
+  let proof := mkOfEqTrueCore e proof
   let size := (← get).newThms.size
   let gen ← getGeneration e
   -- TODO: we should have a flag for collecting all unary patterns in a local theorem
diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean
index bfe1a3d014a5..fd13a47e44f1 100644
--- a/src/Lean/Meta/Tactic/Grind/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean
@@ -126,32 +126,32 @@ builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
   else if (← isEqTrue b) then
     pushEq e a <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b)
   else if (← isEqv a b) then
-    pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkEqProof a b)
+    pushEqTrue e <| mkEqTrueCore e (← mkEqProof a b)
 
 /-- Propagates `Eq` downwards -/
 builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
   if (← isEqTrue e) then
     let_expr Eq _ a b := e | return ()
-    pushEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+    pushEq a b <| mkOfEqTrueCore e (← mkEqTrueProof e)
 
 /-- Propagates `EqMatch` downwards -/
 builtin_grind_propagator propagateEqMatchDown ↓Grind.EqMatch := fun e => do
   if (← isEqTrue e) then
     let_expr Grind.EqMatch _ a b origin := e | return ()
     markCaseSplitAsResolved origin
-    pushEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+    pushEq a b <| mkOfEqTrueCore e (← mkEqTrueProof e)
 
 /-- Propagates `HEq` downwards -/
 builtin_grind_propagator propagateHEqDown ↓HEq := fun e => do
   if (← isEqTrue e) then
     let_expr HEq _ a _ b := e | return ()
-    pushHEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+    pushHEq a b <| mkOfEqTrueCore e (← mkEqTrueProof e)
 
 /-- Propagates `HEq` upwards -/
 builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
   let_expr HEq _ a _ b := e | return ()
   if (← isEqv a b) then
-    pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkHEqProof a b)
+    pushEqTrue e <| mkEqTrueCore e (← mkHEqProof a b)
 
 /-- Propagates `ite` upwards -/
 builtin_grind_propagator propagateIte ↑ite := fun e => do
@@ -166,7 +166,7 @@ builtin_grind_propagator propagateDIte ↑dite := fun e => do
   let_expr f@dite α c h a b := e | return ()
   if (← isEqTrue c) then
      let h₁ ← mkEqTrueProof c
-     let ah₁ := mkApp a (mkApp2 (mkConst ``of_eq_true) c h₁)
+     let ah₁ := mkApp a (mkOfEqTrueCore c h₁)
      let p ← simp ah₁
      let r := p.expr
      let h₂ ← p.getProof
diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
index 3937644300a7..15a232bdeb1e 100644
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -145,7 +145,7 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
       return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)
     else
       return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b (← mkEqFalseProof c)
-  | _ => return mkApp2 (mkConst ``of_eq_true) c (← mkEqTrueProof c)
+  | _ => return mkOfEqTrueCore c (← mkEqTrueProof c)
 
 /-- Introduces new hypotheses in each goal. -/
 private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat) : GrindM (List Goal) := do
diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean
index cbad141607c1..cb41c2c76242 100644
--- a/tests/lean/run/grind_offset_cnstr.lean
+++ b/tests/lean/run/grind_offset_cnstr.lean
@@ -255,3 +255,23 @@ example (a b c : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by
   grind
 example (a b c : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by
   grind
+
+theorem ex1 (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 := by
+  grind
+
+/--
+info: theorem ex1 : ∀ {a4 : Nat} (p : Prop) (a1 a2 a3 : Nat),
+  (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 :=
+fun {a4} p a1 a2 a3 =>
+  intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4) (iff_eq p (a2 ≤ a1))
+    fun a a_1 a_2 =>
+    intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun a_3 =>
+      Classical.byContradiction
+        (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun x =>
+          Nat.unsat_lo_lo a4 a1 1 7 rfl_true x
+            (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm a) (eq_false a_1)))
+              (Nat.lo_lo a2 a3 a4 3 3 a_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm a_3) (eq_false a_1))))))
+-/
+#guard_msgs (info) in
+open Lean Grind in
+#print ex1
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 21e4360b9de6..833f163786ef 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -9,10 +9,8 @@ case grind.1.2
 a b c : Bool
 p q : Prop
 left✝ : a = true
-right✝ : b = true ∨ c = true
 left : p
 right : q
-x✝ : b = false ∨ a = false
 h✝ : b = false
 h : c = true
 ⊢ False
@@ -94,7 +92,6 @@ h₁ : HEq p a
 h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
-right : ¬r ∨ p
 h : ¬r
 ⊢ False
 
@@ -106,7 +103,6 @@ h₁ : HEq p a
 h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
-right : ¬r ∨ p
 h : p
 ⊢ False
 -/