-- 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 ∈ (take (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)).mergeSort r
b : α
bm : b ∈ (drop (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)).mergeSort r
⊢ b ∈ drop (?m.151738 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 α
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

Tactic:
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)))]

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 s).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 : α), 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)
⊢ a ∈ drop (?m.152365 a am b bm) (a✝ :: b✝ :: l)

Tactic:
simpa using am

Result:
no goals

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 ∈ take (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)
b : α
bm : b ∈ take (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)
⊢ b ∈ take (?m.152114 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 α
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 ∈ take (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)
b : α
bm : b ∈ take (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)
⊢ a ∈ take (?m.152112 a am b bm) (a✝ :: b✝ :: l)

Tactic:
simpa using am

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
r : α → α → Bool
s : β → β → Bool
f : α → β
l : List α
hl : ∀ (a : α), a ∈ [] → ∀ (b : α), b ∈ [] → r a b = s (f a) (f b)
⊢ map f ([].mergeSort r) = (map f []).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 : α), a ∈ a✝ :: b✝ :: l → ∀ (b : α), b ∈ a✝ :: b✝ :: l → r a b = s (f a) (f b)
a : α
am : a ∈ (take (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)).mergeSort r
b : α
bm : b ∈ (drop (((a✝ :: b✝ :: l).length + 1) / 2) (a✝ :: b✝ :: l)).mergeSort r
⊢ a ∈ take (?m.151736 a am b bm) (a✝ :: b✝ :: l)

Tactic:
simpa using am

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)
⊢ ((take (((a :: b :: l).length + 1) / 2) (map f (a :: b :: l))).mergeSort s).merge
      ((drop (((a :: b :: l).length + 1) / 2) (map f (a :: b :: l))).mergeSort s) 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

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 s).merge
      ((map f (drop (((a :: b :: l).length + 1) / 2) (a :: b :: l))).mergeSort s) 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

Tactic:
rw [map_take, map_drop]

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)
⊢ ((take (((a :: b :: l).length + 1) / 2) (map f (a :: b :: l))).mergeSort s).merge
      ((drop (((a :: b :: l).length + 1) / 2) (map f (a :: b :: l))).mergeSort s) 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 (take (((a :: b :: l).length + 1) / 2) (a :: b :: l))).mergeSort s).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

Tactic:
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)))]

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 s).merge
      ((map f (drop (((a :: b :: l).length + 1) / 2) (a :: b :: l))).mergeSort s) 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