case h.e'_3
α : Type u_1
β : Type ?u.1021
γ : Type ?u.1024
ι : Sort ?u.1027
κ : ι → Sort ?u.1032
inst✝¹ : LE α
inst✝ : LE β
s t : Set α
h : IsUpperSet (sᶜ)
⊢ s = sᶜᶜ
α : Type u_1
β : Type ?u.1021
γ : Type ?u.1024
ι : Sort ?u.1027
κ : ι → Sort ?u.1032
inst✝¹ : LE α
inst✝ : LE β
s t : Set α
h : IsUpperSet (sᶜ)
⊢ IsLowerSet s
convert h.compl
no goals
case h.e'_3
α : Type u_1
β : Type ?u.1021
γ : Type ?u.1024
ι : Sort ?u.1027
κ : ι → Sort ?u.1032
inst✝¹ : LE α
inst✝ : LE β
s t : Set α
h : IsUpperSet (sᶜ)
⊢ s = sᶜᶜ
rw [compl_compl]