-- 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.mk.mk
α : 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₂
a : α
i : Nat
b : α
j : Nat
ha : (a, i) ∈ l.zipIdx 1
hb : (b, j) ∈ l.zipIdx 1
⊢ decide (le a b = true) = true →
    (if le b a = true then decide (i ≤ j) else true) = true →
      decide (le b a = true) = true → (if le a b = true then decide (j ≤ i) else true) = true → a = b ∧ i = j

Tactic:
intro ab h ba h'

Result:
case intro.intro.refine_2.e_a.x.mk.mk
α : 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₂
a : α
i : Nat
b : α
j : Nat
ha : (a, i) ∈ l.zipIdx 1
hb : (b, j) ∈ l.zipIdx 1
ab : decide (le a b = true) = true
h : (if le b a = true then decide (i ≤ j) else true) = true
ba : decide (le b a = true) = true
h' : (if le a b = true then decide (j ≤ i) else true) = true
⊢ a = b ∧ i = j

Proof state:
α : 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 α
⊢ ∃ l₁ l₂, (a :: l).mergeSort le = l₁ ++ a :: l₂ ∧ l.mergeSort le = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true

Tactic:
rw [← mergeSort_zipIdx]

Result:
α : 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 α
⊢ ∃ l₁ l₂,
    map (fun x => x.fst) ((a :: l).zipIdx.mergeSort (zipIdxLE le)) = l₁ ++ a :: l₂ ∧
      l.mergeSort le = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true

Proof state:
α : 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₂
a : α
i : Nat
b : α
j : Nat
ha : (a, i) ∈ l.zipIdx 1
hb : (b, j) ∈ l.zipIdx 1
ab : decide (le a b = true) = true
h' : (if le a b = true then decide (j ≤ i) else true) = true
ba : le b a = true
h : i ≤ j
⊢ j ≤ i

Tactic:
simpa [ab, ba] using h'

Result:
no goals

Proof state:
α : 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 α
⊢ (map (fun x => x.snd) (a :: l).zipIdx).Nodup

Tactic:
rw [zipIdx_map_snd]

Result:
α : 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 α
⊢ (range' 0 (a :: l).length).Nodup

Proof state:
case intro.intro.refine_2.e_a.x.mk.mk.refl.left
α : 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₂
a : α
i : Nat
b : α
ha : (a, i) ∈ l.zipIdx 1
ab : decide (le a b = true) = true
ba : le b a = true
hb : (b, i) ∈ l.zipIdx 1
h h' : i ≤ i
⊢ a = b

Tactic:
have := mem_zipIdx ha

Result:
case intro.intro.refine_2.e_a.x.mk.mk.refl.left
α : 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₂
a : α
i : Nat
b : α
ha : (a, i) ∈ l.zipIdx 1
ab : decide (le a b = true) = true
ba : le b a = true
hb : (b, i) ∈ l.zipIdx 1
h h' : i ≤ i
this : 1 ≤ i ∧ i < 1 + l.length ∧ a = l[i - 1]
⊢ 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₂
⊢ ∀ (a b : α × Nat),
    a ∈ (l.zipIdx 1).mergeSort (zipIdxLE le) → b ∈ l₁ ++ l₂ → zipIdxLE le a b = true → zipIdxLE le b a = true → a = b

Tactic:
rintro ⟨a, i⟩ ⟨b, j⟩  ha hb

Result:
case intro.intro.refine_2.e_a.x.mk.mk
α : 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₂
a : α
i : Nat
b : α
j : Nat
ha : (a, i) ∈ (l.zipIdx 1).mergeSort (zipIdxLE le)
hb : (b, j) ∈ l₁ ++ l₂
⊢ zipIdxLE le (a, i) (b, j) = true → zipIdxLE le (b, j) (a, i) = true → (a, i) = (b, j)