-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCardAux_perm {n} {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    powersetCardAux n l₁ ~ powersetCardAux n l₂

Proof state:
case zero
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
⊢ powersetCardAux (n + 1) (x✝ :: l₁✝) ~ powersetCardAux (n + 1) (x✝ :: l₂✝)

Tactic:
simp only [powersetCardAux_cons]

Result:
case succ.cons
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
⊢ powersetCardAux (n + 1) l₁✝ ++ List.map (cons x✝) (powersetCardAux n l₁✝) ~
    powersetCardAux (n + 1) l₂✝ ++ List.map (cons x✝) (powersetCardAux n l₂✝)

Proof state:
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ cons b ∘ cons a = cons a ∘ cons b

Tactic:
funext s

Result:
case h
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s

Proof state:
case succ.swap.a.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝))

Tactic:
rw [← append_assoc, ← append_assoc,
  (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]

Result:
case succ.swap.a.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)

Proof state:
α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux n l₁ ~ powersetCardAux n l₂

Tactic:
induction' n with n IHn generalizing l₁ l₂

Result:
case zero
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂

case succ
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂

Proof state:
case succ.swap.a.zero
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂
⊢ List.map (cons a) (powersetCardAux 0 l✝) ++ List.map (cons b) (powersetCardAux 0 (a :: l✝)) ~
    List.map (cons b) (powersetCardAux 0 l✝) ++ List.map (cons a) (powersetCardAux 0 (b :: l✝))

Tactic:
simp [Perm.swap]

Result:
no goals

Proof state:
case succ.swap.a.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) (a :: l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) (b :: l✝))

Tactic:
simp only [powersetCardAux_cons, map_append, List.map_map]

Result:
case succ.swap.a.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝))

Proof state:
case succ.swap.a
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetCardAux n l✝) ++ List.map (cons b) (powersetCardAux n (a :: l✝)) ~
    List.map (cons b) (powersetCardAux n l✝) ++ List.map (cons a) (powersetCardAux n (b :: l✝))

Tactic:
cases n

Result:
case succ.swap.a.zero
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂
⊢ List.map (cons a) (powersetCardAux 0 l✝) ++ List.map (cons b) (powersetCardAux 0 (a :: l✝)) ~
    List.map (cons b) (powersetCardAux 0 l✝) ++ List.map (cons a) (powersetCardAux 0 (b :: l✝))

case succ.swap.a.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) (a :: l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) (b :: l✝))

Proof state:
case succ.cons
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
⊢ powersetCardAux (n + 1) l₁✝ ++ List.map (cons x✝) (powersetCardAux n l₁✝) ~
    powersetCardAux (n + 1) l₂✝ ++ List.map (cons x✝) (powersetCardAux n l₂✝)

Tactic:
exact IH.append ((IHn p).map _)

Result:
no goals

Proof state:
case succ.swap.a.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)

Tactic:
exact perm_append_comm.append_right _

Result:
no goals

Proof state:
case succ.trans
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
IH₂ : powersetCardAux (n + 1) l₂✝ ~ powersetCardAux (n + 1) l₃✝
⊢ powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₃✝

Tactic:
exact IH₁.trans IH₂

Result:
no goals

Proof state:
case h
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s

Tactic:
simp [cons_swap]

Result:
no goals