case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ x : α
⊢ count [x] (permutations'Aux x []) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) []) + 1

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
⊢ count (x :: y :: l) (permutations'Aux x (y :: l)) =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
l : List α
x : α
⊢ count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
induction' l with y l IH generalizing x
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ x : α
⊢ count [x] (permutations'Aux x []) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) []) + 1
simp [takeWhile, count]
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
⊢ count (x :: y :: l) (permutations'Aux x (y :: l)) =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1
rw [permutations'Aux, DecEq_eq, count_cons_self]
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
hx : x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1
by_cases hx : x = y
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
⊢ count (x :: x :: l) (map (cons x) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (x :: l)) + 1
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
hx : x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1
subst hx
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
⊢ count (x :: x :: l) (map (cons x) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (x :: l)) + 1
simpa [takeWhile, Nat.succ_inj', DecEq_eq] using IH _
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length
        (match decide ((fun x x_1 => x = x_1) x y) with
        | true => y :: takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l
        | false => []) +
      1
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) (y :: l)) + 1
rw [takeWhile]
no goals
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x✝ y : α
l : List α
IH :
  ∀ (x : α),
    count (x :: l) (permutations'Aux x l) = length (takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length
        (match decide ((fun x x_1 => x = x_1) x y) with
        | true => y :: takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l
        | false => []) +
      1
simp only [mem_map, cons.injEq, Ne.symm hx, false_and, and_false, exists_false,
  not_false_iff, count_eq_zero_of_not_mem, zero_add, hx, decide_False, length_nil]