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

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

State before:
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
⊢ s = t
Tactic:
apply Set.ext
State after:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
⊢ ∀ (x : α), x ∈ s ↔ x ∈ t

State before:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
⊢ ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic:
intro x
State after:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s ↔ x ∈ t

State before:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s ↔ x ∈ t
Tactic:
constructor
State after:
case a.mp
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s → x ∈ t

case a.mpr
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ t → x ∈ s

State before:
case a.mp
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s → x ∈ t
Tactic:
exact hst x
State after:
no goals

State before:
case a.mpr
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ t → x ∈ s
Tactic:
exact hts x
State after:
no goals