grind reports type error constructing proof

Stream: lean4

[Bhavik Mehta]

Here's my example, which does use mathlib:

import Mathlib

open Finset

example {a b c d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) :
    Ico (a, b) (a, d) ⊆ Icc (a, b) (c, d) := by
  grind

The issue reported in the grind diagnostic is

 [issue] type error constructing proof for Set.subset_def
      when assigning metavariable ?s with
        Ico (a, b) (a, d)
      has type
        Finset (ℕ × ℕ)
      but is expected to have type
        Set ?α

[Robin Arnez]

I don't think this is really a problem here; it still uses Finset.subset_iff. Really, it's just missing a few lemmas about Ico, Icc and <= and < on Prod:

import Mathlib

open Finset

example {a b c d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) :
    Ico (a, b) (a, d) ⊆ Icc (a, b) (c, d) := by
  grind [Finset.mem_Ico, Finset.mem_Icc, Prod.le_def, Prod.lt_iff]

[Bhavik Mehta]

Hmm okay, I think it's a confusing diagnostic response from grind in that case!