awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
⊢ l' ∈ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
have this : (∃ (a : List α), a ∈ L ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
  ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
Tactic: have :
    (∃ a : List α,
        a ∈ L ∧ ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
      ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts) :=
    ⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ =>
      ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ (a : List α), a ∈ L ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
have rw : l' ∈ flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r ↔
  l' ∈ r ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
Tactic: rw [foldr_permutationsAux2]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
⊢ (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L).length =
    n * L.length + r.length
have rw : (map length L).sum = n * L.length
Tactic: rw [length_foldr_permutationsAux2, (_ : (map length L).sum = n * length L)]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : ∀ (H : ∀ (l : List α), l ∈ L → l.length = n), (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length
have sum_map : (map length L).sum = n * L.length
Tactic: have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : ∀ (H : ∀ (l : List α), l ∈ L → l.length = n), (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
sum_map : (map length L).sum = n * L.length
⊢ (map length (l :: L)).sum = n * (l :: L).length
have length_l : l.length = n
Tactic: have length_l : length l = n := H _ mem_cons_self
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
⊢ (map length L).sum = n * L.length
have nil : ∀ (H : ∀ (l : List α), Membership.mem (γ := List (List α)) [] l → l.length = n),
  (map.{u_1, 0} (α := List α) length []).sum = n * length.{u_1} (α := List α) []
Tactic: induction L with
  | nil => simp
  | cons l L ih =>
    have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
    have length_l : length l = n := H _ mem_cons_self
    simp [sum_map, length_l, Nat.add_comm, mul_succ]
Cleared hypotheses: L, H
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
nil :
  ∀ (H : ∀ (l : List α), Membership.mem (γ := List (List α)) [] l → l.length = n),
    (map.{u_1, 0} (α := List α) length []).sum = n * length.{u_1} (α := List α) []
⊢ (map length L).sum = n * L.length
have cons : ∀ (l : List α) (L : List (List α))
  (ih : ∀ (H : ∀ (l : List α), l ∈ L → l.length = n), (map length L).sum = n * L.length)
  (H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n), (map length (l :: L)).sum = n * (l :: L).length
Tactic: induction L with
  | nil => simp
  | cons l L ih =>
    have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
    have length_l : length l = n := H _ mem_cons_self
    simp [sum_map, length_l, Nat.add_comm, mul_succ]
Cleared hypotheses: L, H
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
is : List α
⊢ permutationsAux [] is = []
have rw : Eq (α := List (List α))
  (permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
      (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
        foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
      [] is :
    List (List α))
  ([] : List (List α))
Tactic: rw [permutationsAux, permutationsAux.rec]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
is : List α
rw :
  Eq (α := List (List α))
    (permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
        (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
          foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
        [] is :
      List (List α))
    ([] : List (List α))
⊢ permutationsAux [] is = []
have rw₁ : Eq.{u_1 + 1} (α := List (List α)) [] []
Tactic: rw [permutationsAux, permutationsAux.rec]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
⊢ (t :: ts).permutationsAux is =
    foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
      is.permutations
have rw : foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd)
    (permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
      (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
        foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
      ts (t :: is))
    (is ::
      permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
        (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
          foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
        is []) =
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
    is.permutations
Tactic: rw [permutationsAux, permutationsAux.rec]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List (List α)) (permutations []) [[]]
have rw : Eq.{u_1 + 1} (α := List (List α)) ([] :: permutationsAux [] []) [[]]
Tactic: rw [permutations, permutationsAux_nil]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := List (List α)) ([] :: permutationsAux [] []) [[]]
⊢ Eq.{u_1 + 1} (α := List (List α)) (permutations []) [[]]
have rw₁ : Eq.{u_1 + 1} (α := List (List α)) [[]] [[]]
Tactic: rw [permutations, permutationsAux_nil]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (ts is : List α), map (map f) (ts.permutationsAux is) = (map f ts).permutationsAux (map f is)
have refine : ∀ (t : α) (ts is : List α),
  map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is)) →
    map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f []) →
      map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
Tactic: refine permutationsAux.rec (by simp) ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f [])
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
have IH2₁ : map (map f) (is.permutationsAux []) = (map f is).permutationsAux []
Tactic: rw [map] at IH2
Cleared hypotheses: IH2
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) ts.permutations = (map f ts).permutations
have rw : map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations
Tactic: rw [permutations, permutations, map, map_permutationsAux, map]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
rw : map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations
⊢ map (map f) ts.permutations = (map f ts).permutations
have rw₁ : map (map f) (ts :: ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
Tactic: rw [permutations, permutations, map, map_permutationsAux, map]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
rw : map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations
rw₁ : map (map f) (ts :: ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
⊢ map (map f) ts.permutations = (map f ts).permutations
have rw₂ : map f ts :: map (map f) (ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
Tactic: rw [permutations, permutations, map, map_permutationsAux, map]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
rw : map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations
rw₁ : map (map f) (ts :: ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
rw₂ : map f ts :: map (map f) (ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
⊢ map (map f) ts.permutations = (map f ts).permutations
have rw₃ : map f ts :: (map f ts).permutationsAux (map f []) = map f ts :: (map f ts).permutationsAux []
Tactic: rw [permutations, permutations, map, map_permutationsAux, map]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
rw : map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations
rw₁ : map (map f) (ts :: ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
rw₂ : map f ts :: map (map f) (ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
rw₃ : map f ts :: (map f ts).permutationsAux (map f []) = map f ts :: (map f ts).permutationsAux []
⊢ map (map f) ts.permutations = (map f ts).permutations
have rw₄ : map f ts :: (map f ts).permutationsAux [] = map f ts :: (map f ts).permutationsAux []
Tactic: rw [permutations, permutations, map, map_permutationsAux, map]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) ts.permutations' = (map f ts).permutations'
have nil : map (map f) (permutations' []) = (map f []).permutations'
Tactic: induction ts with
  | nil => rfl
  | cons t ts ih => simp [← ih, map_flatMap, ← map_map_permutations'Aux, flatMap_map]
Cleared hypotheses: ts
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
nil : map (map f) (permutations' []) = (map f []).permutations'
⊢ map (map f) ts.permutations' = (map f ts).permutations'
have cons : ∀ (t : α) (ts : List α) (ih : map (map f) ts.permutations' = (map f ts).permutations'),
  map (map f) (t :: ts).permutations' = (map f (t :: ts)).permutations'
Tactic: induction ts with
  | nil => rfl
  | cons t ts ih => simp [← ih, map_flatMap, ← map_map_permutations'Aux, flatMap_map]
Cleared hypotheses: ts
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (t :: is ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')
have cons : flatMap (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd) is'.permutations ++
    (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: is')) =
  flatMap (fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd) is'.permutations ++
    (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++
      ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))
Tactic: simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
    reverse_cons, append_assoc]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ flatMap (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd) is'.permutations ++
      (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++
        ts.permutationsAux (is.reverse ++ t :: is')) =
    flatMap (fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd)
        is'.permutations ++
      (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++
        ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))
have cons : Eq.{u_1 + 1} (α := List α → List (List α)) (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd)
  fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ Eq.{u_1 + 1} (α := List α → List (List α)) (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd)
    fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd
have cons : ∀ (x : List α),
  (permutationsAux2 t (is ++ ts) [] x id).snd = map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] x id).snd
Tactic: funext _
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x : List α
⊢ (permutationsAux2 t (is ++ ts) [] x id).snd = map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] x id).snd
have cons : (permutationsAux2 t (is ++ ts) [] x id).snd = Prod.snd (permutationsAux2 t is [] x fun (x : List α) ↦ x ++ ts)
Tactic: rw [map_permutationsAux2]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x : List α
⊢ (permutationsAux2 t (is ++ ts) [] x id).snd = Prod.snd (permutationsAux2 t is [] x fun (x : List α) ↦ x ++ ts)
have cons : Eq (α := List (List α)) (Prod.snd (permutationsAux2 t [] [] x fun (x : List α) ↦ id (x ++ (is ++ ts))))
  (Prod.snd (permutationsAux2 t [] [] x fun (x : List α) ↦ x ++ is ++ ts))
Tactic: simp +singlePass only [← permutationsAux2_comp_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
is is' ts : List α
⊢ (is ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
have nil : ∀ (is' : List α),
  ([] ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ x ++ ts) (permutationsAux [] is') ++ ts.permutationsAux (reverse [] ++ is')
Tactic: induction is generalizing is' with | nil => simp | cons t is ih =>
  simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
    reverse_cons, append_assoc]
  congr 2
  funext _
  rw [map_permutationsAux2]
  simp +singlePass only [← permutationsAux2_comp_append]
  simp only [id, append_assoc]
Cleared hypotheses: is, is'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
is is' ts : List α
nil :
  ∀ (is' : List α),
    ([] ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (permutationsAux [] is') ++ ts.permutationsAux (reverse [] ++ is')
⊢ (is ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
have cons : ∀ (t : α) (is : List α)
  (ih :
    ∀ (is' : List α),
      (is ++ ts).permutationsAux is' =
        map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is'))
  (is' : List α),
  (t :: is ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')
Tactic: induction is generalizing is' with | nil => simp | cons t is ih =>
  simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
    reverse_cons, append_assoc]
  congr 2
  funext _
  rw [map_permutationsAux2]
  simp +singlePass only [← permutationsAux2_comp_append]
  simp only [id, append_assoc]
Cleared hypotheses: is, is'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
⊢ ∀ (ts is l : List α), l ∈ ts.permutationsAux is → l ~ ts ++ is
have refine : ∀ (t : α) (ts is : List α),
  (∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is) →
    (∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []) →
      ∀ (l : List α), l ∈ (t :: ts).permutationsAux is → l ~ t :: ts ++ is
Tactic: refine permutationsAux.rec (by simp) ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ (t :: ts).permutationsAux is
⊢ l ~ t :: ts ++ is
have m₁ : l ∈ ts.permutationsAux (t :: is) ∨
  ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Tactic: rw [permutationsAux_cons, permutations, mem_foldr_permutationsAux2] at m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m :
  l ∈ ts.permutationsAux (t :: is) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
⊢ l ~ t :: ts ++ is
have inl : ∀ (m : l ∈ ts.permutationsAux (t :: is)), l ~ t :: ts ++ is
Tactic: rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m :
  l ∈ ts.permutationsAux (t :: is) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
inl : ∀ (m : l ∈ ts.permutationsAux (t :: is)), l ~ t :: ts ++ is
⊢ l ~ t :: ts ++ is
have inr : ∀ (l₁ l₂ : List α) (m : l₁ ++ l₂ ∈ is :: is.permutationsAux []), l₂ ≠ [] → l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is
Tactic: rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)
Cleared hypotheses: l, m
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left : l₂ ≠ []
⊢ l₁ ++ l₂ ~ is
have m₁ : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ is.permutationsAux []
Tactic: simp only [mem_cons] at m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left : l₂ ≠ []
m : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is
have inl : ∀ (e : l₁ ++ l₂ = is), l₁ ++ l₂ ~ is
Tactic: rcases m with e | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left : l₂ ≠ []
m : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ is.permutationsAux []
inl : ∀ (e : l₁ ++ l₂ = is), l₁ ++ l₂ ~ is
⊢ l₁ ++ l₂ ~ is
have inr : ∀ (m : l₁ ++ l₂ ∈ is.permutationsAux []), l₁ ++ l₂ ~ is
Tactic: rcases m with e | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is
have p : l₁ ++ l₂ ~ is
Tactic: have p : l₁ ++ l₂ ~ is := by
      simp only [mem_cons] at m
      rcases m with e | m
      · simp [e]
      exact is.append_nil ▸ IH2 _ m
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
⊢ ∀ (ts is : List α), (ts.permutationsAux is).length + is.length ! = (ts.length + is.length)!
have refine : ∀ (t : α) (ts is : List α),
  (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
    (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])! →
      ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
Tactic: refine permutationsAux.rec (by simp) ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)!
IH2 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have IH2₁ : (is.permutationsAux []).length + 1 = is.length !
Tactic: have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)!
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have IH1₁ : (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
  (ts.length + is.length)! * (ts.length + is.length).succ
Tactic: simp only [factorial, Nat.mul_comm, add_eq] at IH1
Cleared hypotheses: IH1