[GOAL]
α : Type u_1
l : List α
s : Multiset α
⊢ ∀ (a : List α), Quotient.mk (isSetoid α) a ∈ powersetAux l ↔ Quotient.mk (isSetoid α) a ≤ ↑l
[PROOFSTEP]
simp [powersetAux_eq_map_coe, Subperm, and_comm]
[GOAL]
α : Type u_1
l : List α
⊢ powersetAux l ~ powersetAux' l
[PROOFSTEP]
rw [powersetAux_eq_map_coe]
[GOAL]
α : Type u_1
l : List α
⊢ List.map ofList (sublists l) ~ powersetAux' l
[PROOFSTEP]
exact (sublists_perm_sublists' _).map _
[GOAL]
α : Type u_1
a : α
l : List α
⊢ powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)
[PROOFSTEP]
simp [powersetAux']
[GOAL]
α : Type u_1
a : α
l : List α
⊢ List.map (ofList ∘ List.cons a) (sublists' l) = List.map (cons a ∘ ofList) (sublists' l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetAux' l₁ ~ powersetAux' l₂
[PROOFSTEP]
induction' p with a l₁ l₂ p IH a b l l₁ l₂ l₃ _ _ IH₁ IH₂
[GOAL]
case nil
α : Type u_1
l₁ l₂ : List α
⊢ powersetAux' [] ~ powersetAux' []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : powersetAux' l₁ ~ powersetAux' l₂
⊢ powersetAux' (a :: l₁) ~ powersetAux' (a :: l₂)
[PROOFSTEP]
simp only [powersetAux'_cons]
[GOAL]
case cons
α : Type u_1
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : powersetAux' l₁ ~ powersetAux' l₂
⊢ powersetAux' l₁ ++ List.map (cons a) (powersetAux' l₁) ~ powersetAux' l₂ ++ List.map (cons a) (powersetAux' l₂)
[PROOFSTEP]
exact IH.append (IH.map _)
[GOAL]
case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ powersetAux' (b :: a :: l) ~ powersetAux' (a :: b :: l)
[PROOFSTEP]
simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
[GOAL]
case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ powersetAux' l ++
      (List.map (cons a) (powersetAux' l) ++
        (List.map (cons b) (powersetAux' l) ++ List.map (cons b ∘ cons a) (powersetAux' l))) ~
    powersetAux' l ++
      (List.map (cons b) (powersetAux' l) ++
        (List.map (cons a) (powersetAux' l) ++ List.map (cons a ∘ cons b) (powersetAux' l)))
[PROOFSTEP]
apply Perm.append_left
[GOAL]
case swap.a
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ List.map (cons a) (powersetAux' l) ++
      (List.map (cons b) (powersetAux' l) ++ List.map (cons b ∘ cons a) (powersetAux' l)) ~
    List.map (cons b) (powersetAux' l) ++
      (List.map (cons a) (powersetAux' l) ++ List.map (cons a ∘ cons b) (powersetAux' l))
[PROOFSTEP]
rw [← append_assoc, ← append_assoc, (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
[GOAL]
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ cons b ∘ cons a = cons a ∘ cons b
[PROOFSTEP]
funext s
[GOAL]
case h
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s
[PROOFSTEP]
simp [cons_swap]
[GOAL]
case swap.a
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ List.map (cons a) (powersetAux' l) ++ List.map (cons b) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l) ~
    List.map (cons b) (powersetAux' l) ++ List.map (cons a) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l)
[PROOFSTEP]
exact perm_append_comm.append_right _
[GOAL]
case trans
α : Type u_1
l₁✝ l₂✝ l₁ l₂ l₃ : List α
a✝¹ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : powersetAux' l₁ ~ powersetAux' l₂
IH₂ : powersetAux' l₂ ~ powersetAux' l₃
⊢ powersetAux' l₁ ~ powersetAux' l₃
[PROOFSTEP]
exact IH₁.trans IH₂
[GOAL]
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ powerset (a ::ₘ Quotient.mk (isSetoid α) l) =
    powerset (Quotient.mk (isSetoid α) l) + map (cons a) (powerset (Quotient.mk (isSetoid α) l))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ List.map ofList (sublists' l) ++ List.map (ofList ∘ List.cons a) (sublists' l) ~
    List.map ofList (sublists' l) ++ List.map ((fun x => a ::ₘ x) ∘ ofList) (sublists' l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s t : Multiset α
⊢ ∀ (a b : List α),
    Quotient.mk (isSetoid α) a ∈ powerset (Quotient.mk (isSetoid α) b) ↔
      Quotient.mk (isSetoid α) a ≤ Quotient.mk (isSetoid α) b
[PROOFSTEP]
simp [Subperm, and_comm]
[GOAL]
α : Type u_1
s : Multiset α
l : List α
⊢ map singleton (Quotient.mk (isSetoid α) l) ≤ powerset (Quotient.mk (isSetoid α) l)
[PROOFSTEP]
simp only [powerset_coe, quot_mk_to_coe, coe_le, coe_map]
[GOAL]
α : Type u_1
s : Multiset α
l : List α
⊢ List.map singleton l <+~ List.map ofList (sublists l)
[PROOFSTEP]
show l.map (((↑) : List α → Multiset α) ∘ List.ret) <+~ (sublists l).map (↑)
[GOAL]
α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ List.ret) l <+~ List.map ofList (sublists l)
[PROOFSTEP]
rw [← List.map_map]
[GOAL]
α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map List.ret l) <+~ List.map ofList (sublists l)
[PROOFSTEP]
exact ((map_ret_sublist_sublists _).map _).subperm
[GOAL]
α : Type u_1
s : Multiset α
⊢ ∀ (a : List α), ↑card (powerset (Quotient.mk (isSetoid α) a)) = 2 ^ ↑card (Quotient.mk (isSetoid α) a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ revzip (powersetAux l)
⊢ x.fst + x.snd = ↑l
[PROOFSTEP]
rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h 
[GOAL]
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a, a ∈ revzip (sublists l) ∧ Prod.map ofList ofList a = x
⊢ x.fst + x.snd = ↑l
[PROOFSTEP]
simp only [Prod_map, Prod.exists] at h 
[GOAL]
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ revzip (sublists l) ∧ (↑a, ↑b) = x
⊢ x.fst + x.snd = ↑l
[PROOFSTEP]
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
[GOAL]
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ revzip (sublists l)
⊢ (↑l₁, ↑l₂).fst + (↑l₁, ↑l₂).snd = ↑l
[PROOFSTEP]
exact Quot.sound (revzip_sublists _ _ _ h)
[GOAL]
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ revzip (powersetAux' l)
⊢ x.fst + x.snd = ↑l
[PROOFSTEP]
rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h 
[GOAL]
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a, a ∈ revzip (sublists' l) ∧ Prod.map ofList ofList a = x
⊢ x.fst + x.snd = ↑l
[PROOFSTEP]
simp only [Prod_map, Prod.exists] at h 
[GOAL]
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ revzip (sublists' l) ∧ (↑a, ↑b) = x
⊢ x.fst + x.snd = ↑l
[PROOFSTEP]
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
[GOAL]
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ revzip (sublists' l)
⊢ (↑l₁, ↑l₂).fst + (↑l₁, ↑l₂).snd = ↑l
[PROOFSTEP]
exact Quot.sound (revzip_sublists' _ _ _ h)
[GOAL]
α✝ : Type u_1
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
⊢ revzip l' = List.map (fun x => (x, ↑l - x)) l'
[PROOFSTEP]
have :
  Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
    ((revzip l').map Prod.fst) :=
  by
  rw [forall₂_map_right_iff, forall₂_same]
  rintro ⟨s, t⟩ h
  dsimp
  rw [← H h, add_tsub_cancel_left]
[GOAL]
α✝ : Type u_1
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
⊢ Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
[PROOFSTEP]
rw [forall₂_map_right_iff, forall₂_same]
[GOAL]
α✝ : Type u_1
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
⊢ ∀ (x : Multiset α × Multiset α), x ∈ revzip l' → x = (x.fst, ↑l - x.fst)
[PROOFSTEP]
rintro ⟨s, t⟩ h
[GOAL]
case mk
α✝ : Type u_1
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
s t : Multiset α
h : (s, t) ∈ revzip l'
⊢ (s, t) = ((s, t).fst, ↑l - (s, t).fst)
[PROOFSTEP]
dsimp
[GOAL]
case mk
α✝ : Type u_1
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
s t : Multiset α
h : (s, t) ∈ revzip l'
⊢ (s, t) = (s, ↑l - s)
[PROOFSTEP]
rw [← H h, add_tsub_cancel_left]
[GOAL]
α✝ : Type u_1
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
⊢ revzip l' = List.map (fun x => (x, ↑l - x)) l'
[PROOFSTEP]
rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]
[GOAL]
α✝ : Type u_1
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
⊢ Forall₂ (fun a c => a = (c, ↑l - c)) (revzip l') l'
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u_1
l : List α
⊢ revzip (powersetAux l) ~ revzip (powersetAux' l)
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
l : List α
this : DecidableEq α
⊢ revzip (powersetAux l) ~ revzip (powersetAux' l)
[PROOFSTEP]
rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']
[GOAL]
α : 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)
[PROOFSTEP]
exact powersetAux_perm_powersetAux'.map _
[GOAL]
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ revzip (powersetAux l₁) ~ revzip (powersetAux l₂)
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ revzip (powersetAux l₁) ~ revzip (powersetAux l₂)
[PROOFSTEP]
simp [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]
[GOAL]
α : 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₂)
[PROOFSTEP]
exact (powersetAux_perm p).map _
[GOAL]
α : Type u_1
n : ℕ
l : List α
⊢ powersetLenAux n l = List.map ofList (sublistsLen n l)
[PROOFSTEP]
rw [powersetLenAux, sublistsLenAux_eq, append_nil]
[GOAL]
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α),
    Quotient.mk (isSetoid α) a ∈ powersetLenAux n l ↔
      Quotient.mk (isSetoid α) a ≤ ↑l ∧ ↑card (Quotient.mk (isSetoid α) a) = n
[PROOFSTEP]
simp [powersetLenAux_eq_map_coe, Subperm]
[GOAL]
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), (∃ a_1, (a_1 <+ l ∧ length a_1 = n) ∧ a_1 ~ a) ↔ (∃ l_1, l_1 ~ a ∧ l_1 <+ l) ∧ length a = n
[PROOFSTEP]
exact fun l₁ =>
  ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩, fun ⟨⟨l₂, p, s⟩, e⟩ =>
    ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩
[GOAL]
α : Type u_1
l : List α
⊢ powersetLenAux 0 l = [0]
[PROOFSTEP]
simp [powersetLenAux_eq_map_coe]
[GOAL]
α : Type u_1
n : ℕ
a : α
l : List α
⊢ powersetLenAux (n + 1) (a :: l) = powersetLenAux (n + 1) l ++ List.map (cons a) (powersetLenAux n l)
[PROOFSTEP]
simp [powersetLenAux_eq_map_coe]
[GOAL]
α : Type u_1
n : ℕ
a : α
l : List α
⊢ List.map (ofList ∘ List.cons a) (sublistsLen n l) = List.map (cons a ∘ ofList) (sublistsLen n l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetLenAux n l₁ ~ powersetLenAux n l₂
[PROOFSTEP]
induction' n with n IHn generalizing l₁ l₂
[GOAL]
case zero
α : Type u_1
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetLenAux Nat.zero l₁ ~ powersetLenAux Nat.zero l₂
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetLenAux (Nat.succ n) l₁ ~ powersetLenAux (Nat.succ n) l₂
[PROOFSTEP]
induction' p with a l₁ l₂ p IH a b l l₁ l₂ l₃ _ _ IH₁ IH₂
[GOAL]
case succ.nil
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁ l₂ : List α
⊢ powersetLenAux (Nat.succ n) [] ~ powersetLenAux (Nat.succ n) []
[PROOFSTEP]
rfl
[GOAL]
case succ.cons
α : Type u_1
l₁✝¹ l₂✝¹ : List α
p✝ : l₁✝¹ ~ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : powersetLenAux (Nat.succ n) l₁ ~ powersetLenAux (Nat.succ n) l₂
⊢ powersetLenAux (Nat.succ n) (a :: l₁) ~ powersetLenAux (Nat.succ n) (a :: l₂)
[PROOFSTEP]
simp only [powersetLenAux_cons]
[GOAL]
case succ.cons
α : Type u_1
l₁✝¹ l₂✝¹ : List α
p✝ : l₁✝¹ ~ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : powersetLenAux (Nat.succ n) l₁ ~ powersetLenAux (Nat.succ n) l₂
⊢ powersetLenAux (n + 1) l₁ ++ List.map (cons a) (powersetLenAux n l₁) ~
    powersetLenAux (n + 1) l₂ ++ List.map (cons a) (powersetLenAux n l₂)
[PROOFSTEP]
exact IH.append ((IHn p).map _)
[GOAL]
case succ.swap
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁ l₂ : List α
a b : α
l : List α
⊢ powersetLenAux (Nat.succ n) (b :: a :: l) ~ powersetLenAux (Nat.succ n) (a :: b :: l)
[PROOFSTEP]
simp only [powersetLenAux_cons, append_assoc]
[GOAL]
case succ.swap
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁ l₂ : List α
a b : α
l : List α
⊢ powersetLenAux (n + 1) l ++
      (List.map (cons a) (powersetLenAux n l) ++ List.map (cons b) (powersetLenAux n (a :: l))) ~
    powersetLenAux (n + 1) l ++
      (List.map (cons b) (powersetLenAux n l) ++ List.map (cons a) (powersetLenAux n (b :: l)))
[PROOFSTEP]
apply Perm.append_left
[GOAL]
case succ.swap.a
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁ l₂ : List α
a b : α
l : List α
⊢ List.map (cons a) (powersetLenAux n l) ++ List.map (cons b) (powersetLenAux n (a :: l)) ~
    List.map (cons b) (powersetLenAux n l) ++ List.map (cons a) (powersetLenAux n (b :: l))
[PROOFSTEP]
cases n
[GOAL]
case succ.swap.a.zero
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
l₁ l₂ : List α
a b : α
l : List α
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux Nat.zero l₁ ~ powersetLenAux Nat.zero l₂
⊢ List.map (cons a) (powersetLenAux Nat.zero l) ++ List.map (cons b) (powersetLenAux Nat.zero (a :: l)) ~
    List.map (cons b) (powersetLenAux Nat.zero l) ++ List.map (cons a) (powersetLenAux Nat.zero (b :: l))
[PROOFSTEP]
simp [Perm.swap]
[GOAL]
case succ.swap.a.succ
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
l₁ l₂ : List α
a b : α
l : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux (Nat.succ n✝) l₁ ~ powersetLenAux (Nat.succ n✝) l₂
⊢ List.map (cons a) (powersetLenAux (Nat.succ n✝) l) ++ List.map (cons b) (powersetLenAux (Nat.succ n✝) (a :: l)) ~
    List.map (cons b) (powersetLenAux (Nat.succ n✝) l) ++ List.map (cons a) (powersetLenAux (Nat.succ n✝) (b :: l))
[PROOFSTEP]
simp only [powersetLenAux_cons, map_append, List.map_map]
[GOAL]
case succ.swap.a.succ
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
l₁ l₂ : List α
a b : α
l : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux (Nat.succ n✝) l₁ ~ powersetLenAux (Nat.succ n✝) l₂
⊢ List.map (cons a) (powersetLenAux (Nat.succ n✝) l) ++
      (List.map (cons b) (powersetLenAux (n✝ + 1) l) ++ List.map (cons b ∘ cons a) (powersetLenAux n✝ l)) ~
    List.map (cons b) (powersetLenAux (Nat.succ n✝) l) ++
      (List.map (cons a) (powersetLenAux (n✝ + 1) l) ++ List.map (cons a ∘ cons b) (powersetLenAux n✝ l))
[PROOFSTEP]
rw [← append_assoc, ← append_assoc, (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
[GOAL]
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
l₁ l₂ : List α
a b : α
l : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux (Nat.succ n✝) l₁ ~ powersetLenAux (Nat.succ n✝) l₂
⊢ cons b ∘ cons a = cons a ∘ cons b
[PROOFSTEP]
funext s
[GOAL]
case h
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
l₁ l₂ : List α
a b : α
l : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux (Nat.succ n✝) l₁ ~ powersetLenAux (Nat.succ n✝) l₂
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s
[PROOFSTEP]
simp [cons_swap]
[GOAL]
case succ.swap.a.succ
α : Type u_1
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
l₁ l₂ : List α
a b : α
l : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux (Nat.succ n✝) l₁ ~ powersetLenAux (Nat.succ n✝) l₂
⊢ List.map (cons a) (powersetLenAux (Nat.succ n✝) l) ++ List.map (cons b) (powersetLenAux (n✝ + 1) l) ++
      List.map (cons a ∘ cons b) (powersetLenAux n✝ l) ~
    List.map (cons b) (powersetLenAux (Nat.succ n✝) l) ++ List.map (cons a) (powersetLenAux (n✝ + 1) l) ++
      List.map (cons a ∘ cons b) (powersetLenAux n✝ l)
[PROOFSTEP]
exact perm_append_comm.append_right _
[GOAL]
case succ.trans
α : Type u_1
l₁✝¹ l₂✝¹ : List α
p : l₁✝¹ ~ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetLenAux n l₁ ~ powersetLenAux n l₂
l₁✝ l₂✝ l₁ l₂ l₃ : List α
a✝¹ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : powersetLenAux (Nat.succ n) l₁ ~ powersetLenAux (Nat.succ n) l₂
IH₂ : powersetLenAux (Nat.succ n) l₂ ~ powersetLenAux (Nat.succ n) l₃
⊢ powersetLenAux (Nat.succ n) l₁ ~ powersetLenAux (Nat.succ n) l₃
[PROOFSTEP]
exact IH₁.trans IH₂
[GOAL]
α : Type u_1
s : Multiset α
l : List α
⊢ powersetLen 0 (Quotient.mk (isSetoid α) l) = {0}
[PROOFSTEP]
simp [powersetLen_coe']
[GOAL]
α : Type u_1
n : ℕ
a : α
s : Multiset α
l : List α
⊢ powersetLen (n + 1) (a ::ₘ Quotient.mk (isSetoid α) l) =
    powersetLen (n + 1) (Quotient.mk (isSetoid α) l) + map (cons a) (powersetLen n (Quotient.mk (isSetoid α) l))
[PROOFSTEP]
simp [powersetLen_coe']
[GOAL]
α : Type u_1
n : ℕ
s t : Multiset α
l : List α
⊢ s ∈ powersetLen n (Quotient.mk (isSetoid α) l) ↔ s ≤ Quotient.mk (isSetoid α) l ∧ ↑card s = n
[PROOFSTEP]
simp [powersetLen_coe']
[GOAL]
α : Type u_1
n : ℕ
s : Multiset α
⊢ ∀ (a : List α), ↑card (powersetLen n (Quotient.mk (isSetoid α) a)) = Nat.choose (↑card (Quotient.mk (isSetoid α) a)) n
[PROOFSTEP]
simp [powersetLen_coe]
[GOAL]
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ powersetLen n (Quotient.mk (isSetoid α) l) ≤ powerset (Quotient.mk (isSetoid α) l)
[PROOFSTEP]
simp only [quot_mk_to_coe, powersetLen_coe, powerset_coe', coe_le]
[GOAL]
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList (sublists' l)
[PROOFSTEP]
exact ((sublistsLen_sublist_sublists' _ _).map _).subperm
[GOAL]
α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ powersetLen n ↑l₁ ≤ powersetLen n ↑l₂
[PROOFSTEP]
simp only [powersetLen_coe, coe_le]
[GOAL]
α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)
[PROOFSTEP]
exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
⊢ powersetLen n (map f s) = map (map f) (powersetLen n s)
[PROOFSTEP]
induction' s using Multiset.induction with t s ih generalizing n
[GOAL]
case empty
α : Type u_1
β : Type u_2
f : α → β
n✝ n : ℕ
⊢ powersetLen n (map f 0) = map (map f) (powersetLen n 0)
[PROOFSTEP]
cases n
[GOAL]
case empty.zero
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
⊢ powersetLen Nat.zero (map f 0) = map (map f) (powersetLen Nat.zero 0)
[PROOFSTEP]
simp [powersetLen_zero_left, powersetLen_zero_right]
[GOAL]
case empty.succ
α : Type u_1
β : Type u_2
f : α → β
n n✝ : ℕ
⊢ powersetLen (Nat.succ n✝) (map f 0) = map (map f) (powersetLen (Nat.succ n✝) 0)
[PROOFSTEP]
simp [powersetLen_zero_left, powersetLen_zero_right]
[GOAL]
case cons
α : Type u_1
β : Type u_2
f : α → β
n✝ : ℕ
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetLen n (map f s) = map (map f) (powersetLen n s)
n : ℕ
⊢ powersetLen n (map f (t ::ₘ s)) = map (map f) (powersetLen n (t ::ₘ s))
[PROOFSTEP]
cases n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetLen n (map f s) = map (map f) (powersetLen n s)
⊢ powersetLen Nat.zero (map f (t ::ₘ s)) = map (map f) (powersetLen Nat.zero (t ::ₘ s))
[PROOFSTEP]
simp [ih, map_comp_cons]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetLen n (map f s) = map (map f) (powersetLen n s)
n✝ : ℕ
⊢ powersetLen (Nat.succ n✝) (map f (t ::ₘ s)) = map (map f) (powersetLen (Nat.succ n✝) (t ::ₘ s))
[PROOFSTEP]
simp [ih, map_comp_cons]
[GOAL]
α✝ : Type u_1
α : Type u_2
S : Multiset α
⊢ (bind (range (↑card S + 1)) fun k => powersetLen k S) = powerset S
[PROOFSTEP]
induction S using Quotient.inductionOn
[GOAL]
case h
α✝ : Type u_1
α : Type u_2
a✝ : List α
⊢ (bind (range (↑card (Quotient.mk (isSetoid α) a✝) + 1)) fun k => powersetLen k (Quotient.mk (isSetoid α) a✝)) =
    powerset (Quotient.mk (isSetoid α) a✝)
[PROOFSTEP]
simp_rw [quot_mk_to_coe, powerset_coe', powersetLen_coe, ← coe_range, coe_bind, ← List.bind_map, coe_card]
[GOAL]
case h
α✝ : Type u_1
α : Type u_2
a✝ : List α
⊢ ↑(List.map ofList (List.bind (List.range (length a✝ + 1)) fun a => sublistsLen a a✝)) =
    ↑(List.map ofList (sublists' a✝))
[PROOFSTEP]
exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)
[GOAL]
α : Type u_1
s : Multiset α
l : List α
h : Nodup (Quotient.mk (isSetoid α) l)
⊢ Nodup (powerset (Quotient.mk (isSetoid α) l))
[PROOFSTEP]
simp only [quot_mk_to_coe, powerset_coe', coe_nodup]
[GOAL]
α : Type u_1
s : Multiset α
l : List α
h : Nodup (Quotient.mk (isSetoid α) l)
⊢ List.Nodup (List.map ofList (sublists' l))
[PROOFSTEP]
refine' (nodup_sublists'.2 h).map_on _
[GOAL]
α : Type u_1
s : Multiset α
l : List α
h : Nodup (Quotient.mk (isSetoid α) l)
⊢ ∀ (x : List α), x ∈ sublists' l → ∀ (y : List α), y ∈ sublists' l → ↑x = ↑y → x = y
[PROOFSTEP]
exact fun x sx y sy e => (h.sublist_ext (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)
