-- Mathlib/Data/List/Permutation.lean
theorem count_permutations'Aux_self [DecidableEq α] (l : List α) (x : α) :
    count (x :: l) (permutations'Aux x l) = length (takeWhile (x = ·) l) + 1

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1

Tactic:
rw [takeWhile]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (match decide (x = y) with
        | true => y :: takeWhile (fun x_1 => decide (x = x_1)) l
        | false => []).length +
      1

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: x :: l) (map (cons x) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (x :: l)).length + 1

Tactic:
simpa [takeWhile, Nat.succ_inj', DecEq_eq] using IH _

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ count [x] (permutations'Aux x []) = (takeWhile (fun x_1 => decide (x = x_1)) []).length + 1

Tactic:
simp [takeWhile, count]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (match decide (x = y) with
        | true => y :: takeWhile (fun x_1 => decide (x = x_1)) l
        | false => []).length +
      1

Tactic:
simp only [mem_map, cons.injEq, Ne.symm hx, false_and, and_false, exists_false,
  not_false_iff, count_eq_zero_of_not_mem, Nat.zero_add, hx, decide_false, length_nil]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) (permutations'Aux x (y :: l)) = (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1

Tactic:
rw [permutations'Aux, count_cons_self]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
hx : x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1

Tactic:
subst hx

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: x :: l) (map (cons x) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (x :: l)).length + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
⊢ count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1

Tactic:
induction' l with y l IH generalizing x

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ count [x] (permutations'Aux x []) = (takeWhile (fun x_1 => decide (x = x_1)) []).length + 1

case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) (permutations'Aux x (y :: l)) = (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1

Tactic:
by_cases hx : x = y

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
hx : x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1

case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 => decide (x = x_1)) (y :: l)).length + 1