missing cases produces suggestions which fail

Stream: lean4

[Bhavik Mehta]

This came up in LftCM:

import Std

@[ext]
structure MyType : Type where
  fst : Nat
  snd : Nat

theorem MyType.le_of_rel : ∀ {a b : MyType},
  (a.1 ≤ b.1 ∧ a.2 = b.2) ∨ (0 < a.2 ∧ a.2 ≤ b.2) ∨ (0 < a.2 ∧ b.2 = 0) → a = b
| (mk _ _), (mk _ _), (Or.inr (Or.inr (And.intro _ (Eq.refl _)))) => _

tells me (correctly) there are two cases missing:

(mk _ _), (mk _ _), (@Or.inr (@Or.inl (@And.intro _ _)))
(mk _ _), (mk _ _), (@Or.inl (@And.intro _ Eq.refl))

The first of these doesn't work because there are too many @ signs printed here. The second also has this problem, but fixing the @ signs produces another problem, that Eq.refl wants an explicit argument. Fixing this produces a third problem, saying that dependent elimination failed:

dependent elimination failed, type mismatch when solving alternative with type
  motive { fst := fst✝¹, snd := snd✝ } { fst := fst✝¹, snd := snd✝ }
    (_ :
      { fst := fst✝¹, snd := snd✝ }.fst ≤ { fst := fst✝¹, snd := snd✝ }.fst ∧
          { fst := fst✝¹, snd := snd✝ }.snd = { fst := fst✝¹, snd := snd✝ }.snd ∨
        0 < { fst := fst✝¹, snd := snd✝ }.snd ∧ { fst := fst✝¹, snd := snd✝ }.snd ≤ { fst := fst✝¹, snd := snd✝ }.snd ∨
          0 < { fst := fst✝¹, snd := snd✝ }.snd ∧ { fst := fst✝¹, snd := snd✝ }.snd = 0)
but expected
  motive { fst := fst✝¹, snd := snd✝ } { fst := fst✝, snd := snd✝ }
    (_ :
      { fst := fst✝¹, snd := snd✝ }.fst ≤ { fst := fst✝, snd := snd✝ }.fst ∧
          { fst := fst✝¹, snd := snd✝ }.snd = { fst := fst✝, snd := snd✝ }.snd ∨
        0 < { fst := fst✝¹, snd := snd✝ }.snd ∧ { fst := fst✝¹, snd := snd✝ }.snd ≤ { fst := fst✝, snd := snd✝ }.snd ∨
          0 < { fst := fst✝¹, snd := snd✝ }.snd ∧ { fst := fst✝, snd := snd✝ }.snd = 0)

[Bhavik Mehta]

To be clear, I'm expecting to be able to induct on Eq.refl here, and I expected the suggestions for missing cases to be valid things to put in the match (note this latter property is true in lean 3)