α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is)) →
      map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f []) →
        map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (ts is : List α), map (map f) (permutationsAux ts is) = permutationsAux (map f ts) (map f is)
refine' permutationsAux.rec (by simp) _
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f [])
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is)) →
      map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f []) →
        map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
introv IH1 IH2
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) []
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f [])
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
rw [map] at IH2
no goals
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) []
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
simp only [foldr_permutationsAux2, map_append, map, map_map_permutationsAux2, permutations,
  bind_map, IH1, append_assoc, permutationsAux_cons, cons_bind, ← IH2, map_bind]
no goals
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (is : List α), map (map f) (permutationsAux [] is) = permutationsAux (map f []) (map f is)
simp