case intro
α : Type uu
β : Type vv
l₁ l₂ ts : List α
n : ℕ
h : length ts < n
⊢ permutations ts ~ permutations' ts
α : Type uu
β : Type vv
l₁ l₂ ts : List α
⊢ permutations ts ~ permutations' ts
obtain ⟨n, h⟩ : ∃ n, length ts < n := ⟨_, Nat.lt_succ_self _⟩
case intro.zero
α : Type uu
β : Type vv
l₁ l₂ ts✝ : List α
n : ℕ
h✝ : length ts✝ < n
ts : List α
h : length ts < zero
⊢ permutations ts ~ permutations' ts

case intro.succ
α : Type uu
β : Type vv
l₁ l₂ ts✝ : List α
n✝ : ℕ
h✝ : length ts✝ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts : List α
h : length ts < succ n
⊢ permutations ts ~ permutations' ts
case intro
α : Type uu
β : Type vv
l₁ l₂ ts : List α
n : ℕ
h : length ts < n
⊢ permutations ts ~ permutations' ts
induction' n with n IH generalizing ts
case intro.succ.refine'_1
α : Type uu
β : Type vv
l₁ l₂ ts✝ : List α
n✝ : ℕ
h✝ : length ts✝ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts : List α
h : length ts < succ n
x✝ : length [] < succ n
⊢ permutations [] ~ permutations' []

case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length (ts ++ [t]) < succ n
⊢ permutations (ts ++ [t]) ~ permutations' (ts ++ [t])
case intro.succ
α : Type uu
β : Type vv
l₁ l₂ ts✝ : List α
n✝ : ℕ
h✝ : length ts✝ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts : List α
h : length ts < succ n
⊢ permutations ts ~ permutations' ts
refine' List.reverseRecOn ts (fun _ => _) (fun ts t _ h => _) h
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
⊢ permutations (ts ++ [t]) ~ permutations' (ts ++ [t])
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length (ts ++ [t]) < succ n
⊢ permutations (ts ++ [t]) ~ permutations' (ts ++ [t])
rw [← concat_eq_append, length_concat, Nat.succ_lt_succ_iff] at h
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ permutations (ts ++ [t]) ~ permutations' (ts ++ [t])
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
⊢ permutations (ts ++ [t]) ~ permutations' (ts ++ [t])
have IH₂ := (IH ts.reverse (by rwa [length_reverse])).trans (reverse_perm _).permutations'
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (map (fun x => x ++ [t]) (permutations ts) ++
      List.bind (permutations (reverse ts)) fun y => (permutationsAux2 t [] [] y id).snd) ~
    permutations' (ts ++ [t])
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ permutations (ts ++ [t]) ~ permutations' (ts ++ [t])
simp only [permutations_append, foldr_permutationsAux2, permutationsAux_nil,
  permutationsAux_cons, append_nil]
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (List.bind (permutations' ts) fun y => (permutationsAux2 t [] [] y id).snd) ++
      map (fun x => x ++ [t]) (permutations' ts) ~
    permutations' ([t] ++ ts)
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (map (fun x => x ++ [t]) (permutations ts) ++
      List.bind (permutations (reverse ts)) fun y => (permutationsAux2 t [] [] y id).snd) ~
    permutations' (ts ++ [t])
refine'
  (perm_append_comm.trans ((IH₂.bind_right _).append ((IH _ h).map _))).trans
    (Perm.trans _ perm_append_comm.permutations')
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ ((List.bind (permutations' ts) fun y => (permutationsAux2 t [] [] y id).snd) ++
      List.bind (permutations' ts) fun x => [x ++ [t]]) ~
    List.bind (permutations' ts) (permutations'Aux t)
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (List.bind (permutations' ts) fun y => (permutationsAux2 t [] [] y id).snd) ++
      map (fun x => x ++ [t]) (permutations' ts) ~
    permutations' ([t] ++ ts)
rw [map_eq_bind, singleton_append, permutations']
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (List.bind (permutations' ts) fun x => (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ~
    List.bind (permutations' ts) (permutations'Aux t)
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ ((List.bind (permutations' ts) fun y => (permutationsAux2 t [] [] y id).snd) ++
      List.bind (permutations' ts) fun x => [x ++ [t]]) ~
    List.bind (permutations' ts) (permutations'Aux t)
refine' (bind_append_perm _ _ _).trans _
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (List.bind (permutations' ts) fun x => (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) =
    List.bind (permutations' ts) (permutations'Aux t)
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (List.bind (permutations' ts) fun x => (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ~
    List.bind (permutations' ts) (permutations'Aux t)
refine' Perm.of_eq _
case intro.succ.refine'_2.e_b
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (fun x => (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) = permutations'Aux t
case intro.succ.refine'_2
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (List.bind (permutations' ts) fun x => (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) =
    List.bind (permutations' ts) (permutations'Aux t)
congr
case intro.succ.refine'_2.e_b.h
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝¹ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ id).snd ++ [x✝ ++ [t]] = permutations'Aux t x✝
case intro.succ.refine'_2.e_b
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
⊢ (fun x => (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) = permutations'Aux t
funext _
no goals
case intro.succ.refine'_2.e_b.h
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝¹ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
IH₂ : permutations (reverse ts) ~ permutations' ts
x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ id).snd ++ [x✝ ++ [t]] = permutations'Aux t x✝
rw [permutations'Aux_eq_permutationsAux2, permutationsAux2_append]
no goals
case intro.zero
α : Type uu
β : Type vv
l₁ l₂ ts✝ : List α
n : ℕ
h✝ : length ts✝ < n
ts : List α
h : length ts < zero
⊢ permutations ts ~ permutations' ts
cases h
no goals
case intro.succ.refine'_1
α : Type uu
β : Type vv
l₁ l₂ ts✝ : List α
n✝ : ℕ
h✝ : length ts✝ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts : List α
h : length ts < succ n
x✝ : length [] < succ n
⊢ permutations [] ~ permutations' []
simp [permutations]
no goals
α : Type uu
β : Type vv
l₁ l₂ ts✝¹ : List α
n✝ : ℕ
h✝¹ : length ts✝¹ < n✝
n : ℕ
IH : ∀ (ts : List α), length ts < n → permutations ts ~ permutations' ts
ts✝ : List α
h✝ : length ts✝ < succ n
ts : List α
t : α
x✝ : length ts < succ n → permutations ts ~ permutations' ts
h : length ts < n
⊢ length (reverse ts) < n
rwa [length_reverse]