α : Type u_1
l : List α
this : DecidableEq α
⊢ revzip (powersetAux l) ~ revzip (powersetAux' l)
α : Type u_1
l : List α
⊢ revzip (powersetAux l) ~ revzip (powersetAux' l)
haveI := Classical.decEq α
α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l - x)) (powersetAux l) ~ List.map (fun x => (x, ↑l - x)) (powersetAux' l)
α : Type u_1
l : List α
this : DecidableEq α
⊢ revzip (powersetAux l) ~ revzip (powersetAux' l)
rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']
no goals
α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l - x)) (powersetAux l) ~ List.map (fun x => (x, ↑l - x)) (powersetAux' l)
exact powersetAux_perm_powersetAux'.map _