-- Mathlib/Data/List/Permutation.lean
theorem mem_permutationsAux_of_perm :
    ∀ {ts is l : List α},
      l ~ is ++ ts → (∃ (is' : _) (_ : is' ~ is), l = is' ++ ts) ∨ l ∈ permutationsAux ts is

Proof state:
case inl.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
clear p

Result:
case inl.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Proof state:
α : Type u_1
⊢ ∀ (is l : List α), l ~ is ++ [] → (∃ is', ∃ (_ : is' ~ is), l = is' ++ []) ∨ l ∈ [].permutationsAux is

Tactic:
simp

Result:
no goals

Proof state:
case inl.intro.intro.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
⊢ (∃ is', ∃ (_ : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
have p := (perm_middle.symm.trans p').cons_inv

Result:
case inl.intro.intro.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
⊢ (∃ is', ∃ (_ : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts

Proof state:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ a :: l₂' ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁ ++ t :: a :: l₂' ++ ts

Tactic:
simp

Result:
no goals

Proof state:
case inl.intro.intro.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
⊢ (∃ is', ∃ (_ : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
rcases l₂ with - | ⟨a, l₂'⟩

Result:
case inl.intro.intro.intro.intro.nil
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is', ∃ (_ : is' ~ is), l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts

case inl.intro.intro.intro.intro.cons
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is', ∃ (_ : is' ~ is), l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts

Proof state:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
rcases IH1 _ (p.trans perm_middle) with (⟨is', p', e⟩ | m)

Result:
case inl.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

case inr
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Proof state:
α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (∀ (l : List α),
        l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
        ∀ (l : List α),
          l ~ is ++ t :: ts → (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is

Tactic:
intro t ts is IH1 IH2 l p

Result:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is