How does ` exact xntu (Or.inl xt)` work?

Stream: lean4

[Hallon]

example : s \ (t ∪ u) ⊆ (s \ t) \ u := by
  rintro x ⟨xs, xntu⟩
  -- xs: x ∈ s
  -- xntu: x ∉ t ∪ u
  constructor
  · show x ∈ s \ t
    use xs
    intro xt
    -- xt: x ∈ t
    -- goal: False
    exact xntu (Or.inl xt)
  · show x ∉ u
    intro xu
    apply xntu (Or.inr xu)

Could anybody teach me that how exact xntu (Or.inl xt) works?

[Hallon]

Contradiction between xntu and xt is clear, but why write Or.inr xt?

[Ruben Van de Velde]

import Mathlib

variable {s t u : Set α}

example : s \ (t ∪ u) ⊆ (s \ t) \ u := by
  rintro x ⟨xs, xntu⟩
  -- xs: x ∈ s
  -- xntu: x ∉ t ∪ u
  constructor
  · show x ∈ s \ t
    use xs
    intro xt
    -- xt: x ∈ t
    -- goal: False
    apply xntu
    -- goal: x ∈ t ∪ u
    rw [Set.mem_union] -- this happens to be true by definition, so lean will accept the proof without this line
    -- goal: x ∈ t ∨ x ∈ u
    apply Or.inl -- or use tactic `left`
    -- goal: x ∈ t
    exact xt
  · show x ∉ u
    intro xu
    apply xntu (Or.inr xu)

Does this help?

[Hallon]

OK, thanks very much. :kiss_with_blush:

[Kevin Buzzard]

The other important thing is that Set.mem_union is proved with rfl, which means that the definition of the union symbol is the output of the rewrite, so you can skip it if you're just making the term directly.

[Hallon]

OK~

[Kyle Miller]

I just generated an informal version of your first proof, in case seeing how it could be explained in english is illuminating.

image.png

In particular, exact xntu (Or.inl xt) gets turned into two claims, with the first claim explaining how xntu could be regarded as being something implying false.

[Hallon]

wow, it's very detailed. Thanks very much.

[Kevin Buzzard]

A computer wrote this, not Kyle! Although Kyle was involved in writing the program which wrote the text in the image :-)