Subset of an empty set is empty

Stream: new members

[Yagub Aliyev]

How to show that a subset of an empty set is empty in Lean? This is my incomplete attempt:

https://adam.math.hhu.de/#/g/hhu-adam/robo/world/SetTheory/level/4

theorem Set.subset_empty_iff {A : Type _} (s : Set A) : s ⊆ ∅ ↔ s = ∅ := by
constructor
rw[imp_iff_not_or]
by_cases h : s = ∅
right
exact h
left
by_contra
have h0 : s=∅ := a

[Ruben Van de Velde]

Looking at the available lemmas, Set.Subset.antisymm looks interesting.

[Ruben Van de Velde]

Incidentally, this seems to be what the game suggests itself