awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'

Tactic:
?_
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
n : ℕ
h : ts.length < n
succ :
  ∀ (n : ℕ) (IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations') (ts : List α)
    (h : ts.length < n + 1), ts.permutations ~ ts.permutations'
⊢ ts.permutations ~ ts.permutations'

Tactic:
induction n generalizing ts with | zero => cases h | succ n IH => ?_

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'

Tactic:
List.reverseRecOn ts (fun _ => ?_) (fun ts t _ h => ?_) h

Premises used: List.reverseRecOn
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
succ : length.{u_1} (α := α) [] < n + 1 → Perm.{u_1} (α := List α) (permutations []) (permutations' [])
succ₁ :
  ∀ (ts : List α) (t : α),
    (ts.length < n + 1 → ts.permutations ~ ts.permutations') →
      ∀ (h : (ts ++ [t]).length < n + 1), (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
⊢ ts.permutations ~ ts.permutations'

Tactic:
refine List.reverseRecOn ts (fun _ => ?_) (fun ts t _ h => ?_) h
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
h_1 : length.{u_1} (α := α) [] < n + 1
⊢ Perm.{u_1} (α := List α) (permutations []) (permutations' [])

Tactic:
simp [permutations]

Premises used: List.permutations
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : (ts ++ [t]).length < n + 1
⊢ ts.length < n

Tactic:
rw [← concat_eq_append, length_concat, Nat.succ_lt_succ_iff] at h

Premises used: Nat.succ_lt_succ_iff, List.concat_eq_append, List.length_concat
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h rwa rwa₁ rwa₂ rwa₃ : ts.length < n
⊢ ts.reverse.length < n

Tactic:
rwa [length_reverse]

Premises used: List.length_reverse
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
⊢ ts.reverse.permutations ~ ts.permutations'

Tactic:
have IH₂ := (IH ts.reverse (by rwa [length_reverse])).trans (reverse_perm _).permutations'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
succ :
  HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [t]) ts.permutations)
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.reverse.permutations) ~
    (ts ++ [t]).permutations'
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
simp only [permutations_append, foldr_permutationsAux2, permutationsAux_nil,
    permutationsAux_cons, append_nil]

Premises used: List.permutationsAux_nil, List.permutationsAux_cons, List.append_nil, List.permutations_append, List.foldr_permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [t]) ts.permutations)
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.reverse.permutations) ~
    (ts ++ [t]).permutations'

Tactic:
(perm_append_comm.trans ((IH₂.flatMap_right _).append ((IH _ h).map _))).trans
      (Perm.trans ?_ perm_append_comm.permutations')

Premises used: List.Perm.trans, List.perm_append_comm, List.Perm.append, List.Perm.flatMap_right, List.Perm.permutations', List.Perm.map
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
succ :
  HAppend.hAppend (α := List (List α))
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations')
      (map (fun (x : List α) ↦ x ++ [t]) ts.permutations') ~
    ([t] ++ ts).permutations'
⊢ HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [t]) ts.permutations)
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.reverse.permutations) ~
    (ts ++ [t]).permutations'

Tactic:
refine
    (perm_append_comm.trans ((IH₂.flatMap_right _).append ((IH _ h).map _))).trans
      (Perm.trans ?_ perm_append_comm.permutations')

Premises used: List.Perm.trans, List.perm_append_comm, List.Perm.append, List.Perm.flatMap_right, List.Perm.permutations', List.Perm.map
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
succ :
  HAppend.hAppend (α := List (List α))
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations')
      (flatMap (fun (x : List α) ↦ [x ++ [t]]) ts.permutations') ~
    flatMap (permutations'Aux t) ts.permutations'
⊢ HAppend.hAppend (α := List (List α))
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations')
      (map (fun (x : List α) ↦ x ++ [t]) ts.permutations') ~
    ([t] ++ ts).permutations'

Tactic:
rw [map_eq_flatMap, singleton_append, permutations']

Premises used: List.map_eq_flatMap, List.singleton_append, List.permutations'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ HAppend.hAppend (α := List (List α))
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations')
      (flatMap (fun (x : List α) ↦ [x ++ [t]]) ts.permutations') ~
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
(flatMap_append_perm _ _ _).trans ?_

Premises used: List.flatMap_append_perm, List.Perm.trans
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
succ :
  flatMap (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'
⊢ HAppend.hAppend (α := List (List α))
      (flatMap (fun (y : List α) ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations')
      (flatMap (fun (x : List α) ↦ [x ++ [t]]) ts.permutations') ~
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
refine (flatMap_append_perm _ _ _).trans ?_

Premises used: List.flatMap_append_perm, List.Perm.trans
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
Perm.of_eq ?_

Premises used: List.Perm.of_eq
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
succ :
  flatMap (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' =
    flatMap (permutations'Aux t) ts.permutations'
⊢ flatMap (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
refine Perm.of_eq ?_

Premises used: List.Perm.of_eq
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
succ : (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) = permutations'Aux t
⊢ flatMap (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' =
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
congr
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
succ : ∀ (x : List α), (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]] = permutations'Aux t x
⊢ (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) = permutations'Aux t

Tactic:
funext _
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
n : ℕ
IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations'
ts_1 : List α
h_1 : ts_1.length < n + 1
ts : List α
t : α
h_2 : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
x : List α
succ : (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]] = (permutationsAux2 t [] [x ++ [t]] x id).snd
succ₁ succ₂ : (permutationsAux2 t [] [x ++ [t]] x id).snd = (permutationsAux2 t [] [x ++ [t]] x id).snd
⊢ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]] = permutations'Aux t x

Tactic:
rw [permutations'Aux_eq_permutationsAux2, permutationsAux2_append]

Premises used: List.permutationsAux2_append, List.permutations'Aux_eq_permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
⊢ s ∈ t.permutations' ↔ s ~ t

Tactic:
(permutations_perm_permutations' _).symm.mem_iff.trans mem_permutations

Premises used: List.permutations_perm_permutations', List.mem_permutations, Iff.trans, List.Perm.symm, List.Perm.mem_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
h : s ~ t
⊢ s.permutations ~ t.permutations

Tactic:
(permutations_perm_permutations' _).trans <|
    h.permutations'.trans (permutations_perm_permutations' _).symm

Premises used: List.Perm.trans, List.permutations_perm_permutations', List.Perm.permutations', List.Perm.symm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
⊢ s.permutations ~ t.permutations ↔ s ~ t

Tactic:
⟨fun h => mem_permutations.1 <| h.mem_iff.1 <| mem_permutations.2 (Perm.refl _),
    Perm.permutations⟩

Premises used: Iff.mpr, List.Perm.refl, List.mem_permutations, Iff.intro, Iff.mp, List.Perm.permutations, List.Perm.mem_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
⊢ s.permutations' ~ t.permutations' ↔ s ~ t

Tactic:
⟨fun h => mem_permutations'.1 <| h.mem_iff.1 <| mem_permutations'.2 (Perm.refl _),
    Perm.permutations'⟩

Premises used: Iff.mpr, List.Perm.refl, List.mem_permutations', Iff.intro, Iff.mp, List.Perm.permutations', List.Perm.mem_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
n : ℕ
hn : n < (permutations'Aux x []).length
⊢ n = 0

Tactic:
simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn

Premises used: Nat.lt_one_iff, List.permutations'Aux, Nat.zero_add, List.length
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
n : ℕ
hn_1 : n < (permutations'Aux x []).length
hn : n = 0
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x []) n hn_1 = insertIdx [] n x

Tactic:
simp [hn]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH :
  ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x s) n hn = s.insertIdx n x
n : ℕ
hn : n < (permutations'Aux x (y :: s)).length
cons :
  ∀ (hn : 0 < (permutations'Aux x (y :: s)).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) 0 hn =
      (y :: s).insertIdx 0 x
cons₁ :
  ∀ (n : ℕ) (hn : n + 1 < (permutations'Aux x (y :: s)).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) (n + 1) hn =
      (y :: s).insertIdx (n + 1) x
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) n hn =
    (y :: s).insertIdx n x

Tactic:
cases n
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH :
  ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x s) n hn = s.insertIdx n x
hn : 0 < (permutations'Aux x (y :: s)).length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) 0 hn =
    (y :: s).insertIdx 0 x

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH :
  ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x s) n hn = s.insertIdx n x
n : ℕ
hn : n + 1 < (permutations'Aux x (y :: s)).length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) (n + 1) hn =
    (y :: s).insertIdx (n + 1) x

Tactic:
simpa [get] using IH _ _

Premises used: List.get
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
n : ℕ
hn : n < (permutations'Aux x s).length
nil :
  ∀ (n : ℕ) (hn : n < (permutations'Aux x []).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x []) n hn = insertIdx [] n x
cons :
  ∀ (y : α) (s : List α)
    (IH :
      ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length),
        getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x s) n hn =
          s.insertIdx n x)
    (n : ℕ) (hn : n < (permutations'Aux x (y :: s)).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) n hn =
      (y :: s).insertIdx n x
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x s) n hn = s.insertIdx n x

Tactic:
induction s generalizing n with
  | nil =>
    simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn
    simp [hn]
  | cons y s IH =>
    cases n
    · simp
    · simpa [get] using IH _ _

Premises used: List.get, List.cons, Nat.lt_one_iff, List.permutations'Aux, Nat.zero_add, List.length, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
n : ℕ
hn : n < (permutations'Aux x s).length
⊢ (permutations'Aux x s).get (⟨n, hn⟩ : Fin (permutations'Aux x s).length) = s.insertIdx n x

Tactic:
simp [getElem_permutations'Aux]

Premises used: List.getElem_permutations'Aux
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
inst : DecidableEq α
h : ∀ (l₁ l₂ : List α), l₁.beq l₂ = decide (l₁ = l₂)
⊢ Eq.{u_1 + 1} (α := List α → List α → Bool) List.beq fun (a b : List α) ↦ decide (a = b)

Tactic:
funext l₁ l₂
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
h : (l₁ == l₂) = true ↔ decide (l₁ = l₂) = true
h₁ : l₁ = l₂ ↔ decide (l₁ = l₂) = true
h₂ h₃ : l₁ = l₂ ↔ l₁ = l₂
⊢ (l₁ == l₂) = decide (l₁ = l₂)

Tactic:
rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]

Premises used: beq_iff_eq, Bool.eq_iff_iff, decide_eq_true_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
inst : DecidableEq α
x : α
⊢ count [x] (permutations'Aux x []) = length.{u_1} (α := α) (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) []) + 1

Tactic:
simp [takeWhile, count]

Premises used: List.count, List.takeWhile
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 : α
cons :
  count (x :: y :: l) (map (List.cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) (y :: l)).length + 1
⊢ 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]

Premises used: List.permutations'Aux, List.count_cons_self
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 : α
pos :
  ∀ (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
neg :
  ∀ (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
⊢ 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
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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
pos :
  count (x :: x :: l) (map (cons x) (permutations'Aux x l)) + 1 =
    (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) (x :: l)).length + 1
⊢ 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
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 _

Premises used: Nat.succ_inj, _private.0.List.DecEq_eq, List.takeWhile
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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
neg :
  count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    length.{u_1} (α := α)
        (match (motive := Bool → List α) decide (x = y) with
        | true => y :: takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) l
        | false => []) +
      1
⊢ 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]

Premises used: List.takeWhile
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 =
    length.{u_1} (α := α)
        (match (motive := Bool → List α) decide (x = y) with
        | true => y :: takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) l
        | false => []) +
      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]

Premises used: false_and, decide_false, Ne.symm, List.cons.injEq, exists_false, List.count_eq_zero_of_not_mem, and_false, Nat.zero_add, not_false_iff, List.mem_map, List.length_nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
nil :
  ∀ (x : α),
    count [x] (permutations'Aux x []) = length.{u_1} (α := α) (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) []) + 1
cons :
  ∀ (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
⊢ count (x :: l) (permutations'Aux x l) = (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) l).length + 1

Tactic:
induction l generalizing x with
  | nil => simp [takeWhile, count]
  | cons y l IH =>
    rw [permutations'Aux, count_cons_self]
    by_cases hx : x = y
    · subst hx
      simpa [takeWhile, Nat.succ_inj, DecEq_eq] using IH _
    · rw [takeWhile]
      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]

Premises used: Nat.succ_inj, false_and, decide_false, List.cons, List.cons.injEq, List.count, exists_false, List.permutations'Aux, List.count_eq_zero_of_not_mem, List.count_cons_self, _private.0.List.DecEq_eq, and_false, Nat.zero_add, not_false_iff, List.mem_map, List.takeWhile, List.length_nil, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
⊢ (permutations'Aux x []).length = length.{u_1} (α := α) [] + 1

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : (permutations'Aux x s).length = s.length + 1
⊢ (permutations'Aux x (y :: s)).length = (y :: s).length + 1

Tactic:
simpa using IH
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
nil : (permutations'Aux x []).length = length.{u_1} (α := α) [] + 1
cons :
  ∀ (y : α) (s : List α) (IH : (permutations'Aux x s).length = s.length + 1),
    (permutations'Aux x (y :: s)).length = (y :: s).length + 1
⊢ (permutations'Aux x s).length = s.length + 1

Tactic:
induction s with
  | nil => simp
  | cons y s IH => simpa using IH

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
a :
  Eq.{u_1 + 1} (α := List α) ((fun (l : List α) ↦ l.insertIdx s.length x) s)
    ((fun (l : List α) ↦ l.insertIdx s.length x) t)
⊢ s = t

Tactic:
apply insertIdx_injective s.length x

Premises used: List.insertIdx_injective, List.length
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s.length = t.length

Tactic:
simpa using congr_arg length h

Premises used: congr_arg, List.length