Failed to input the tactics step-by-step within a case block

First thanks for such excellent tools!

I'm testing repl to see if I can enter the tactics one-by-one so that I can get state information within each step. When I was testing the following simple problem, I met the problem on case analysis.

open Real
example (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + rexp c + e < b + rexp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
    apply exp_lt_exp.mpr h₁
  apply le_refl

Here is the input/output from my terminal

> lake exe repl 
{"cmd": "import Mathlib\nopen Real\nexample (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + rexp c + e < b + rexp d + e := by sorry"}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 3, "column": 90},
   "goal":
   "a b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ a + rexp c + e < b + rexp d + e",
   "endPos": {"line": 3, "column": 95}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 7},
   "data": "declaration uses 'sorry'"}],
 "env": 0}

{"tactic": "apply add_lt_add_of_lt_of_le", "proofState": 0}

{"proofState": 1,
 "goals":
 ["case h₁\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ a + rexp c < b + rexp d",
  "case h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"]}

{"tactic": "·apply add_lt_add_of_le_of_lt h₀", "proofState": 1}

{"proofState": 2,
 "messages":
 [{"severity": "error",
   "pos": {"line": 0, "column": 0},
   "endPos": {"line": 0, "column": 0},
   "data":
   "unsolved goals\ncase h₁\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ rexp c < rexp d"}],
 "goals": ["case h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"]}

{"tactic": "  apply exp_lt_exp.mpr h₁", "proofState": 2}

{"message":
 "tactic 'apply' failed, failed to unify\n  rexp c < rexp d\nwith\n  e ≤ e\ncase h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"}

The problem occurred after I entered the second tactic {"tactic": " apply exp_lt_exp.mpr h₁", "proofState": 2} from the case block. However, if I entered the two tactics from the case block within one command, normal state information will be returned.

{"tactic": "· apply add_lt_add_of_le_of_lt h₀\n  apply exp_lt_exp.mpr h₁", "proofState": 1}

{"proofState": 3,
 "goals": ["case h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"]}

I guess repl just ignores the two whitespaces before the second tactic within the case block when I enter them separately, because I tried to remove the two leading whitespaces in the interactive mode using vscode, and got the same error message

open Real
example (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + rexp c + e < b + rexp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
  apply exp_lt_exp.mpr h₁

tactic 'apply' failed, failed to unify
  rexp c < rexp d
with
  e ≤ e

So I wonder if it's possible to handle this issue? Thanks!

Start by reproducing the case-block sequence with lake exe repl, using the reported apply add_lt_add_of_lt_of_le and separate tactic commands. Trace how the REPL selects the next goal after the first tactic; done means entering the second tactic separately targets the remaining rexp c < rexp d goal instead of e ≤ e.