case mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ sᶜ
⊢ ↑(Set.sumCompl s).symm ↑{ val := x, property := hx } = Sum.inr { val := x, property := hx }
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : ↑(sᶜ)
⊢ ↑(Set.sumCompl s).symm ↑x = Sum.inr x
cases' x with x hx
no goals
case mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ sᶜ
⊢ ↑(Set.sumCompl s).symm ↑{ val := x, property := hx } = Sum.inr { val := x, property := hx }
exact Set.sumCompl_symm_apply_of_not_mem hx