-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem mergeSort_zipIdx {l : List α} :
    (mergeSort (l.zipIdx) (zipIdxLE le)).map (·.1) = mergeSort l le :=
  go 0 l
where go : ∀ (i : Nat) (l : List α),
    (mergeSort (l.zipIdx i) (zipIdxLE le)).map (·.1) = mergeSort l le
  | _, []
  | _, [a] => by simp [mergeSort]
  | _, a :: b :: xs => by
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1

Proof state:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ xs.length + 1 + 1 - (xs.length + 1 + 1 + 1) / 2 < xs.length + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ map (fun x => x.fst) (((a :: b :: xs).zipIdx x✝).mergeSort (zipIdxLE le)) = (a :: b :: xs).mergeSort le

Tactic:
simp only [mergeSort, zipIdx]

Result:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ map (fun x => x.fst)
      (((splitInTwo ⟨(a, x✝) :: (b, x✝ + 1) :: xs.zipIdx (x✝ + 1 + 1), ⋯⟩).fst.val.mergeSort (zipIdxLE le)).merge
        ((splitInTwo ⟨(a, x✝) :: (b, x✝ + 1) :: xs.zipIdx (x✝ + 1 + 1), ⋯⟩).snd.val.mergeSort (zipIdxLE le))
        (zipIdxLE le)) =
    ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le

Proof state:
case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
j : α
x : Nat
k : α
y : Nat
mx : (j, x) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝
my : (k, y) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)
this✝² : min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) < xs.length + 1 + 1
this✝¹ : xs.length + 1 + 1 - (xs.length + 1 + 1 + 1) / 2 < xs.length + 1 + 1
this✝ : x✝ ≤ x ∧ x < x✝ + min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) ∧ j = (a :: b :: xs)[x - x✝]
this :
  x✝ + (xs.length + 3) / 2 ≤ y ∧
    y < x✝ + (xs.length + 3) / 2 + (xs.length + 1 + 1 - (xs.length + 1 + 1 + 1) / 2) ∧
      k = (a :: b :: xs)[(xs.length + 1 + 1 + 1) / 2 + (y - (x✝ + (xs.length + 3) / 2))]
⊢ x ≤ y

Tactic:
omega

Result:
no goals

Proof state:
case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
j : α
x : Nat
k : α
y : Nat
mx : (j, x) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝
my : (k, y) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)
⊢ x ≤ y

Tactic:
have := mem_zipIdx mx

Result:
case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝¹ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
j : α
x : Nat
k : α
y : Nat
mx : (j, x) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝
my : (k, y) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)
this :
  x✝ ≤ x ∧ x < x✝ + (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length ∧ j = (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val[x - x✝]
⊢ x ≤ y

Proof state:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
⊢ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1

Tactic:
simp [splitInTwo_fst]

Result:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
⊢ min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) < xs.length + 1 + 1

Proof state:
case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝² : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this✝¹ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
j : α
x : Nat
k : α
y : Nat
mx : (j, x) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝
my : (k, y) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)
this✝ :
  x✝ ≤ x ∧ x < x✝ + (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length ∧ j = (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val[x - x✝]
this :
  x✝ + (xs.length + 3) / 2 ≤ y ∧
    y < x✝ + (xs.length + 3) / 2 + (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length ∧
      k = (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val[y - (x✝ + (xs.length + 3) / 2)]
⊢ x ≤ y

Tactic:
simp_all

Result:
case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
j : α
x : Nat
k : α
y : Nat
mx : (j, x) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝
my : (k, y) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)
this✝² : min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) < xs.length + 1 + 1
this✝¹ : xs.length + 1 + 1 - (xs.length + 1 + 1 + 1) / 2 < xs.length + 1 + 1
this✝ : x✝ ≤ x ∧ x < x✝ + min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) ∧ j = (a :: b :: xs)[x - x✝]
this :
  x✝ + (xs.length + 3) / 2 ≤ y ∧
    y < x✝ + (xs.length + 3) / 2 + (xs.length + 1 + 1 - (xs.length + 1 + 1 + 1) / 2) ∧
      k = (a :: b :: xs)[(xs.length + 1 + 1 + 1) / 2 + (y - (x✝ + (xs.length + 3) / 2))]
⊢ x ≤ y

Proof state:
case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ ∀ (a_1 : α) (b_1 : Nat) (a_2 : α) (b_2 : Nat),
    (a_1, b_1) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝ →
      (a_2, b_2) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2) → b_1 ≤ b_2

Tactic:
intros j x k y mx my

Result:
case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
j : α
x : Nat
k : α
y : Nat
mx : (j, x) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝
my : (k, y) ∈ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)
⊢ x ≤ y

Proof state:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ map (fun x => x.fst)
      ((((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝).mergeSort (zipIdxLE le)).merge
        (((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)).mergeSort (zipIdxLE le))
        (zipIdxLE le)) =
    ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le

Tactic:
rw [merge_stable]

Result:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ (map (fun x => x.fst) (((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝).mergeSort (zipIdxLE le))).merge
      (map (fun x => x.fst)
        (((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)).mergeSort (zipIdxLE le)))
      le =
    ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le

case x
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ ∀ (x y : α × Nat),
    x ∈ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.zipIdx x✝).mergeSort (zipIdxLE le) →
      y ∈ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.zipIdx (x✝ + (xs.length + 3) / 2)).mergeSort (zipIdxLE le) →
        x.snd ≤ y.snd