-- Mathlib/Data/List/Permutation.lean
theorem perm_of_mem_permutationsAux :
    ∀ {ts is l : List α}, l ∈ permutationsAux ts is → l ~ ts ++ is

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

Tactic:
introv IH1 IH2 m

Result:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l : List α
m : l ∈ (t :: ts).permutationsAux is
⊢ l ~ t :: ts ++ is

Proof state:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l : List α
m : l ∈ (t :: ts).permutationsAux is
⊢ l ~ t :: ts ++ is

Tactic:
rw [permutationsAux_cons, permutations, mem_foldr_permutationsAux2] at m

Result:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l : List α
m :
  l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
⊢ l ~ t :: ts ++ is

Proof state:
α : Type u_1
⊢ ∀ {ts is l : List α}, l ∈ ts.permutationsAux is → l ~ ts ++ is

Tactic:
show ∀ (ts is l : List α), l ∈ permutationsAux ts is → l ~ ts ++ is

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

Proof state:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
⊢ l₁ ++ l₂ ~ is

Tactic:
simp only [mem_cons] at m

Result:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Proof state:
case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Tactic:
exact is.append_nil ▸ IH2 _ m

Result:
no goals

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

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

Result:
α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is) →
      (∀ l ∈ is.permutationsAux [], l ~ is ++ []) → ∀ l ∈ (t :: ts).permutationsAux is, l ~ t :: ts ++ is

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
p : l₁ ++ l₂ ~ is
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is

Tactic:
exact ((perm_middle.trans (p.cons _)).append_right _).trans (perm_append_comm.cons _)

Result:
no goals

Proof state:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l : List α
m : l ∈ ts.permutationsAux (t :: is)
⊢ l ~ t :: ts ++ is

Tactic:
exact (IH1 _ m).trans perm_middle

Result:
no goals

Proof state:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is

Tactic:
simp [e]

Result:
no goals

Proof state:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Tactic:
rcases m with e | m

Result:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is

case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

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

Tactic:
rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)

Result:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l : List α
m : l ∈ ts.permutationsAux (t :: is)
⊢ l ~ t :: ts ++ is

case inr.intro.intro.intro.intro
α : Type u_1
t : α
ts is : List α
IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is
IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is

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

Tactic:
simp

Result:
no goals