Set Theory Game - Family Intersections 6

Stream: new members

[Sam Middleton]

Hi! I'm Sam, and I've been enjoying several of the games at https://adam.math.hhu.de/, but I've gotten stuck on level 6 of Family Intersection World in the Set Theory Game.
I've reached a point where I have assumptions hA: x ∉ A & hs: x ∈ A ∪ s and the goal x ∈ s.
Is there a more elegant way to finish than:

rcases hs
apply hA at h
by_contra hFoo -- an arbitrary assumption left over from earlier
exact h
exact h

[Philippe Duchon]

Instead of by_contra hFoo; exact h, you could use contradiction (h and hA are in direct contradiction), or exfalso; apply hA; exact h (does the same thing, really, but does not depend on some arbitrary assumption). (I'm not sure which options the Set Theory Game leaves open though)

[Ruben Van de Velde]

In mathlib, there's a lemma for that (Or.resolve_left, I think), but I think what you wrote is fine for the game