possible bug revealed by failure to apply simple rel, warning/error is confusing

[rzeta0]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following is an MWE reproducing an issue I found working on a wider exercise.

import Mathlib.Tactic

example {n: ℕ} (h: 5 ≤ n): 2^n ≥ 30 := by
  calc
    2^n ≥ 2^5 := by rel [h] -- < -- fails ---
    _ ≥ 30 := by norm_num

The rel [h] fails.

The error message is confusing:

rel failed, cannot prove goal by 'substituting' the listed relationships. The steps which could not be automatically justified were:
1 ≤ 2

The code and error message have been verified on the online environment:
https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0AVJAYxmEICgyBTADyXHUrgG8A7ALjkFRCAXzgApUHAKxxAJkRwWASg4AmAHos4gUyI4AZgAMcNgF44WAJ5k4cQknTljx+YpXyROvfrhRK6OAG1UAXTgBaX3AAPH4BAGZIwOgAziG+RpYA+spqmg4GEtAgCSwAriBkQA

Context

The issue was mentioned on the lean zulipchat and it was recommended a bug report was raised (forgive me if I misunderstood that bit)

https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/can't.20apply.20simple.20inequality.20by.20.60rel.60

Steps to Reproduce

1. use the MWE above
2. or use the linked example on the online environment

Expected behavior: [Clear and concise description of what you expect to happen]

It is expected that the rel [h] succeeds with no error or warning.

There may be some discussion about (0.5)^n ≥ (0.5)^5 but the MWE above only uses natural numbers, not reals or irrationals, not even integers.

Actual behavior: [Clear and concise description of what actually happens]

The rel [h] fails.

The error message is confusing:

rel failed, cannot prove goal by 'substituting' the listed relationships. The steps which could not be automatically justified were:
1 ≤ 2

Additional

Adding an explicit hypothesis g: 1 ≤ 2 in response to the error message is also fails.
Even if it worked, this should not be considered a satisfactory solution.

import Mathlib.Tactic

example {n: ℕ} (h: 5 ≤ n): 2^n ≥ 30 := by
  have g: 1 ≤ 2 := by norm_num -- < -- shouldn't ne necessary, still fails
  calc
    2^n ≥ 2^5 := by rel [h] -- < -- fails ---
    _ ≥ 30 := by norm_num

Versions

using macOS 15.2 VSC 1.96.2 the lean version is "4.3.0"
using live.lean-lang.org "4.15.0-rc1"