case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
a b : α
⊢ List.bind (permutations'Aux a []) (permutations'Aux b) ~ List.bind (permutations'Aux b []) (permutations'Aux a)

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
⊢ List.bind (permutations'Aux a (c :: l)) (permutations'Aux b) ~
    List.bind (permutations'Aux b (c :: l)) (permutations'Aux a)
α : Type uu
β : Type vv
l₁ l₂ : List α
a b : α
l : List α
⊢ List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
induction' l with c l ih
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (cons a ∘ cons c) (permutations'Aux b l) ++
          List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b)) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (cons b ∘ cons c) (permutations'Aux a l) ++
          List.bind (map (cons c) (permutations'Aux b l)) (permutations'Aux a))
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
⊢ List.bind (permutations'Aux a (c :: l)) (permutations'Aux b) ~
    List.bind (permutations'Aux b (c :: l)) (permutations'Aux a)
simp [permutations'Aux]
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ List.bind (map (cons c) (permutations'Aux b l)) (permutations'Aux a)
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (cons a ∘ cons c) (permutations'Aux b l) ++
          List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b)) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (cons b ∘ cons c) (permutations'Aux a l) ++
          List.bind (map (cons c) (permutations'Aux b l)) (permutations'Aux a))
apply Perm.swap'
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
this :
  ∀ (a b : α),
    List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ List.bind (map (cons c) (permutations'Aux b l)) (permutations'Aux a)
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ List.bind (map (cons c) (permutations'Aux b l)) (permutations'Aux a)
have :
  ∀ a b,
    (map (cons c) (permutations'Aux a l)).bind (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) ((permutations'Aux a l).bind (permutations'Aux b)) := by
  intros a' b'
  simp only [map_bind, permutations'Aux]
  show List.bind (permutations'Aux _ l) (fun a => ([b' :: c :: a] ++
    map (cons c) (permutations'Aux _ a))) ~ _
  refine' (bind_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans _
  rw [← map_eq_bind, ← bind_map]
  exact Perm.refl _
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
this :
  ∀ (a b : α),
    List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++
      (map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++
      (map (cons a ∘ cons c) (permutations'Aux b l) ++
        map (cons c) (List.bind (permutations'Aux b l) (permutations'Aux a)))
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
this :
  ∀ (a b : α),
    List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ List.bind (map (cons c) (permutations'Aux b l)) (permutations'Aux a)
refine' (((this _ _).append_left _).trans _).trans ((this _ _).append_left _).symm
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
this :
  ∀ (a b : α),
    List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons b ∘ cons c) (permutations'Aux a l) ++
      map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons a ∘ cons c) (permutations'Aux b l) ++
      map (cons c) (List.bind (permutations'Aux b l) (permutations'Aux a))
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
this :
  ∀ (a b : α),
    List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++
      (map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++
      (map (cons a ∘ cons c) (permutations'Aux b l) ++
        map (cons c) (List.bind (permutations'Aux b l) (permutations'Aux a)))
rw [← append_assoc, ← append_assoc]
no goals
case cons.p
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
this :
  ∀ (a b : α),
    List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons b ∘ cons c) (permutations'Aux a l) ++
      map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons a ∘ cons c) (permutations'Aux b l) ++
      map (cons c) (List.bind (permutations'Aux b l) (permutations'Aux a))
exact perm_append_comm.append (ih.map _)
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
a b : α
⊢ List.bind (permutations'Aux a []) (permutations'Aux b) ~ List.bind (permutations'Aux b []) (permutations'Aux a)
simp [swap]
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ List.bind (map (cons c) (permutations'Aux a' l)) (permutations'Aux b') ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
⊢ ∀ (a b : α),
    List.bind (map (cons c) (permutations'Aux a l)) (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (List.bind (permutations'Aux a l) (permutations'Aux b))
intros a' b'
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ (List.bind (permutations'Aux a' l) fun a => (b' :: c :: a) :: map (cons c) (permutations'Aux b' a)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ List.bind (map (cons c) (permutations'Aux a' l)) (permutations'Aux b') ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
simp only [map_bind, permutations'Aux]
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ (List.bind (permutations'Aux a' l) fun a => [b' :: c :: a] ++ map (cons c) (permutations'Aux b' a)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ (List.bind (permutations'Aux a' l) fun a => (b' :: c :: a) :: map (cons c) (permutations'Aux b' a)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
show List.bind (permutations'Aux _ l) (fun a => ([b' :: c :: a] ++
  map (cons c) (permutations'Aux _ a))) ~ _
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ ((List.bind (permutations'Aux a' l) fun x => [b' :: c :: x]) ++
      List.bind (permutations'Aux a' l) fun a => map (cons c) (permutations'Aux b' a)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ (List.bind (permutations'Aux a' l) fun a => [b' :: c :: a] ++ map (cons c) (permutations'Aux b' a)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
refine' (bind_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans _
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ map (fun x => b' :: c :: x) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) fun a => permutations'Aux b' a) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ ((List.bind (permutations'Aux a' l) fun x => [b' :: c :: x]) ++
      List.bind (permutations'Aux a' l) fun a => map (cons c) (permutations'Aux b' a)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
rw [← map_eq_bind, ← bind_map]
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
a b c : α
l : List α
ih : List.bind (permutations'Aux a l) (permutations'Aux b) ~ List.bind (permutations'Aux b l) (permutations'Aux a)
a' b' : α
⊢ map (fun x => b' :: c :: x) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) fun a => permutations'Aux b' a) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (List.bind (permutations'Aux a' l) (permutations'Aux b'))
exact Perm.refl _