[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)


[GOAL]
n✝ n : ℕ
⊢ boddDiv2 n = (bodd n, div2 n)
[PROOFSTEP]
unfold bodd div2
[GOAL]
n✝ n : ℕ
⊢ boddDiv2 n = ((boddDiv2 n).fst, (boddDiv2 n).snd)
[PROOFSTEP]
cases boddDiv2 n
[GOAL]
case mk
n✝ n : ℕ
fst✝ : Bool
snd✝ : ℕ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
h : m = n
⊢ bit0 m = bit0 n
[PROOFSTEP]
subst h
[GOAL]
n m : ℕ
⊢ bit0 m = bit0 m
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
h : m = n
⊢ bit1 m = bit1 n
[PROOFSTEP]
subst h
[GOAL]
n m : ℕ
⊢ bit1 m = bit1 m
[PROOFSTEP]
rfl
[GOAL]
n✝ n : ℕ
h : n = 0
⊢ bit1 n = 1
[PROOFSTEP]
subst h
[GOAL]
n : ℕ
⊢ bit1 0 = 1
[PROOFSTEP]
rfl
[GOAL]
n✝ n : ℕ
h : n = 0
⊢ 1 = bit1 n
[PROOFSTEP]
subst h
[GOAL]
n : ℕ
⊢ 1 = bit1 0
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0
[PROOFSTEP]
cases b <;> [exact Nat.bit0_ne_zero h; exact Nat.bit1_ne_zero _]
[GOAL]
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0
[PROOFSTEP]
cases b
[GOAL]
case false
n✝ n : ℕ
h : n ≠ 0
⊢ bit false n ≠ 0
[PROOFSTEP]
exact Nat.bit0_ne_zero h
[GOAL]
case true
n✝ n : ℕ
h : n ≠ 0
⊢ bit true n ≠ 0
[PROOFSTEP]
exact Nat.bit1_ne_zero _
[GOAL]
n : ℕ
⊢ bit0 n % 2 = 0
[PROOFSTEP]
rw [Nat.mod_two_of_bodd]
[GOAL]
n : ℕ
⊢ (bif bodd (bit0 n) then 1 else 0) = 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ bit1 n % 2 = 1
[PROOFSTEP]
rw [Nat.mod_two_of_bodd]
[GOAL]
n : ℕ
⊢ (bif bodd (bit1 n) then 1 else 0) = 1
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
h : 0 < bit0 n
⊢ 0 < n
[PROOFSTEP]
cases n
[GOAL]
case zero
n : ℕ
h : 0 < bit0 zero
⊢ 0 < zero
[PROOFSTEP]
cases h
[GOAL]
case succ
n n✝ : ℕ
h : 0 < bit0 (succ n✝)
⊢ 0 < succ n✝
[PROOFSTEP]
apply succ_pos
[GOAL]
n✝ : ℕ
C : ℕ → Sort u
H : (b : Bool) → (n : ℕ) → C (bit b n)
b : Bool
n : ℕ
⊢ HEq (H (bodd (bit b n)) (div2 (bit b n))) (H b n)
[PROOFSTEP]
rw [bodd_bit, div2_bit]
[GOAL]
n : ℕ
C : ℕ → Sort u
⊢ Function.Injective fun H n => bitCasesOn n H
[PROOFSTEP]
intro H₁ H₂ h
[GOAL]
n : ℕ
C : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → C (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
⊢ H₁ = H₂
[PROOFSTEP]
ext b n
[GOAL]
case h.h
n✝ : ℕ
C : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → C (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n
[PROOFSTEP]
simpa only [bitCasesOn_bit] using congr_fun h (bit b n)
[GOAL]
n✝ n : ℕ
h : n = 0
⊢ bit0 n = 0
[PROOFSTEP]
simp [h]
[GOAL]
n✝ n : ℕ
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false
[PROOFSTEP]
constructor
[GOAL]
case mp
n✝ n : ℕ
b : Bool
⊢ bit b n = 0 → n = 0 ∧ b = false
[PROOFSTEP]
cases b
[GOAL]
case mp.false
n✝ n : ℕ
⊢ bit false n = 0 → n = 0 ∧ false = false
[PROOFSTEP]
simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]
[GOAL]
case mp.true
n✝ n : ℕ
⊢ bit true n = 0 → n = 0 ∧ true = false
[PROOFSTEP]
simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]
[GOAL]
case mpr
n✝ n : ℕ
b : Bool
⊢ n = 0 ∧ b = false → bit b n = 0
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case mpr.intro
n : ℕ
⊢ bit false 0 = 0
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [binaryRec]
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
rcases bit_eq_zero_iff.mp h' with ⟨rfl, rfl⟩
[GOAL]
case pos.intro
n : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z ∨ (0 = 0 → false = true)
h' : bit false 0 = 0
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 (binaryRec z f 0)
[PROOFSTEP]
rw [binaryRec_zero]
[GOAL]
case pos.intro
n : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z ∨ (0 = 0 → false = true)
h' : bit false 0 = 0
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
simp only [imp_false, or_false_iff, eq_self_iff_true, not_true] at h
[GOAL]
case pos.intro
n : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : bit false 0 = 0
h : f false 0 z = z
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
exact h.symm
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ (let n' := div2 (bit b n);
    let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
    Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
dsimp only []
  -- Porting note: this line was `generalize_proofs e`:
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
generalize
  @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
    (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
  e
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))
⊢ Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
revert e
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))),
    Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [bodd_bit, div2_bit]
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit b n)), Eq.mpr e (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
intros
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e✝ : C (bit b n) = C (bit b n)
⊢ Eq.mpr e✝ (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → C n → C (bit b n)
b : Bool
n : ℕ
ih : C n
h : ¬(n = 0 → b = true)
⊢ C (bit b n)
[PROOFSTEP]
convert z
[GOAL]
case h.e'_1
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → C n → C (bit b n)
b : Bool
n : ℕ
ih : C n
h : ¬(n = 0 → b = true)
⊢ bit b n = 0
[PROOFSTEP]
rw [bit_eq_zero_iff]
[GOAL]
case h.e'_1
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → C n → C (bit b n)
b : Bool
n : ℕ
ih : C n
h : ¬(n = 0 → b = true)
⊢ n = 0 ∧ b = false
[PROOFSTEP]
simpa using h
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z₀ : C 0
z₁ : C 1
f : (b : Bool) → (n : ℕ) → n ≠ 0 → C n → C (bit b n)
b : Bool
n : ℕ
h : n = 0 → b = true
ih : C n
h' : n = 0
⊢ C (bit b n)
[PROOFSTEP]
rw [h', h h']
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z₀ : C 0
z₁ : C 1
f : (b : Bool) → (n : ℕ) → n ≠ 0 → C n → C (bit b n)
b : Bool
n : ℕ
h : n = 0 → b = true
ih : C n
h' : n = 0
⊢ C (bit true 0)
[PROOFSTEP]
exact z₁
[GOAL]
n : ℕ
⊢ bits 0 = []
[PROOFSTEP]
simp [Nat.bits]
[GOAL]
n✝ n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ bits (bit b n) = b :: bits n
[PROOFSTEP]
rw [Nat.bits, binaryRec_eq']
[GOAL]
case h
n✝ n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
⊢ bits 1 = [true]
[PROOFSTEP]
convert bit1_bits 0
[GOAL]
n✝ n : ℕ
⊢ bodd n = List.headI (bits n)
[PROOFSTEP]
induction' n using Nat.binaryRec' with b n h _
[GOAL]
case z
n : ℕ
⊢ bodd 0 = List.headI (bits 0)
[PROOFSTEP]
simp
[GOAL]
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n = 0 → b = true
a✝ : bodd n = List.headI (bits n)
⊢ bodd (bit b n) = List.headI (bits (bit b n))
[PROOFSTEP]
simp [bodd_bit, bits_append_bit _ _ h]
[GOAL]
n✝ n : ℕ
⊢ bits (div2 n) = List.tail (bits n)
[PROOFSTEP]
induction' n using Nat.binaryRec' with b n h _
[GOAL]
case z
n : ℕ
⊢ bits (div2 0) = List.tail (bits 0)
[PROOFSTEP]
simp
[GOAL]
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n = 0 → b = true
a✝ : bits (div2 n) = List.tail (bits n)
⊢ bits (div2 (bit b n)) = List.tail (bits (bit b n))
[PROOFSTEP]
simp [div2_bit, bits_append_bit _ _ h]