diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean
index 09406b80f624..cda31733b773 100644
--- a/src/Init/Data/Array/Mem.lean
+++ b/src/Init/Data/Array/Mem.lean
@@ -38,8 +38,8 @@ macro "array_get_dec" : tactic =>
     -- subsumed by simp
     -- | with_reducible apply sizeOf_get
     -- | with_reducible apply sizeOf_getElem
-    | (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
-    | (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
+    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp_arith
+    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp_arith
     )
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
@@ -52,7 +52,7 @@ macro "array_mem_dec" : tactic =>
   `(tactic| first
     | with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
     | with_reducible
-        apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
+        apply Nat.lt_of_lt_of_le (Array.sizeOf_lt_of_mem ?h)
         case' h => assumption
       simp_arith)
 
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index 307b4d421696..e37af41afeb3 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -192,7 +192,7 @@ macro "sizeOf_list_dec" : tactic =>
   `(tactic| first
     | with_reducible apply sizeOf_lt_of_mem; assumption; done
     | with_reducible
-        apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+        apply Nat.lt_of_lt_of_le (sizeOf_lt_of_mem ?h)
         case' h => assumption
       simp_arith)
 
diff --git a/tests/lean/run/issue5027.lean b/tests/lean/run/issue5027.lean
new file mode 100644
index 000000000000..6355fe37631c
--- /dev/null
+++ b/tests/lean/run/issue5027.lean
@@ -0,0 +1,16 @@
+inductive Term (α: Type): Type where
+  | Composite : Array (Term α) → Term α
+  | Atom: α → Term α
+
+-- height of a term
+def height (f: Term α): Nat :=
+  let rec max_height (a: Array (Term α)) (i: Nat) (m: Nat): Nat :=
+    if h: i < a.size then
+      -- The recusive call to height used to fail because of a too weak
+      -- array_get_dec
+      max_height a (i + 1) (max (height a[i]) m)
+    else
+      m
+  match f with
+  | .Composite a => 1 + max_height a 0 0
+  | .Atom _ => 1