-- 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 swap'
α : Type u_1
a : α
l₁✝¹ l₂✝¹ r₁✝ r₂✝ s₁ s₂ : List α
x y : α
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₁ = y :: x :: l₁✝
e₂ : l₂ ++ a :: r₂ = x :: y :: l₂✝
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

Tactic:
obtain _ | ⟨y, _ | ⟨z, l₁⟩⟩ := l₁
  <;> obtain _ | ⟨u, _ | ⟨v, l₂⟩⟩ := l₂
  <;> dsimp at e₁ e₂ <;> injections <;> subst_vars
  <;> try exact p.cons _

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

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₂

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₂✝

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₂

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₂

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

Tactic:
obtain ⟨l₂, r₂, rfl⟩ := append_of_mem (a := a) (p₁.subset (by simp))

Result:
case trans.intro.intro
α : Type u_1
a : α
l₁✝ l₂✝¹ r₁✝ r₂✝¹ s₁ s₂ l₁ l₂✝ r₁ r₂✝ l₂ r₂ : 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
p₂ : l₂ ++ a :: r₂ ~ l₂✝ ++ a :: r₂✝
IH₂ :
  ∀ {l₁ l₂_1 r₁ r₂_1 : List α},
    l₁ ++ a :: r₁ = l₂ ++ a :: r₂ → l₂_1 ++ a :: r₂_1 = l₂✝ ++ a :: r₂✝ → l₁ ++ r₁ ~ l₂_1 ++ r₂_1
⊢ l₁ ++ r₁ ~ l₂✝ ++ r₂✝

Proof state:
case trans.intro.intro
α : Type u_1
a : α
l₁✝ l₂✝¹ r₁✝ r₂✝¹ s₁ s₂ l₁ l₂✝ r₁ r₂✝ l₂ r₂ : 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
p₂ : l₂ ++ a :: r₂ ~ l₂✝ ++ a :: r₂✝
IH₂ :
  ∀ {l₁ l₂_1 r₁ r₂_1 : List α},
    l₁ ++ a :: r₁ = l₂ ++ a :: r₂ → l₂_1 ++ a :: r₂_1 = l₂✝ ++ a :: r₂✝ → l₁ ++ r₁ ~ l₂_1 ++ r₂_1
⊢ l₁ ++ r₁ ~ l₂✝ ++ r₂✝

Tactic:
exact (IH₁ rfl rfl).trans (IH₂ rfl rfl)

Result:
no goals