awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail fun (x : List α) ↦ f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
have cons : g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
  (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
Tactic: rw [ys_ih]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
cons :
  g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
cons₁ : List α' → β'
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail fun (x : List α) ↦ f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
have cons₂ : ∀ (a : List α), g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)
Tactic: rw [ys_ih]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
have cons : g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts))
Tactic: refine ⟨?_, rfl⟩
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts))
have cons : g' (f (t :: ys_hd :: (tail ++ ts))) = f' (map g (t :: ys_hd :: (tail ++ ts)))
Tactic: simp only [← map_cons, ← map_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd
have nil : ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
  map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd
Tactic: induction ys generalizing f f' with
  | nil => simp
  | cons ys_hd _ ys_ih =>
    simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
    rw [ys_ih]
    · refine ⟨?_, rfl⟩
      simp only [← map_cons, ← map_append]; apply H
    · intro a; apply H
Cleared hypotheses: ys, f, f', H
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
nil :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd
have cons : ∀ (ys_hd : α) (tail : List α)
  (ys_ih :
    ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
      map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd)
  (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
  map g' (permutationsAux2 t ts r (ys_hd :: tail) f).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail)) f').snd
Tactic: induction ys generalizing f f' with
  | nil => simp
  | cons ys_hd _ ys_ih =>
    simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
    rw [ys_ih]
    · refine ⟨?_, rfl⟩
      simp only [← map_cons, ← map_append]; apply H
    · intro a; apply H
Cleared hypotheses: ys, f, f', H
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ map f (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 t ts [] ys f).snd
have rw : (permutationsAux2 (id t) ts (map f []) ys f).snd = (permutationsAux2 t ts [] ys f).snd
Tactic: rw [map_permutationsAux2' id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
rw : (permutationsAux2 (id t) ts (map f []) ys f).snd = (permutationsAux2 t ts [] ys f).snd
f' : List α → β
⊢ map f (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 t ts [] ys f).snd
have H : ∀ (a : List α), f (id a) = f (map id a)
Tactic: rw [map_permutationsAux2' id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r ys f).snd = map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
have rw : (permutationsAux2 t ts [] ys f).snd ++ r =
  map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
Tactic: rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
rw :
  (permutationsAux2 t ts [] ys f).snd ++ r =
    map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
⊢ (permutationsAux2 t ts r ys f).snd = map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
have rw₁ : (permutationsAux2 t ts [] ys f).snd ++ r = Prod.snd (permutationsAux2 t [] [] ys fun (x : List α) ↦ f (x ++ ts)) ++ r
Tactic: rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
rw :
  (permutationsAux2 t ts [] ys f).snd ++ r =
    map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
rw₁ :
  (permutationsAux2 t ts [] ys f).snd ++ r = Prod.snd (permutationsAux2 t [] [] ys fun (x : List α) ↦ f (x ++ ts)) ++ r
⊢ (permutationsAux2 t ts r ys f).snd = map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
have rw₂ : (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts [] ys f).snd ++ r
Tactic: rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
have nil : map (map f) (permutations'Aux t []) = permutations'Aux (f t) (map f [])
Tactic: induction ts with
  | nil => rfl
  | cons a ts ih => simp only [permutations'Aux, map_cons, map_map, ← ih, Function.comp_def]
Cleared hypotheses: ts
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
nil : map (map f) (permutations'Aux t []) = permutations'Aux (f t) (map f [])
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
have cons : ∀ (a : α) (ts : List α) (ih : map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)),
  map (map f) (permutations'Aux t (a :: ts)) = permutations'Aux (f t) (map f (a :: ts))
Tactic: induction ts with
  | nil => rfl
  | cons a ts ih => simp only [permutations'Aux, map_cons, map_map, ← ih, Function.comp_def]
Cleared hypotheses: ts
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
have cons : ∀ (a : α) (ts : List α) (ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd),
  permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
Tactic: induction ts with | nil => rfl | cons a ts ih => ?_
Cleared hypotheses: ts
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
have cons : map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
  (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun (x : List α) ↦ a :: x).snd
Tactic: simp only [permutations'Aux, ih, cons_append, permutationsAux2_snd_cons, append_nil, id_eq,
    cons.injEq, true_and]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun (x : List α) ↦ a :: x).snd
have cons : map (cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
  Prod.snd (permutationsAux2 t [] [] ts fun (x : List α) ↦ a :: x) ++ [a :: (ts ++ [t])]
Tactic: simp +singlePass only [← permutationsAux2_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts ys l l' : List α
⊢ Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
have cons : ∀ (y : α) (ys : List α)
  (ih :
    ∀ {l : List α},
      Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
        ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts)
  {l : List α},
  Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (y :: ys) fun (x : List α) ↦ l ++ x)) l' ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
Tactic: induction ys generalizing l with
  | nil => simp +contextual
  | cons y ys ih => ?_
Cleared hypotheses: ys, l
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (y :: ys) fun (x : List α) ↦ l ++ x)) l' ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
have cons : (l' = l ++ (t :: y :: ys ++ ts) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
  ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
Tactic: rw [permutationsAux2_snd_cons,
    show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by simp, mem_cons, ih]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
have cons : (l' = l ++ (t :: y :: ys ++ ts) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
  ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
cons :
  (l' = l ++ (t :: y :: ys ++ ts) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
have cons₁ : (∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
  l' = l ++ (t :: y :: ys ++ ts) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: (l₁ ++ l₂)
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l_1 ++ x))
        (l ++ y' :: l₁ ++ t :: l₂ ++ ts) ↔
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α),
          l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ (l₁_1 : List α),
      ∃ (l₂_1 : List α),
        l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
have cons : ∀
  (ih :
    ∀ {l_1 : List α},
      Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (l₁ ++ l₂) fun (x : List α) ↦ l_1 ++ x))
          (l ++ y :: l₁ ++ t :: l₂ ++ ts) ↔
        ∃ (l₁_1 : List α),
          ∃ (l₂_1 : List α),
            l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts),
  l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: (l₁ ++ l₂) ++ ts) ∨
    ∃ (l₁_1 : List α),
      ∃ (l₂_1 : List α),
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
Tactic: rcases ye with ⟨rfl, rfl⟩
Cleared hypotheses: ys, y', ye, ih
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts ys l : List α
⊢ Eq.{u_1 + 1} (α := (a : List α) → List α) id fun (x : List α) ↦ [] ++ x
have h : ∀ (x : List α), id x = [] ++ x
Tactic: funext _
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd.length = ys.length
have nil : ∀ (f : List α → β), (permutationsAux2 t ts [] [] f).snd.length = length.{u_1} (α := α) []
Tactic: induction ys generalizing f
Cleared hypotheses: ys, f
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
nil : ∀ (f : List α → β), (permutationsAux2 t ts [] [] f).snd.length = length.{u_1} (α := α) []
⊢ (permutationsAux2 t ts [] ys f).snd.length = ys.length
have cons : ∀ (head : α) (tail : List α),
  (∀ (f : List α → β), (permutationsAux2 t ts [] tail f).snd.length = tail.length) →
    ∀ (f : List α → β), (permutationsAux2 t ts [] (head :: tail) f).snd.length = (head :: tail).length
Tactic: induction ys generalizing f
Cleared hypotheses: ys, f
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
have cons : (permutationsAux2 t ts (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L) l
      id).snd =
  flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
Tactic: simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
cons :
  (permutationsAux2 t ts (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L) l
        id).snd =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
have cons₁ : (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
  flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
Tactic: simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
cons :
  (permutationsAux2 t ts (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L) l
        id).snd =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
cons₁ :
  (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
have cons₂ : (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
  (permutationsAux2 t ts [] l id).snd ++ flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
Tactic: simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
cons :
  (permutationsAux2 t ts (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L) l
        id).snd =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
cons₁ :
  (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
cons₂ :
  (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
have cons₃ : (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
  (permutationsAux2 t ts [] l id).snd ++ (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r)
Tactic: simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
have nil : foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r [] =
  flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) [] ++ r
Tactic: induction L with
  | nil => rfl
  | cons l L ih => simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
nil :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r [] =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) [] ++ r
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
have cons : ∀ (l : List α) (L : List (List α))
  (ih :
    foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
      flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r),
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
Tactic: induction L with
  | nil => rfl
  | cons l L ih => simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]
Cleared hypotheses: L