case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
⊢ filter p [] ++ filter (fun x => decide ¬p x = true) [] ~ []

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
⊢ filter p (x :: l) ++ filter (fun x => decide ¬p x = true) (x :: l) ~ x :: l
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
induction' l with x l ih
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
⊢ filter p [] ++ filter (fun x => decide ¬p x = true) [] ~ []
rfl
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : p x = true
⊢ filter p (x :: l) ++ filter (fun x => decide ¬p x = true) (x :: l) ~ x :: l

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : ¬p x = true
⊢ filter p (x :: l) ++ filter (fun x => decide ¬p x = true) (x :: l) ~ x :: l
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
⊢ filter p (x :: l) ++ filter (fun x => decide ¬p x = true) (x :: l) ~ x :: l
by_cases h : p x
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : p x = true
⊢ x :: (filter p l ++ filter (fun x => decide ¬p x = true) l) ~ x :: l
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : p x = true
⊢ filter p (x :: l) ++ filter (fun x => decide ¬p x = true) (x :: l) ~ x :: l
simp only [h, filter_cons_of_pos, filter_cons_of_neg, not_true, not_false_iff, cons_append]
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : p x = true
⊢ x :: (filter p l ++ filter (fun x => decide ¬p x = true) l) ~ x :: l
exact ih.cons x
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : ¬p x = true
⊢ filter p l ++ x :: filter (fun x => decide ¬p x = true) l ~ x :: l
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : ¬p x = true
⊢ filter p (x :: l) ++ filter (fun x => decide ¬p x = true) (x :: l) ~ x :: l
simp only [h, filter_cons_of_neg, not_false_iff, filter_cons_of_pos]
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : ¬p x = true
⊢ filter p l ++ x :: filter (fun x => decide ¬p x = true) l ~
    x :: (filter p l ++ filter (fun x => decide ¬p x = true) l)
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : ¬p x = true
⊢ filter p l ++ x :: filter (fun x => decide ¬p x = true) l ~ x :: l
refine' Perm.trans _ (ih.cons x)
no goals
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
h : ¬p x = true
⊢ filter p l ++ x :: filter (fun x => decide ¬p x = true) l ~
    x :: (filter p l ++ filter (fun x => decide ¬p x = true) l)
exact perm_append_comm.trans (perm_append_comm.cons _)