α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
have : ((⟨x, Or.inl hx⟩ : (s ∪ sᶜ : Set α)) : α) ∈ s := hx
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Trans.trans (Trans.trans (Set.union (_ : s ∩ sᶜ ⊆ ∅)).symm (Set.ofEq (_ : s ∪ sᶜ = univ))) (Set.univ α)).symm x =
    Sum.inl { val := x, property := hx }
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
rw [Equiv.Set.sumCompl]
no goals
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Trans.trans (Trans.trans (Set.union (_ : s ∩ sᶜ ⊆ ∅)).symm (Set.ofEq (_ : s ∪ sᶜ = univ))) (Set.univ α)).symm x =
    Sum.inl { val := x, property := hx }
simpa using Set.union_apply_left (by simp) this
no goals
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ s ∩ sᶜ ⊆ ∅
simp