What's the meaning of this underscore _ in last line?

Stream: lean4

[Hallon]

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
simp only [subset_def, mem_inter_iff] at *
-- h: ∀ x ∈ s, x ∈ t
-- ∀ (x : α), x ∈ s ∧ x ∈ u → x ∈ t ∧ x ∈ u
rintro x ⟨xs, xu⟩
exact ⟨h _ xs, xu⟩

[Hallon]

Similar to this hypothesis h, I need x \in t by x \in s. Sometimes directly write h xs, sometimes need to underline h _ xs, how to distinguish between adding underline or not?

[Hallon]

Is anybody here? Help!!! :pleading_face:

[Hallon]

This is the example which dont need underscore:

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

[Sébastien Gouëzel]

It means "Hey, Lean, could you please fill this out for me by putting the only thing that makes sense here". In this case, it is x, and Lean can guess it because it's mentioned in xs.

[Sébastien Gouëzel]

Whether you need it or not depends on whether it is declared as an implicit or explicit argument in the theorem you're applying. If you go to the definition of subset, you will see that the point is implicit, as it is written in curly braces {x : α}.

[Sébastien Gouëzel]

When you declare a theorem

theorem foo (a : A) (b : B) {c : C} (d : D) : ...

arguments between parentheses (called explicit arguments) will need to be provided when applying the theorem, while you expect that arguments between curly braces (called implicit arguments) should be guessed by Lean.

[Hallon]

Uh-huh