awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw : (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
        is.permutations).length +
    is.length ! =
  ((t :: ts).length + is.length)!
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₁ : is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
  ((t :: ts).length + is.length)!
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₂ : is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
  ((t :: ts).length + is.length)!
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₃ : is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
  ((t :: ts).length + is.length)!
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₄ : is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
  (ts.length + 1 + is.length)!
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₇ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
  (ts.length + is.length + 1) * (ts.length + is.length)!
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
rw₇ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length + 1) * (ts.length + is.length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₈ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
  (ts.length + is.length)! * (ts.length + is.length + 1)
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
rw₇ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length + 1) * (ts.length + is.length)!
rw₈ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length + 1)
rw₉ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₁₀ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
rw₇ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length + 1) * (ts.length + is.length)!
rw₈ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length + 1)
rw₉ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw₁₀ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₁₁ : (ts.permutationsAux (t :: is)).length + is.length * is.length ! + is.length ! =
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
rw₇ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length + 1) * (ts.length + is.length)!
rw₈ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length + 1)
rw₉ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw₁₀ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
rw₁₁ :
  (ts.permutationsAux (t :: is)).length + is.length * is.length ! + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₁₂ : (ts.permutationsAux (t :: is)).length + (is.length * is.length ! + is.length !) =
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]