why does `grind` fail here?

Stream: general

[Asei Inoue]

/-- Redefining the weak (non-strict) order relation on natural numbers -/
protected inductive Nat.myle (n : Nat) : Nat → Prop
  /-- `∀ n, n ≤ n` -/
  | refl : Nat.myle n n
  /-- If `n ≤ m`, then `n ≤ m + 1` -/
  | step {m : Nat} : Nat.myle n m → Nat.myle n (m + 1)

/-- Replace the standard `≤` with `myle` -/
instance : LE Nat where
  le := Nat.myle

attribute [grind =>] Nat.myle.refl Nat.myle.step

/-- Reflexivity -/
@[grind =>, refl]
theorem Nat.myle_refl (n : Nat) : n ≤ n := by
  exact Nat.myle.refl

-- Let m, n, and k be terms of Nat
variable {m n k : Nat}

@[grind =>]
theorem Nat.myle_step (h : n ≤ m) : n ≤ m + 1 := by
  apply Nat.myle.step h

/-- Transitivity -/
theorem Nat.myle_trans (hnm : n ≤ m) (hmk : m ≤ k) : n ≤ k := by
  induction hmk with
  | refl =>
    fail_if_success grind -- Why does `grind` fail here?
    assumption
  | @step k hmk ih =>
    fail_if_success grind -- Why does `grind` fail here?
    exact Nat.myle_step ih

[Notification Bot]

Asei Inoue has marked this topic as resolved.

[Asei Inoue]

grind is confused by two distinct LE implementations

[Notification Bot]

Isak Colboubrani has marked this topic as unresolved.