-- Module: Mathlib.Data.List.Permutation
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
rw₁₂ :
  (ts.permutationsAux (t :: is)).length + (is.length * 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 + is.length !)
rw₁₄ rw₁₅ :
  (ts.permutationsAux (t :: is)).length + (is.length ! * is.length + is.length !) =
    (ts.permutationsAux (t :: is)).length + (is.length ! * is.length + is.length !)
⊢ ((t :: ts).permutationsAux 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]

Premises used: Nat.mul_succ, HMul.hMul, Nat.succ_eq_add_one, Nat.factorial_succ, List.length_foldr_permutationsAux2', List.permutationsAux_cons, List.permutations, Nat.mul_comm, List.Perm.length_eq, HAdd.hAdd, Nat.add_assoc, Nat.succ_add, OfNat.ofNat, List.length, List.perm_of_mem_permutations, Nat.add_comm