possible bug of `guard_hyp`

Stream: general

[Asei Inoue]

def Set (α : Type) := α → Prop

def Set.inter {α : Type} (s t : Set α) : Set α := fun x => s x ∧ t x

instance (α : Type) : Inter (Set α) where
  inter := Set.inter

variable {α : Type} (s u : Set α)

example (h : s ∩ u = u ∩ s): True := by
  dsimp [Inter.inter] at h
  guard_hyp h : s.inter u = u.inter s
  sorry

example (h : s ∩ u = u ∩ s): True := by
  unfold Inter.inter at h

  /-
  hypothesis h has type
    (instInterSet α).1 s u = (instInterSet α).1 u s
  not
    s ∩ u = u ∩ s
  -/
  guard_hyp h : (instInterSet α).1 s u = (instInterSet α).1 u s
  sorry

[Asei Inoue]

I think this is a bug of guard_hyp.

[Eric Wieser]

I'm very confused about what (instInterSet α).1 means in the goal view here, and how it is different from @Inter.inter _ (instInterSet α)

[Asei Inoue]

@Eric Wieser sorry, I dont understand what do you mean. This is not a bug?

[Daniel Weber]

Setting set_option pp.all true the unfold changes
@Eq.{1} (Set α) (@Inter.inter.{0} (Set α) (instInterSet α) s u) (@Inter.inter.{0} (Set α) (instInterSet α) u s) to
@Eq.{1} (Set α) ((instInterSet α).1 s u) ((instInterSet α).1 u s) while the dsimp changes it to
@Eq.{1} (Set α) (@Set.inter α s u) (@Set.inter α u s)

[Eric Wieser]

I don't understand what the (instInterSet α).1 is in that second state, and the infotree hovers don't tell me anything about .1

[Daniel Weber]

It's the same as (instInterSet α).inter, I believe

[Eric Wieser]

But something about it is not the same, otherwise the goal view wouldn't have changed

[Daniel Weber]

guard_hyp h : (_ : Set α → Set α → Set α) s u = (_ : Set α → Set α → Set α) u s this works, but I'm really not sure what it's filling the metavariables with