case refl
α : Type u_1
inst✝ : Preorder α
⊢ empty ↑∅ = true
α : Type u_1
inst✝ : Preorder α
s : Ordset α
h : s = ∅
⊢ empty ↑s = true
cases h
no goals
case refl
α : Type u_1
inst✝ : Preorder α
⊢ empty ↑∅ = true
exact rfl
no goals
α : Type u_1
inst✝ : Preorder α
s : Ordset α
h : empty ↑s = true
⊢ s = ∅
cases s with | mk s_val _ => cases s_val <;> [rfl; cases h]
no goals
case mk
α : Type u_1
inst✝ : Preorder α
s_val : Ordnode α
property✝ : Valid s_val
h : empty ↑{ val := s_val, property := property✝ } = true
⊢ { val := s_val, property := property✝ } = ∅
cases s_val <;> [rfl; cases h]