Theorem: Set.eq_empty_of_subset_empty (GMLInit/Data/Set/Subset.lean)

State before:
α : Sort u_1
s t u : Set α
⊢ s.Subset Set.empty → s = Set.empty
Tactic:
intro hs
State after:
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s = Set.empty

State before:
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s = Set.empty
Tactic:
antisymmetry using (.⊆.)
State after:
case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s.Subset Set.empty

case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ Set.empty.Subset s

State before:
case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s.Subset Set.empty
Tactic:
exact hs
State after:
no goals

State before:
case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ Set.empty.Subset s
Tactic:
exact empty_subset s
State after:
no goals