Theorem: Std.RBSet.isEmpty_iff_eq_empty (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
t : RBSet α cmp
⊢ isEmpty t = true ↔ t = ∅
Tactic:
obtain ⟨⟨⟩, _⟩ := t <;>
simp [isEmpty]
State after:
case mk.nil
α : Type u_1
cmp : α → α → Ordering
property✝ : RBNode.WF cmp RBNode.nil
⊢ { val := RBNode.nil, property := property✝ } = ∅

case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ ¬{ val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } = ∅

State before:
case mk.nil
α : Type u_1
cmp : α → α → Ordering
property✝ : RBNode.WF cmp RBNode.nil
⊢ { val := RBNode.nil, property := property✝ } = ∅
Tactic:
rfl
State after:
no goals

State before:
case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ ¬{ val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } = ∅
Tactic:
change _ ≠ Subtype.mk _ _
State after:
case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ { val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } ≠ { val := RBNode.nil, property := ⋯ }

State before:
case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ { val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } ≠ { val := RBNode.nil, property := ⋯ }
Tactic:
simp
State after:
no goals