Why fun x works for ⊆ but not ∀ {x}

Stream: new members

[Michał Pacholski]

I'm trying to understand why does Lean accept this proof term

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u :=
  fun x ⟨xs, xu⟩ ↦ ⟨h xs, xu⟩

Whereas both of the following fail

example (h : ∀ {x : α}, x ∈ s → x ∈ t) : ∀ {x : α}, x ∈ s ∩ u → x ∈ t ∩ u :=
  fun x ⟨xs, xu⟩ ↦ ⟨h {x} xs, xu⟩
-- type mismatch
--  fun x x_1 ↦ ?m.1714
-- has type
--   (x : x✝ ∈ s ∩ u) → (x_1 : ?m.1715 x) → ?m.1716 x x_1 : Sort (imax ?u.1709 ?u.1712)
-- but is expected to have type
--   x✝ ∈ s ∩ u → x✝ ∈ t ∩ u : Prop
-- the following variables have been introduced by the implicit lambda feature
--   x✝ : α
-- you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.

example (h : ∀ x : α, x ∈ s → x ∈ t) : ∀ x : α, x ∈ s ∩ u → x ∈ t ∩ u :=
  fun x ⟨xs, xu⟩ ↦ ⟨h xs, xu⟩
-- Application type mismatch: In the application
--   h xs
-- the argument
--   xs
-- has type
--   x ∈ s : Prop
-- but is expected to have type
--   α : Type u_1

I understand both of the errors: in the first case I should have written fun {x} ... and in the second ⟨h x xs, xu⟩. But then why is the first example correct? Shouldn't it be flagged with the same error as one of the failing examples?

Btw, I took this example from course "mathematics in lean", chapter: Sets and Functions.

[Ruben Van de Velde]

Because docs#Set.Subset uses ⦃a⦄

[Ruben Van de Velde]

That's a binder between {} and ()

[Ruben Van de Velde]

If you had included variables and imports, I could have verified that worked

[Kevin Buzzard]

import Mathlib.Tactic

variable (s t u : Set ℕ)

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  unfold Subset Set.instHasSubset at h
  unfold LE.le Set.instLE Set.Subset at h
  dsimp only at h
  -- h : ∀ ⦃a : ℕ⦄, a ∈ s → a ∈ t
  exact fun x ⟨xs, xu⟩ ↦ ⟨h xs, xu⟩

It seems that ⊆ unfolds to ∀ ⦃a : ℕ⦄, a ∈ s → a ∈ t rather than ∀ {a : ℕ}, a ∈ s → a ∈ t which presumably explains the difference.

[Michał Pacholski]

Thank you! I didn't know about ⦃a⦄ binder. I'm also amazed with how helpful this community is: not only did I get the answer to my question, but I also learned how I could have found it out myself. I couldn't have asked for more.

[Michał Pacholski]

Ruben Van de Velde said:

If you had included variables and imports, I could have verified that worked

I'll remember to do it next time!

[Kevin Buzzard]

NB to see exactly what to unfold in the above, it's sometimes helpful to set_option pp.notation false. I didn't do this but only because I've been around long enough to know the names of the declarations underlying of a lot of the common notation.

[Ruben Van de Velde]

For what it's worth, I used loogle to find where to look: https://loogle.lean-lang.org/?q=HasSubset+%28Set+_%29

[Kyle Miller]

A helpful exploratory tactic, to deal with typeclass-defined notation, is unfold_projs:

import Mathlib.Tactic

variable (s t u : Set ℕ)

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  unfold_projs
  -- ⊢ (s.inter u).Subset (t.inter u)
  -- Now we know it's `Set.Subset`.
  unfold Set.Subset
  -- ⊢ ∀ ⦃a : ℕ⦄, a ∈ s.inter u → a ∈ t.inter u

[Kyle Miller]

In the newest Lean version, if you right click on ⊆ and select "go to definition" in VS Code, it brings you to the HasSubset instance in Mathlib.Data.Set.Defs, and just a handful of lines before that you can see Set.Subset. There's still a little indirection here, but it's a lot nicer than a couple versions ago where it would only bring you to HasSubset itself.