-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem mergeSort_cons {le : α → α → Bool}
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a)
    (a : α) (l : List α) :
    ∃ l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ ∧ mergeSort l le = l₁ ++ l₂ ∧
      ∀ b, b ∈ l₁ → !le a b

Proof state:
case intro.intro.refine_2.e_a.x
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
p : l₁ ++ (a, 0) :: l₂ ~ (a :: l).zipIdx
q : (l.zipIdx 1).mergeSort (zipIdxLE le) ~ l₁ ++ l₂
⊢ Pairwise (fun a b => zipIdxLE le a b = true) ((l.zipIdx 1).mergeSort (zipIdxLE le))

Tactic:
exact sorted_mergeSort (zipIdxLE_trans trans) (zipIdxLE_total total) ..

Result:
no goals

Proof state:
case intro.intro.refine_3
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
p : l₁ ++ (a, 0) :: l₂ ~ (a :: l).zipIdx
⊢ ∀ (b : α), b ∈ map (fun x => x.fst) l₁ → (!le a b) = true

Tactic:
intro b m

Result:
case intro.intro.refine_3
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
p : l₁ ++ (a, 0) :: l₂ ~ (a :: l).zipIdx
b : α
m : b ∈ map (fun x => x.fst) l₁
⊢ (!le a b) = true

Proof state:
case intro.intro.refine_2.e_a.x
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
p : l₁ ++ (a, 0) :: l₂ ~ (a :: l).zipIdx
q : (l.zipIdx 1).mergeSort (zipIdxLE le) ~ l₁ ++ l₂
⊢ (l.zipIdx 1).mergeSort (zipIdxLE le) ~ l₁ ++ l₂

Tactic:
exact q

Result:
no goals

Proof state:
case intro.intro.refine_3.intro.intro.intro
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
j : α
w✝ : Nat
m : (j, w✝) ∈ l₁
p : map (fun x => x.snd) (l₁ ++ (a, 0) :: l₂) ~ map (fun x => x.snd) (a :: l).zipIdx
nd' : (map (fun x => x.snd) l₁ ++ map (fun x => x.snd) ((a, 0) :: l₂)).Nodup
j0 : ¬w✝ = 0
r : zipIdxLE le (j, w✝) (a, 0) = true
⊢ (!le a j) = true

Tactic:
simp_all [zipIdxLE]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
p : (a :: l).zipIdx.mergeSort (zipIdxLE le) ~ (a :: l).zipIdx
⊢ ∃ l₁ l₂,
    map (fun x => x.fst) (((a, 0) :: l.zipIdx (0 + 1)).mergeSort (zipIdxLE le)) = l₁ ++ a :: l₂ ∧
      l.mergeSort le = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true

Tactic:
rw [h] at p

Result:
case intro.intro
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
p : l₁ ++ (a, 0) :: l₂ ~ (a :: l).zipIdx
⊢ ∃ l₁ l₂,
    map (fun x => x.fst) (((a, 0) :: l.zipIdx (0 + 1)).mergeSort (zipIdxLE le)) = l₁ ++ a :: l₂ ∧
      l.mergeSort le = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true

Proof state:
case intro.intro
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
⊢ ∃ l₁ l₂,
    map (fun x => x.fst) (((a, 0) :: l.zipIdx (0 + 1)).mergeSort (zipIdxLE le)) = l₁ ++ a :: l₂ ∧
      l.mergeSort le = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true

Tactic:
have p := mergeSort_perm ((a :: l).zipIdx) (zipIdxLE le)

Result:
case intro.intro
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
l : List α
nd : (map (fun x => x.snd) (a :: l).zipIdx).Nodup
m₁ : (a, 0) ∈ (a :: l).zipIdx.mergeSort (zipIdxLE le)
l₁ l₂ : List (α × Nat)
h : (a :: l).zipIdx.mergeSort (zipIdxLE le) = l₁ ++ (a, 0) :: l₂
s : Pairwise (fun a b => zipIdxLE le a b = true) (l₁ ++ (a, 0) :: l₂)
p : (a :: l).zipIdx.mergeSort (zipIdxLE le) ~ (a :: l).zipIdx
⊢ ∃ l₁ l₂,
    map (fun x => x.fst) (((a, 0) :: l.zipIdx (0 + 1)).mergeSort (zipIdxLE le)) = l₁ ++ a :: l₂ ∧
      l.mergeSort le = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true