α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (ts is l : List α), l ~ is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts is
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ {ts is l : List α}, l ~ is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts is
show ∀ (ts is l : List α),
    l ~ is ++ ts → (∃ (is' : _)(_ : is' ~ is), l = is' ++ ts) ∨ l ∈ permutationsAux ts is
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (t : α) (ts is : List α),
    (∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []) →
        ∀ (l : List α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ permutationsAux (t :: ts) is
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (ts is l : List α), l ~ is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts is
refine' permutationsAux.rec (by simp) _
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ permutationsAux (t :: ts) is
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (t : α) (ts is : List α),
    (∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []) →
        ∀ (l : List α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ permutationsAux (t :: ts) is
intro t ts is IH1 IH2 l p
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ permutationsAux (t :: ts) is
rw [permutationsAux_cons, mem_foldr_permutationsAux2]
case inl.intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

case inr
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ permutationsAux ts (t :: is)
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
rcases IH1 _ (p.trans perm_middle) with (⟨is', p', e⟩ | m)
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (is l : List α), l ~ is ++ [] → (∃ is' x, l = is' ++ []) ∨ l ∈ permutationsAux [] is
simp
case inl.intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
case inl.intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
clear p
case inl.intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
is' : List α
p' : is' ~ t :: is
⊢ (∃ is'_1 x, is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
case inl.intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
subst e
case inl.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
is' : List α
p' : is' ~ t :: is
l₁ l₂ : List α
e : is' = l₁ ++ t :: l₂
⊢ (∃ is'_1 x, is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
case inl.intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
is' : List α
p' : is' ~ t :: is
⊢ (∃ is'_1 x, is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
rcases mem_split (p'.symm.subset (mem_cons_self _ _)) with ⟨l₁, l₂, e⟩
case inl.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
⊢ (∃ is' x, l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ permutations is ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
case inl.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
is' : List α
p' : is' ~ t :: is
l₁ l₂ : List α
e : is' = l₁ ++ t :: l₂
⊢ (∃ is'_1 x, is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
subst is'
case inl.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
⊢ (∃ is' x, l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ permutations is ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
case inl.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
⊢ (∃ is' x, l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ permutations is ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
have p := (perm_middle.symm.trans p').cons_inv
case inl.intro.intro.intro.intro.nil
α : Type uu
β : Type vv
l₁✝ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is' x, l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts

case inl.intro.intro.intro.intro.cons
α : Type uu
β : Type vv
l₁✝ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts
case inl.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
⊢ (∃ is' x, l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ permutations is ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
cases' l₂ with a l₂'
no goals
case inl.intro.intro.intro.intro.nil
α : Type uu
β : Type vv
l₁✝ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is' x, l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts
exact Or.inl ⟨l₁, by simpa using p⟩
no goals
α : Type uu
β : Type vv
l₁✝ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ ∃ x, l₁ ++ [t] ++ ts = l₁ ++ t :: ts
simpa using p
no goals
case inl.intro.intro.intro.intro.cons
α : Type uu
β : Type vv
l₁✝ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ permutationsAux ts (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts
exact Or.inr (Or.inr ⟨l₁, a :: l₂', mem_permutations_of_perm_lemma (IH2 _) p, by simp⟩)
no goals
α : Type uu
β : Type vv
l₁✝ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ a :: l₂' ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁ ++ t :: a :: l₂' ++ ts
simp
no goals
case inr
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ permutationsAux ts (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ permutationsAux is []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ permutationsAux ts (t :: is)
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ permutations is ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
exact Or.inr (Or.inl m)