-- Mathlib/Data/Multiset/Powerset.lean
theorem powerset_aux'_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetAux' l₁ ~ powersetAux' l₂

Proof state:
case nil
α : Type u_1
l₁ l₂ : List α
⊢ powersetAux' [] ~ powersetAux' []

Tactic:
simp

Result:
no goals

Proof state:
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✝)

Tactic:
exact perm_append_comm.append_right _

Result:
no goals

Proof state:
case h
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s

Tactic:
simp [cons_swap]

Result:
no goals

Proof state:
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✝)))

Tactic:
apply Perm.append_left

Result:
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✝))

Proof state:
case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ powersetAux' (b :: a :: l✝) ~ powersetAux' (a :: b :: l✝)

Tactic:
simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]

Result:
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✝)))

Proof state:
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✝))

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

Result:
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✝)

Proof state:
case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : powersetAux' l₁✝ ~ powersetAux' l₂✝
⊢ powersetAux' l₁✝ ++ List.map (cons x✝) (powersetAux' l₁✝) ~ powersetAux' l₂✝ ++ List.map (cons x✝) (powersetAux' l₂✝)

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

Result:
no goals

Proof state:
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₃✝

Tactic:
exact IH₁.trans IH₂

Result:
no goals

Proof state:
case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : powersetAux' l₁✝ ~ powersetAux' l₂✝
⊢ powersetAux' (x✝ :: l₁✝) ~ powersetAux' (x✝ :: l₂✝)

Tactic:
simp only [powersetAux'_cons]

Result:
case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : powersetAux' l₁✝ ~ powersetAux' l₂✝
⊢ powersetAux' l₁✝ ++ List.map (cons x✝) (powersetAux' l₁✝) ~ powersetAux' l₂✝ ++ List.map (cons x✝) (powersetAux' l₂✝)

Proof state:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetAux' l₁ ~ powersetAux' l₂

Tactic:
induction p with
| nil => simp
| cons _ _ IH =>
  simp only [powersetAux'_cons]
  exact IH.append (IH.map _)
| swap a b =>
  simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
  apply Perm.append_left
  rw [← append_assoc, ← append_assoc,
    (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
  exact perm_append_comm.append_right _
| trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ cons b ∘ cons a = cons a ∘ cons b

Tactic:
funext s

Result:
case h
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s