α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (t : α) (ts is : List α),
    length (permutationsAux ts (t :: is)) + (length (t :: is))! = (length ts + length (t :: is))! →
      length (permutationsAux is []) + (length [])! = (length is + length [])! →
        length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (ts is : List α), length (permutationsAux ts is) + (length is)! = (length ts + length is)!
refine' permutationsAux.rec (by simp) _
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : length (permutationsAux ts (t :: is)) + (length (t :: is))! = (length ts + length (t :: is))!
IH2 : length (permutationsAux is []) + (length [])! = (length is + length [])!
⊢ length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (t : α) (ts is : List α),
    length (permutationsAux ts (t :: is)) + (length (t :: is))! = (length ts + length (t :: is))! →
      length (permutationsAux is []) + (length [])! = (length is + length [])! →
        length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
intro t ts is IH1 IH2
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : length (permutationsAux ts (t :: is)) + (length (t :: is))! = (length ts + length (t :: is))!
IH2✝ : length (permutationsAux is []) + (length [])! = (length is + length [])!
IH2 : length (permutationsAux is []) + 1 = (length is)!
⊢ length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : length (permutationsAux ts (t :: is)) + (length (t :: is))! = (length ts + length (t :: is))!
IH2 : length (permutationsAux is []) + (length [])! = (length is + length [])!
⊢ length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH2✝ : length (permutationsAux is []) + (length [])! = (length is + length [])!
IH2 : length (permutationsAux is []) + 1 = (length is)!
IH1 :
  length (permutationsAux ts (t :: is)) + (length is)! * succ (length is) =
    (length ts + length is)! * succ (length ts + length is)
⊢ length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : length (permutationsAux ts (t :: is)) + (length (t :: is))! = (length ts + length (t :: is))!
IH2✝ : length (permutationsAux is []) + (length [])! = (length is + length [])!
IH2 : length (permutationsAux is []) + 1 = (length is)!
⊢ length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
simp [Nat.factorial, Nat.add_succ, mul_comm] at IH1
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH2✝ : length (permutationsAux is []) + (length [])! = (length is + length [])!
IH2 : length (permutationsAux is []) + 1 = (length is)!
IH1 :
  length (permutationsAux ts (t :: is)) + (length is)! * succ (length is) =
    (length ts + length is)! * succ (length ts + length is)
⊢ length (permutationsAux (t :: ts) is) + (length is)! = (length (t :: ts) + length is)!
rw [permutationsAux_cons,
  length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
  permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, mul_comm (_ + 1),
  ← Nat.succ_eq_add_one, ← IH1, add_comm (_ * _), add_assoc, Nat.mul_succ, mul_comm]
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
⊢ ∀ (is : List α), length (permutationsAux [] is) + (length is)! = (length [] + length is)!
simp
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
t : α
ts is : List α
IH1 : length (permutationsAux ts (t :: is)) + (length (t :: is))! = (length ts + length (t :: is))!
IH2 : length (permutationsAux is []) + (length [])! = (length is + length [])!
⊢ length (permutationsAux is []) + 1 = (length is)!
simpa using IH2