case nil
α : Type uu
β : Type vv
l₁ l₂ s t : List α
⊢ List.permutations' [] ~ List.permutations' []

case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ t✝ : List α
a : α
s t : List α
a✝ : s ~ t
IH : List.permutations' s ~ List.permutations' t
⊢ List.permutations' (a :: s) ~ List.permutations' (a :: t)

case swap
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ List.permutations' (b :: a :: l) ~ List.permutations' (a :: b :: l)

case trans
α : Type uu
β : Type vv
l₁ l₂ s✝ t✝ s t u : List α
a✝¹ : s ~ t
a✝ : t ~ u
IH₁ : List.permutations' s ~ List.permutations' t
IH₂ : List.permutations' t ~ List.permutations' u
⊢ List.permutations' s ~ List.permutations' u
α : Type uu
β : Type vv
l₁ l₂ s t : List α
p : s ~ t
⊢ List.permutations' s ~ List.permutations' t
induction' p with a s t _ IH a b l s t u _ _ IH₁ IH₂
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ s t : List α
⊢ List.permutations' [] ~ List.permutations' []
simp
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ t✝ : List α
a : α
s t : List α
a✝ : s ~ t
IH : List.permutations' s ~ List.permutations' t
⊢ List.permutations' (a :: s) ~ List.permutations' (a :: t)
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ t✝ : List α
a : α
s t : List α
a✝ : s ~ t
IH : List.permutations' s ~ List.permutations' t
⊢ List.permutations' (a :: s) ~ List.permutations' (a :: t)
simp only [permutations']
no goals
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ t✝ : List α
a : α
s t : List α
a✝ : s ~ t
IH : List.permutations' s ~ List.permutations' t
⊢ List.permutations' (a :: s) ~ List.permutations' (a :: t)
exact IH.bind_right _
case swap
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ List.bind (List.bind (List.permutations' l) (permutations'Aux a)) (permutations'Aux b) ~
    List.bind (List.bind (List.permutations' l) (permutations'Aux b)) (permutations'Aux a)
case swap
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ List.permutations' (b :: a :: l) ~ List.permutations' (a :: b :: l)
dsimp [permutations']
case swap
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ (List.bind (List.permutations' l) fun x => List.bind (permutations'Aux a x) (permutations'Aux b)) ~
    List.bind (List.permutations' l) fun x => List.bind (permutations'Aux b x) (permutations'Aux a)
case swap
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ List.bind (List.bind (List.permutations' l) (permutations'Aux a)) (permutations'Aux b) ~
    List.bind (List.bind (List.permutations' l) (permutations'Aux b)) (permutations'Aux a)
rw [bind_assoc, bind_assoc]
case swap.h
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ ∀ (a_1 : List α),
    a_1 ∈ List.permutations' l →
      List.bind (permutations'Aux a a_1) (permutations'Aux b) ~ List.bind (permutations'Aux b a_1) (permutations'Aux a)
case swap
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ (List.bind (List.permutations' l) fun x => List.bind (permutations'Aux a x) (permutations'Aux b)) ~
    List.bind (List.permutations' l) fun x => List.bind (permutations'Aux b x) (permutations'Aux a)
apply Perm.bind_left
case swap.h
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l l' : List α
a✝ : l' ∈ List.permutations' l
⊢ List.bind (permutations'Aux a l') (permutations'Aux b) ~ List.bind (permutations'Aux b l') (permutations'Aux a)
case swap.h
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l : List α
⊢ ∀ (a_1 : List α),
    a_1 ∈ List.permutations' l →
      List.bind (permutations'Aux a a_1) (permutations'Aux b) ~ List.bind (permutations'Aux b a_1) (permutations'Aux a)
intro l' _
no goals
case swap.h
α : Type uu
β : Type vv
l₁ l₂ s t : List α
a b : α
l l' : List α
a✝ : l' ∈ List.permutations' l
⊢ List.bind (permutations'Aux a l') (permutations'Aux b) ~ List.bind (permutations'Aux b l') (permutations'Aux a)
apply perm_permutations'Aux_comm
no goals
case trans
α : Type uu
β : Type vv
l₁ l₂ s✝ t✝ s t u : List α
a✝¹ : s ~ t
a✝ : t ~ u
IH₁ : List.permutations' s ~ List.permutations' t
IH₂ : List.permutations' t ~ List.permutations' u
⊢ List.permutations' s ~ List.permutations' u
exact IH₁.trans IH₂