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

case inr.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: permutationsAux is []
left✝ : l₂ ≠ []
e : l = l₁ ++ t :: l₂ ++ ts
⊢ l ~ t :: ts ++ is
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l : List α
m :
  l ∈ permutationsAux ts (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is :: permutationsAux is [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
⊢ l ~ t :: ts ++ is
rcases m with (m | ⟨l₁, l₂, m, _, e⟩)
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (is l : List α), l ∈ permutationsAux [] is → l ~ [] ++ is
simp
no goals
case inl
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l : List α
m : l ∈ permutationsAux ts (t :: is)
⊢ l ~ t :: ts ++ is
exact (IH1 _ m).trans perm_middle
case inr.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: permutationsAux is []
left✝ : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is
case inr.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: permutationsAux is []
left✝ : l₂ ≠ []
e : l = l₁ ++ t :: l₂ ++ ts
⊢ l ~ t :: ts ++ is
subst e
no goals
case inr.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: permutationsAux is []
left✝ : l₂ ≠ []
p : l₁ ++ l₂ ~ is
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is
exact ((perm_middle.trans (p.cons _)).append_right _).trans (perm_append_comm.cons _)
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ permutationsAux is []
⊢ l₁ ++ l₂ ~ is
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: permutationsAux is []
left✝ : l₂ ≠ []
⊢ l₁ ++ l₂ ~ is
simp [permutations] at m
case inl
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is

case inr
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ ∈ permutationsAux is []
⊢ l₁ ++ l₂ ~ is
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ permutationsAux is []
⊢ l₁ ++ l₂ ~ is
cases' m with e m
no goals
case inr
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ ∈ permutationsAux is []
⊢ l₁ ++ l₂ ~ is
exact is.append_nil ▸ IH2 _ m
no goals
case inl
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ permutationsAux ts (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ permutationsAux is [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is
simp [e]