implicit arguments in `Set.mem_of_subset_of_mem`

Stream: mathlib4

[Paige Thomas]

When I use show_term apply Set.mem_of_subset_of_mem a1 a2, I get exact Set.mem_of_subset_of_mem a1 a2, but when I use that, I get

application type mismatch
  Set.mem_of_subset_of_mem a1
argument
  a1
has type
  x :: visited ⊆ dfs_aux g (nexts g x ++ stack) (x :: visited) : Prop
but is expected to have type
  ?m.66788 ⊆ List.Mem x : Prop

application type mismatch
  Set.mem_of_subset_of_mem ?m.66892 a2
argument
  a2
has type
  x ∈ x :: visited : Prop
but is expected to have type
  dfs_aux g (nexts g x ++ stack) (x :: visited) ∈ ?m.66788 : Prop

Is this because the {s₁ : Set α} {s₂ : Set α} {a : α} in the theorem are implicit?

[Lucas Allen]

For types that aren't metavariables the expression need to match exactly. In the first error the problem is that the expression dfs_aux g (nexts g x ++ stack) (x :: visited) isn't exactly List.Mem x. And for the second error the problem is that x isn't exactly dfs_aux g (nexts g x ++ stack) (x :: visited).

You could try using apply Set.mem_of_subset_of_mem and see what that gives.

[Paige Thomas]

Thank you.