-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_inv_core {a : α} {l₁ l₂ r₁ r₂ : List α} :
    l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂

Proof state:
case cons.cons.cons
α : Type u_1
a : α
l₁ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ tail✝¹ : List α
head✝ : α
tail✝ : List α
p : tail✝¹ ++ a :: r₁ ~ tail✝ ++ a :: r₂
IH :
  ∀ {l₁ l₂ r₁_1 r₂_1 : List α},
    l₁ ++ a :: r₁_1 = tail✝¹ ++ a :: r₁ → l₂ ++ a :: r₂_1 = tail✝ ++ a :: r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ head✝ :: tail✝¹ ++ r₁ ~ head✝ :: tail✝ ++ r₂

Tactic:
exact (IH rfl rfl).cons _

Result:
no goals

Proof state:
case swap'.cons.cons.cons.cons
α : Type u_1
a : α
l₁✝ l₂✝ r₁✝ r₂✝ s₁ s₂ r₁ r₂ l₁ : List α
u v : α
l₂ : List α
p : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
IH :
  ∀ {l₁_1 l₂_1 r₁_1 r₂_1 : List α},
    l₁_1 ++ a :: r₁_1 = l₁ ++ a :: r₁ → l₂_1 ++ a :: r₂_1 = l₂ ++ a :: r₂ → l₁_1 ++ r₁_1 ~ l₂_1 ++ r₂_1
⊢ v :: u :: l₁ ++ r₁ ~ u :: v :: l₂ ++ r₂

Tactic:
exact (IH rfl rfl).swap' _ _

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l₁✝¹ l₂✝¹ r₁✝ r₂✝ s₁ s₂ : List α
x : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = l₁✝ → l₂ ++ a :: r₂ = l₂✝ → l₁ ++ r₁ ~ l₂ ++ r₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = x :: l₁✝
e₂ : l₂ ++ a :: r₂ = x :: l₂✝
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

Tactic:
cases l₁ <;> cases l₂ <;>
  dsimp at e₁ e₂ <;> injections <;> subst_vars

Result:
case cons.nil.nil
α : Type u_1
l₁ l₂ r₁✝ r₂✝ s₁ s₂ : List α
x : α
r₁ r₂ : List α
head_eq✝ : x = x
p : r₁ ~ r₂
IH : ∀ {l₁ l₂ r₁_1 r₂_1 : List α}, l₁ ++ x :: r₁_1 = r₁ → l₂ ++ x :: r₂_1 = r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ [] ++ r₁ ~ [] ++ r₂

case cons.nil.cons
α : Type u_1
l₁ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ : List α
head✝ : α
tail✝ : List α
p : r₁ ~ tail✝ ++ head✝ :: r₂
IH :
  ∀ {l₁ l₂ r₁_1 r₂_1 : List α},
    l₁ ++ head✝ :: r₁_1 = r₁ → l₂ ++ head✝ :: r₂_1 = tail✝ ++ head✝ :: r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ [] ++ r₁ ~ head✝ :: tail✝ ++ r₂

case cons.cons.nil
α : Type u_1
l₁ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ : List α
head✝ : α
tail✝ : List α
p : tail✝ ++ head✝ :: r₁ ~ r₂
IH :
  ∀ {l₁ l₂ r₁_1 r₂_1 : List α},
    l₁ ++ head✝ :: r₁_1 = tail✝ ++ head✝ :: r₁ → l₂ ++ head✝ :: r₂_1 = r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ head✝ :: tail✝ ++ r₁ ~ [] ++ r₂

case cons.cons.cons
α : Type u_1
a : α
l₁ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ tail✝¹ : List α
head✝ : α
tail✝ : List α
p : tail✝¹ ++ a :: r₁ ~ tail✝ ++ a :: r₂
IH :
  ∀ {l₁ l₂ r₁_1 r₂_1 : List α},
    l₁ ++ a :: r₁_1 = tail✝¹ ++ a :: r₁ → l₂ ++ a :: r₂_1 = tail✝ ++ a :: r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ head✝ :: tail✝¹ ++ r₁ ~ head✝ :: tail✝ ++ r₂

Proof state:
case cons.nil.nil
α : Type u_1
l₁ l₂ r₁✝ r₂✝ s₁ s₂ : List α
x : α
r₁ r₂ : List α
head_eq✝ : x = x
p : r₁ ~ r₂
IH : ∀ {l₁ l₂ r₁_1 r₂_1 : List α}, l₁ ++ x :: r₁_1 = r₁ → l₂ ++ x :: r₂_1 = r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ [] ++ r₁ ~ [] ++ r₂

Tactic:
exact p

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
l₁✝ l₂✝ r₁✝ r₂✝ s₁ s₂ l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = []
e₂ : l₂ ++ a :: r₂ = []
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

Tactic:
simp at e₁

Result:
no goals

Proof state:
case cons.cons.nil
α : Type u_1
l₁ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ : List α
head✝ : α
tail✝ : List α
p : tail✝ ++ head✝ :: r₁ ~ r₂
IH :
  ∀ {l₁ l₂ r₁_1 r₂_1 : List α},
    l₁ ++ head✝ :: r₁_1 = tail✝ ++ head✝ :: r₁ → l₂ ++ head✝ :: r₂_1 = r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ head✝ :: tail✝ ++ r₁ ~ [] ++ r₂

Tactic:
exact perm_middle.symm.trans p

Result:
no goals

Proof state:
case cons.nil.cons
α : Type u_1
l₁ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ : List α
head✝ : α
tail✝ : List α
p : r₁ ~ tail✝ ++ head✝ :: r₂
IH :
  ∀ {l₁ l₂ r₁_1 r₂_1 : List α},
    l₁ ++ head✝ :: r₁_1 = r₁ → l₂ ++ head✝ :: r₂_1 = tail✝ ++ head✝ :: r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ [] ++ r₁ ~ head✝ :: tail✝ ++ r₂

Tactic:
exact p.trans perm_middle

Result:
no goals

Proof state:
case trans
α : Type u_1
a : α
l₁✝¹ l₂✝¹ r₁✝ r₂✝ s₁ s₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
p₂ : l₂✝ ~ l₃✝
IH₁ : ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = l₁✝ → l₂ ++ a :: r₂ = l₂✝ → l₁ ++ r₁ ~ l₂ ++ r₂
IH₂ : ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = l₂✝ → l₂ ++ a :: r₂ = l₃✝ → l₁ ++ r₁ ~ l₂ ++ r₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = l₁✝
e₂ : l₂ ++ a :: r₂ = l₃✝
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

Tactic:
subst e₁ e₂

Result:
case trans
α : Type u_1
a : α
l₁✝ l₂✝¹ r₁✝ r₂✝ s₁ s₂ l₂✝ l₁ l₂ r₁ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ l₂✝
IH₁ : ∀ {l₁_1 l₂ r₁_1 r₂ : List α}, l₁_1 ++ a :: r₁_1 = l₁ ++ a :: r₁ → l₂ ++ a :: r₂ = l₂✝ → l₁_1 ++ r₁_1 ~ l₂ ++ r₂
p₂ : l₂✝ ~ l₂ ++ a :: r₂
IH₂ : ∀ {l₁ l₂_1 r₁ r₂_1 : List α}, l₁ ++ a :: r₁ = l₂✝ → l₂_1 ++ a :: r₂_1 = l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂_1 ++ r₂_1
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

Proof state:
α : Type u_1
a : α
l₁ l₂ r₁ r₂ : List α
⊢ ∀ (s₁ s₂ : List α), s₁ ~ s₂ → ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂

Tactic:
intro s₁ s₂ p

Result:
α : Type u_1
a : α
l₁ l₂ r₁ r₂ s₁ s₂ : List α
p : s₁ ~ s₂
⊢ ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂

Proof state:
case swap'.nil.cons.cons
α : Type u_1
l₁ l₂✝ r₁ r₂✝ s₁ s₂ l₁✝ r₂ : List α
u v : α
l₂ : List α
p : l₁✝ ~ l₂ ++ v :: r₂
IH : ∀ {l₁ l₂_1 r₁ r₂_1 : List α}, l₁ ++ v :: r₁ = l₁✝ → l₂_1 ++ v :: r₂_1 = l₂ ++ v :: r₂ → l₁ ++ r₁ ~ l₂_1 ++ r₂_1
⊢ [] ++ u :: l₁✝ ~ u :: v :: l₂ ++ r₂

Tactic:
exact (p.trans perm_middle).cons u

Result:
no goals

Proof state:
case swap'.cons.cons.cons.nil
α : Type u_1
l₁✝ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ : List α
y : α
l₁ : List α
u : α
p : l₁ ++ y :: r₁ ~ r₂
IH :
  ∀ {l₁_1 l₂ r₁_1 r₂_1 : List α}, l₁_1 ++ y :: r₁_1 = l₁ ++ y :: r₁ → l₂ ++ y :: r₂_1 = r₂ → l₁_1 ++ r₁_1 ~ l₂ ++ r₂_1
⊢ y :: u :: l₁ ++ r₁ ~ [u] ++ r₂

Tactic:
exact (swap _ _ _).trans ((perm_middle.symm.trans p).cons u)

Result:
no goals

Proof state:
case swap'.cons.cons.nil
α : Type u_1
l₁✝ l₂ r₁✝ r₂ s₁ s₂ l₂✝ r₁ : List α
y z : α
l₁ : List α
p : l₁ ++ z :: r₁ ~ l₂✝
IH : ∀ {l₁_1 l₂ r₁_1 r₂ : List α}, l₁_1 ++ z :: r₁_1 = l₁ ++ z :: r₁ → l₂ ++ z :: r₂ = l₂✝ → l₁_1 ++ r₁_1 ~ l₂ ++ r₂
⊢ y :: z :: l₁ ++ r₁ ~ [] ++ y :: l₂✝

Tactic:
exact (perm_middle.symm.trans p).cons y

Result:
no goals

Proof state:
α : Type u_1
a : α
l₁✝ l₂✝¹ r₁✝ r₂✝ s₁ s₂ l₂✝ l₁ l₂ r₁ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ l₂✝
IH₁ : ∀ {l₁_1 l₂ r₁_1 r₂ : List α}, l₁_1 ++ a :: r₁_1 = l₁ ++ a :: r₁ → l₂ ++ a :: r₂ = l₂✝ → l₁_1 ++ r₁_1 ~ l₂ ++ r₂
p₂ : l₂✝ ~ l₂ ++ a :: r₂
IH₂ : ∀ {l₁ l₂_1 r₁ r₂_1 : List α}, l₁ ++ a :: r₁ = l₂✝ → l₂_1 ++ a :: r₂_1 = l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂_1 ++ r₂_1
⊢ a ∈ l₁ ++ a :: r₁

Tactic:
simp

Result:
no goals

Proof state:
case swap'.cons.nil.cons.nil
α : Type u_1
l₁ l₂ r₁✝ r₂✝ s₁ s₂ r₁ r₂ : List α
u : α
p : r₁ ~ r₂
IH : ∀ {l₁ l₂ r₁_1 r₂_1 : List α}, l₁ ++ u :: r₁_1 = r₁ → l₂ ++ u :: r₂_1 = r₂ → l₁ ++ r₁_1 ~ l₂ ++ r₂_1
⊢ [u] ++ r₁ ~ [u] ++ r₂

Tactic:
exact p.cons _

Result:
no goals

Proof state:
case swap'.cons.nil.cons.cons
α : Type u_1
l₁ l₂✝ r₁✝ r₂✝ s₁ s₂ r₁ r₂ : List α
u v : α
l₂ : List α
p : r₁ ~ l₂ ++ u :: r₂
IH :
  ∀ {l₁ l₂_1 r₁_1 r₂_1 : List α}, l₁ ++ u :: r₁_1 = r₁ → l₂_1 ++ u :: r₂_1 = l₂ ++ u :: r₂ → l₁ ++ r₁_1 ~ l₂_1 ++ r₂_1
⊢ [v] ++ r₁ ~ u :: v :: l₂ ++ r₂

Tactic:
exact ((p.trans perm_middle).cons _).trans (swap _ _ _)

Result:
no goals