α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ revzip (powersetAux l₁) ~ revzip (powersetAux l₂)
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ revzip (powersetAux l₁) ~ revzip (powersetAux l₂)
haveI := Classical.decEq α
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₁) ~ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₂)
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ revzip (powersetAux l₁) ~ revzip (powersetAux l₂)
simp [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]
no goals
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₁) ~ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₂)
exact (powersetAux_perm p).map _