-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem map_mergeSort {r : α → α → Bool} {s : β → β → Bool} {f : α → β} {l : List α}
    (hl : ∀ a ∈ l, ∀ b ∈ l, r a b = s (f a) (f b)) :
    (l.mergeSort r).map f = (l.map f).mergeSort s :=
  match l with
  | [] => by simp
  | [x] => by simp
  | a :: b :: l => by
    simp only [mergeSort, splitInTwo_fst, splitInTwo_snd, map_cons]
    rw [map_merge (fun a am b bm => hl a (mem_of_mem_take (by simpa using am))
      b (mem_of_mem_drop (by simpa using bm)))]
    rw [map_mergeSort (s := s) (fun a am b bm => hl a (mem_of_mem_take (by simpa using am))
      b (mem_of_mem_take (by simpa using bm)))]
    rw [map_mergeSort (s := s) (fun a am b bm => hl a (mem_of_mem_drop (by simpa using am))
      b (mem_of_mem_drop (by simpa using bm)))]
    rw [map_take, map_drop]
    simp
  termination_by length l

Proof state:
α : Type u_2
β : Type u_1
r : α → α → Bool
s : β → β → Bool
f : α → β
l✝ : List α
a✝ b✝ : α
l : List α
hl : ∀ (a : α), a ∈ a✝ :: b✝ :: l → ∀ (b : α), b ∈ a✝ :: b✝ :: l → r a b = s (f a) (f b)
a : α
am : a ∈ drop (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)
b : α
bm : b ∈ drop (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)
⊢ b ∈ drop (?m.152367 a am b bm) (a✝ :: b✝ :: l)

Tactic:
simpa using bm

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
r : α → α → Bool
s : β → β → Bool
f : α → β
l : List α
x : α
hl : ∀ (a : α), a ∈ [x] → ∀ (b : α), b ∈ [x] → r a b = s (f a) (f b)
⊢ map f ([x].mergeSort r) = (map f [x]).mergeSort s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
r : α → α → Bool
s : β → β → Bool
f : α → β
l✝ : List α
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → r a_1 b_1 = s (f a_1) (f b_1)
⊢ map f
      (((take (((a :: b :: l).length + 1) / 2) (a :: b :: l)).mergeSort r).merge
        ((drop (((a :: b :: l).length + 1) / 2) (a :: b :: l)).mergeSort r) r) =
    ((take (((f a :: f b :: map f l).length + 1) / 2) (f a :: f b :: map f l)).mergeSort s).merge
      ((drop (((f a :: f b :: map f l).length + 1) / 2) (f a :: f b :: map f l)).mergeSort s) s

Tactic:
rw [map_merge (fun a am b bm => hl a (mem_of_mem_take (by simpa using am))
  b (mem_of_mem_drop (by simpa using bm)))]

Result:
α : Type u_2
β : Type u_1
r : α → α → Bool
s : β → β → Bool
f : α → β
l✝ : List α
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → r a_1 b_1 = s (f a_1) (f b_1)
⊢ (map f ((take (((a :: b :: l).length + 1) / 2) (a :: b :: l)).mergeSort r)).merge
      (map f ((drop (((a :: b :: l).length + 1) / 2) (a :: b :: l)).mergeSort r)) s =
    ((take (((f a :: f b :: map f l).length + 1) / 2) (f a :: f b :: map f l)).mergeSort s).merge
      ((drop (((f a :: f b :: map f l).length + 1) / 2) (f a :: f b :: map f l)).mergeSort s) s

Proof state:
α : Type u_2
β : Type u_1
r : α → α → Bool
s : β → β → Bool
f : α → β
l✝ : List α
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → r a_1 b_1 = s (f a_1) (f b_1)
⊢ map f ((a :: b :: l).mergeSort r) = (map f (a :: b :: l)).mergeSort s

Tactic:
simp only [mergeSort, splitInTwo_fst, splitInTwo_snd, map_cons]

Result:
α : Type u_2
β : Type u_1
r : α → α → Bool
s : β → β → Bool
f : α → β
l✝ : List α
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → r a_1 b_1 = s (f a_1) (f b_1)
⊢ map f
      (((take (((a :: b :: l).length + 1) / 2) (a :: b :: l)).mergeSort r).merge
        ((drop (((a :: b :: l).length + 1) / 2) (a :: b :: l)).mergeSort r) r) =
    ((take (((f a :: f b :: map f l).length + 1) / 2) (f a :: f b :: map f l)).mergeSort s).merge
      ((drop (((f a :: f b :: map f l).length + 1) / 2) (f a :: f b :: map f l)).mergeSort s) s