no goals
α : Type u_1
β : Type ?u.39948
γ : Type ?u.39951
ι : Sort ?u.39954
ι' : Sort ?u.39957
f : α → β
s t : Set α
inst✝ : BooleanAlgebra α
S : Set α
⊢ compl '' (compl '' S) = S
rw [← image_comp, compl_comp_compl, image_id]