case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
f g : α → List β
a : α
l : List α
IH : List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x
⊢ f a ++ (List.bind l f ++ (g a ++ List.bind l g)) ~ f a ++ (g a ++ List.bind l fun x => f x ++ g x)
α : Type uu
β : Type vv
l₁ l₂ l : List α
f g : α → List β
⊢ List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x
induction' l with a l IH <;> simp
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
f g : α → List β
a : α
l : List α
IH : List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x
⊢ List.bind l f ++ (g a ++ List.bind l g) ~ g a ++ (List.bind l f ++ List.bind l g)
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
f g : α → List β
a : α
l : List α
IH : List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x
⊢ f a ++ (List.bind l f ++ (g a ++ List.bind l g)) ~ f a ++ (g a ++ List.bind l fun x => f x ++ g x)
refine' (Perm.trans _ (IH.append_left _)).append_left _
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
f g : α → List β
a : α
l : List α
IH : List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x
⊢ List.bind l f ++ g a ++ List.bind l g ~ g a ++ List.bind l f ++ List.bind l g
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
f g : α → List β
a : α
l : List α
IH : List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x
⊢ List.bind l f ++ (g a ++ List.bind l g) ~ g a ++ (List.bind l f ++ List.bind l g)
rw [← append_assoc, ← append_assoc]
no goals
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
f g : α → List β
a : α
l : List α
IH : List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x
⊢ List.bind l f ++ g a ++ List.bind l g ~ g a ++ List.bind l f ++ List.bind l g
exact perm_append_comm.append_right _