-- Mathlib/Data/List/Sym.lean
theorem Sublist.sym (n : ℕ) {xs ys : List α} (h : xs <+ ys) : xs.sym n <+ ys.sym n :=
  match n, h with
  | 0, _ => by simp [List.sym]
  | n + 1, .slnil => by simp only [refl]
  | n + 1, .cons a h => by
    rw [List.sym, ← nil_append (List.sym (n + 1) xs)]
    apply Sublist.append (nil_sublist _)
    exact h.sym (n + 1)
  | n + 1, .cons₂ a h => by
    rw [List.sym, List.sym]
    apply Sublist.append
    · exact ((cons₂ a h).sym n).map _
    · exact h.sym (n + 1)

Proof state:
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ List.sym (n + 1) (a :: l₁✝) <+ List.sym (n + 1) (a :: l₂✝)

Tactic:
rw [List.sym, List.sym]

Result:
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p => a ::ₛ p) (List.sym n (a :: l₁✝)) ++ List.sym (n + 1) l₁✝ <+
    map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝

Proof state:
α : Type u_1
n✝ : ℕ
xs ys : List α
h : xs <+ ys
n : ℕ
⊢ List.sym (n + 1) [] <+ List.sym (n + 1) []

Tactic:
simp only [refl]

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ List.sym (n + 1) xs <+ List.sym (n + 1) l₂✝

Tactic:
exact h.sym (n + 1)

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ List.sym (n + 1) xs <+ List.sym (n + 1) (a :: l₂✝)

Tactic:
rw [List.sym, ← nil_append (List.sym (n + 1) xs)]

Result:
α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ [] ++ List.sym (n + 1) xs <+ map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝

Proof state:
α : Type u_1
n : ℕ
xs✝ ys✝ : List α
h : xs✝ <+ ys✝
ys xs : List α
x✝ : xs <+ ys
⊢ List.sym 0 xs <+ List.sym 0 ys

Tactic:
simp [List.sym]

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ [] ++ List.sym (n + 1) xs <+ map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝

Tactic:
apply Sublist.append (nil_sublist _)

Result:
α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ List.sym (n + 1) xs <+ List.sym (n + 1) l₂✝

Proof state:
case hr
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ List.sym (n + 1) l₁✝ <+ List.sym (n + 1) l₂✝

Tactic:
exact h.sym (n + 1)

Result:
no goals

Proof state:
case hl
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p => a ::ₛ p) (List.sym n (a :: l₁✝)) <+ map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝))

Tactic:
exact ((cons₂ a h).sym n).map _

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p => a ::ₛ p) (List.sym n (a :: l₁✝)) ++ List.sym (n + 1) l₁✝ <+
    map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝

Tactic:
apply Sublist.append

Result:
case hl
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p => a ::ₛ p) (List.sym n (a :: l₁✝)) <+ map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝))

case hr
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ List.sym (n + 1) l₁✝ <+ List.sym (n + 1) l₂✝