What's the meaninig of * in lean?

Stream: new members

[Michael Novak]

I think, I learned about it previousely, but I forgot - what's the meaning of * in lean? For example in the following:

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

[Damiano Testa]

It means every hypothesis in context, including the goal.

[Michael Novak]

Thank you very much!

[Damiano Testa]

Note also that, even with tactics that fail when they do not modify something, the expectation with * is that they should fail if they do not modify all hypotheses.

[Damiano Testa]

In your example, * covers also s t u, simp does nothing on them, but the tactic succeeds, since it could do something on h and on the goal.

[Michael Novak]

I'm not sure I understand. When using *, will a tactic fail or not, if it could only modify some of the hypotheses in the context? It seems like your last two comments contradict each other, but I probably misunderstood.

[Damiano Testa]

Ok, I should have said "they modify some hypothesis" instead of "they do not modify all hypotheses"! :upside_down:

[Damiano Testa]

In your example, even though simp would fail on s, the tactic simp ... at * succeeds, since it modified h and the goal.

[Michael Novak]

O.k, I think I understand now. Thank you very much!