-- 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:
α : 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

Tactic:
rw [permutationsAux_cons, mem_foldr_permutationsAux2]

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 ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

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 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:
subst e

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 []
is' : List α
p' : is' ~ t :: is
⊢ (∃ is'_1, ∃ (_ : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ 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₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ ∃ (_ : l₁ ~ is), l₁ ++ [t] ++ ts = l₁ ++ t :: ts

Tactic:
simpa using p

Result:
no goals

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 []
is' : List α
p' : is' ~ t :: is
⊢ (∃ is'_1, ∃ (_ : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts

Tactic:
rcases append_of_mem (p'.symm.subset (mem_cons_self _ _)) with ⟨l₁, l₂, e⟩

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 []
is' : List α
p' : is' ~ t :: is
l₁ l₂ : List α
e : is' = l₁ ++ t :: l₂
⊢ (∃ is'_1, ∃ (_ : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts

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

Tactic:
show ∀ (ts is l : List α),
    l ~ is ++ ts → (∃ (is' : _) (_ : is' ~ is), l = is' ++ ts) ∨ l ∈ permutationsAux ts is

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

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 []
is' : List α
p' : is' ~ t :: is
l₁ l₂ : List α
e : is' = l₁ ++ t :: l₂
⊢ (∃ is'_1, ∃ (_ : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts

Tactic:
subst is'

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
⊢ (∃ 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:
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

Tactic:
exact Or.inl ⟨l₁, by simpa using p⟩

Result:
no goals

Proof state:
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

Tactic:
exact Or.inr (Or.inr ⟨l₁, a :: l₂', mem_permutations_of_perm_lemma (IH2 _) p, by simp⟩)

Result:
no goals

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

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

Result:
α : 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