awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s t : List α
x y : α
l : List α
⊢ flatMap (permutations'Aux y) (flatMap (permutations'Aux x) l.permutations') ~
    flatMap (permutations'Aux x) (flatMap (permutations'Aux y) l.permutations')
have swap : Perm (α := List α)
  (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux y) (permutations'Aux x x_1)) l.permutations')
  (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux x) (permutations'Aux y x_1)) l.permutations')
Tactic: rw [flatMap_assoc, flatMap_assoc]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s t : List α
x y : α
l : List α
⊢ Perm (α := List α)
    (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux y) (permutations'Aux x x_1)) l.permutations')
    (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux x) (permutations'Aux y x_1)) l.permutations')
have swap : ∀ (a : List α),
  a ∈ l.permutations' →
    flatMap (permutations'Aux y) (permutations'Aux x a) ~ flatMap (permutations'Aux x) (permutations'Aux y a)
Tactic: apply Perm.flatMap_left
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s t : List α
p : s ~ t
⊢ s.permutations' ~ t.permutations'
have nil : Perm.{u_1} (α := List α) (List.permutations' []) (List.permutations' [])
Tactic: induction p with
  | nil => simp
  | cons _ _ IH => exact IH.flatMap_right _
  | swap =>
    dsimp
    rw [flatMap_assoc, flatMap_assoc]
    apply Perm.flatMap_left
    intro l' _
    apply perm_permutations'Aux_comm
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s t : List α
p : s ~ t
nil : Perm.{u_1} (α := List α) (List.permutations' []) (List.permutations' [])
⊢ s.permutations' ~ t.permutations'
have cons : ∀ (x : α) {l₁ l₂ : List α},
  l₁ ~ l₂ → ∀ (IH : l₁.permutations' ~ l₂.permutations'), (x :: l₁).permutations' ~ (x :: l₂).permutations'
Tactic: induction p with
  | nil => simp
  | cons _ _ IH => exact IH.flatMap_right _
  | swap =>
    dsimp
    rw [flatMap_assoc, flatMap_assoc]
    apply Perm.flatMap_left
    intro l' _
    apply perm_permutations'Aux_comm
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s t : List α
p : s ~ t
nil : Perm.{u_1} (α := List α) (List.permutations' []) (List.permutations' [])
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ → ∀ (IH : l₁.permutations' ~ l₂.permutations'), (x :: l₁).permutations' ~ (x :: l₂).permutations'
⊢ s.permutations' ~ t.permutations'
have swap : ∀ (x y : α) (l : List α), (y :: x :: l).permutations' ~ (x :: y :: l).permutations'
Tactic: induction p with
  | nil => simp
  | cons _ _ IH => exact IH.flatMap_right _
  | swap =>
    dsimp
    rw [flatMap_assoc, flatMap_assoc]
    apply Perm.flatMap_left
    intro l' _
    apply perm_permutations'Aux_comm
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s t : List α
p : s ~ t
nil : Perm.{u_1} (α := List α) (List.permutations' []) (List.permutations' [])
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ → ∀ (IH : l₁.permutations' ~ l₂.permutations'), (x :: l₁).permutations' ~ (x :: l₂).permutations'
swap : ∀ (x y : α) (l : List α), (y :: x :: l).permutations' ~ (x :: y :: l).permutations'
⊢ s.permutations' ~ t.permutations'
have trans : ∀ {l₁ l₂ l₃ : List α},
  l₁ ~ l₂ →
    l₂ ~ l₃ →
      ∀ (IH₁ : l₁.permutations' ~ l₂.permutations') (IH₂ : l₂.permutations' ~ l₃.permutations'),
        l₁.permutations' ~ l₃.permutations'
Tactic: induction p with
  | nil => simp
  | cons _ _ IH => exact IH.flatMap_right _
  | swap =>
    dsimp
    rw [flatMap_assoc, flatMap_assoc]
    apply Perm.flatMap_left
    intro l' _
    apply perm_permutations'Aux_comm
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
ts : List α
⊢ ts.permutations ~ ts.permutations'
have obtain : ∀ (n : ℕ) (h : ts.length < n), ts.permutations ~ ts.permutations'
Tactic: obtain ⟨n, h⟩ : ∃ n, length ts < n := ⟨_, Nat.lt_succ_self _⟩
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
ts : List α
n : ℕ
h : ts.length < n
⊢ ts.permutations ~ ts.permutations'
have succ : ∀ (n : ℕ) (IH : ∀ (ts : List α) (h : ts.length < n), ts.permutations ~ ts.permutations') (ts : List α)
  (h : ts.length < n + 1), ts.permutations ~ ts.permutations'
Tactic: induction n generalizing ts with | zero => cases h | succ n IH => ?_
Cleared hypotheses: ts, n, h
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
have succ : length.{u_1} (α := α) [] < n + 1 → Perm.{u_1} (α := List α) (permutations []) (permutations' [])
Tactic: refine List.reverseRecOn ts (fun _ => ?_) (fun ts t _ h => ?_) h
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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' [])
⊢ ts.permutations ~ ts.permutations'
have succ₁ : ∀ (ts : List α) (t : α),
  (ts.length < n + 1 → ts.permutations ~ ts.permutations') →
    ∀ (h : (ts ++ [t]).length < n + 1), (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
Tactic: refine List.reverseRecOn ts (fun _ => ?_) (fun ts t _ h => ?_) h
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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 ++ [t]).permutations ~ (ts ++ [t]).permutations'
have h₁ : ts.length < n
Tactic: rw [← concat_eq_append, length_concat, Nat.succ_lt_succ_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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 ++ [t]).permutations ~ (ts ++ [t]).permutations'
have IH₂ : ts.reverse.permutations ~ ts.permutations'
Tactic: have IH₂ := (IH ts.reverse (by rwa [length_reverse])).trans (reverse_perm _).permutations'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
have 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'
Tactic: simp only [permutations_append, foldr_permutationsAux2, permutationsAux_nil,
    permutationsAux_cons, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
have 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'
Tactic: refine
    (perm_append_comm.trans ((IH₂.flatMap_right _).append ((IH _ h).map _))).trans
      (Perm.trans ?_ perm_append_comm.permutations')
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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')
      (map (fun (x : List α) ↦ x ++ [t]) ts.permutations') ~
    ([t] ++ ts).permutations'
have 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'
Tactic: rw [map_eq_flatMap, singleton_append, permutations']
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
have succ : flatMap (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' ~
  flatMap (permutations'Aux t) ts.permutations'
Tactic: refine (flatMap_append_perm _ _ _).trans ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
have succ : flatMap (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' =
  flatMap (permutations'Aux t) ts.permutations'
Tactic: refine Perm.of_eq ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
have succ : (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) = permutations'Aux t
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
⊢ (fun (x : List α) ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) = permutations'Aux t
have succ : ∀ (x : List α), (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]] = permutations'Aux t x
Tactic: funext _
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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 α
⊢ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]] = permutations'Aux t x
have succ : (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]] = (permutationsAux2 t [] [x ++ [t]] x id).snd
Tactic: rw [permutations'Aux_eq_permutationsAux2, permutationsAux2_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]] = permutations'Aux t x
have succ₁ : (permutationsAux2 t [] [x ++ [t]] x id).snd = (permutationsAux2 t [] [x ++ [t]] x id).snd
Tactic: rw [permutations'Aux_eq_permutationsAux2, permutationsAux2_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
x : α
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
have hn₁ : n = 0
Tactic: simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) n hn =
    (y :: s).insertIdx n x
have 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
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x (y :: s)) n hn =
    (y :: s).insertIdx n x
have 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
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
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
have 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
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 _ _
Cleared hypotheses: s, n, hn
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (permutations'Aux x s) n hn = s.insertIdx n x
have 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
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 _ _
Cleared hypotheses: s, n, hn
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List α → List α → Bool) List.beq fun (a b : List α) ↦ decide (a = b)
have h : ∀ (l₁ l₂ : List α), l₁.beq l₂ = decide (l₁ = l₂)
Tactic: funext l₁ l₂
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ == l₂) = decide (l₁ = l₂)
have h : (l₁ == l₂) = true ↔ decide (l₁ = l₂) = true
Tactic: rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
h : (l₁ == l₂) = true ↔ decide (l₁ = l₂) = true
⊢ (l₁ == l₂) = decide (l₁ = l₂)
have h₁ : l₁ = l₂ ↔ decide (l₁ = l₂) = true
Tactic: rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
h : (l₁ == l₂) = true ↔ decide (l₁ = l₂) = true
h₁ : l₁ = l₂ ↔ decide (l₁ = l₂) = true
⊢ (l₁ == l₂) = decide (l₁ = l₂)
have h₂ : l₁ = l₂ ↔ l₁ = l₂
Tactic: rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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 : α
⊢ count (x :: y :: l) (permutations'Aux x (y :: l)) = (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) (y :: l)).length + 1
have cons : 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 [permutations'Aux, count_cons_self]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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 : α
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) (y :: l)).length + 1
have 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
Tactic: by_cases hx : x = y
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) (y :: l)).length + 1
have 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
Tactic: by_cases hx : x = y
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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 =
    (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) (y :: l)).length + 1
have 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
Tactic: subst hx
Cleared hypotheses: y, hx
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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 =
    (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) (y :: l)).length + 1
have 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
Tactic: rw [takeWhile]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : 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
have nil : ∀ (x : α),
  count [x] (permutations'Aux x []) = length.{u_1} (α := α) (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) []) + 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]
Cleared hypotheses: l, x
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ count (x :: l) (permutations'Aux x l) = (takeWhile (fun (x_1 : α) ↦ decide (x = x_1)) l).length + 1
have 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
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]
Cleared hypotheses: l, x
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).length = s.length + 1
have nil : (permutations'Aux x []).length = length.{u_1} (α := α) [] + 1
Tactic: induction s with
  | nil => simp
  | cons y s IH => simpa using IH
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
nil : (permutations'Aux x []).length = length.{u_1} (α := α) [] + 1
⊢ (permutations'Aux x s).length = s.length + 1
have cons : ∀ (y : α) (s : List α) (IH : (permutations'Aux x s).length = s.length + 1),
  (permutations'Aux x (y :: s)).length = (y :: s).length + 1
Tactic: induction s with
  | nil => simp
  | cons y s IH => simpa using IH
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s = t
have a : Eq.{u_1 + 1} (α := List α) ((fun (l : List α) ↦ l.insertIdx s.length x) s)
  ((fun (l : List α) ↦ l.insertIdx s.length x) t)
Tactic: apply insertIdx_injective s.length x