-- Mathlib/Data/List/Permutation.lean
theorem length_permutationsAux :
    ∀ ts is : List α, length (permutationsAux ts is) + is.length ! = (length ts + length is)!

Proof state:
α : 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 ! = (is.length + [].length)!
⊢ (is.permutationsAux []).length + 1 = is.length !

Tactic:
simpa using IH2

Result:
no goals

Proof state:
α : 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 ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Tactic:
simp only [length, factorial, Nat.mul_comm, add_eq] at IH1

Result:
α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
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)!

Proof state:
α : Type u_1
⊢ ∀ (is : List α), ([].permutationsAux is).length + is.length ! = ([].length + is.length)!

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ ∀ (ts is : List α), (ts.permutationsAux is).length + is.length ! = (ts.length + is.length)!

Tactic:
refine permutationsAux.rec (by simp) ?_

Result:
α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
      (is.permutationsAux []).length + [].length ! = (is.length + [].length)! →
        ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Proof state:
α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
      (is.permutationsAux []).length + [].length ! = (is.length + [].length)! →
        ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Tactic:
intro t ts is IH1 IH2

Result:
α : 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 ! = (is.length + [].length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Proof state:
α : 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 ! = (is.length + [].length)!
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Tactic:
have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2

Result:
α : 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 ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Proof state:
α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
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)!

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]

Result:
no goals