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₂

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₂
α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetLenAux n l₁ ~ powersetLenAux n l₂
induction' n with n IHn generalizing l₁ l₂
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) []

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

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)

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₃
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₂
induction' p with a l₁ l₂ p IH a b l l₁ l₂ l₃ _ _ IH₁ IH₂
no goals
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₂
simp
no goals
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) []
rfl
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₂)
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₂)
simp only [powersetLenAux_cons]
no goals
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₂)
exact IH.append ((IHn p).map _)
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)))
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)
simp only [powersetLenAux_cons, append_assoc]
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))
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)))
apply Perm.append_left
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))

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))
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))
cases n
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))
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))
simp only [powersetLenAux_cons, map_append, List.map_map]
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)
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))
rw [← append_assoc, ← append_assoc,
  (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
no goals
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)
exact perm_append_comm.append_right _
no goals
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))
simp [Perm.swap]
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
α : 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
funext s
no goals
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
simp [cons_swap]
no goals
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₃
exact IH₁.trans IH₂