-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem map_merge {f : α → β} {r : α → α → Bool} {s : β → β → Bool} {l l' : List α}
    (hl : ∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) :
    (l.merge l' r).map f = (l.map f).merge (l'.map f) s

Proof state:
case isTrue
α : Type u_2
β : Type u_1
f : α → β
r : α → α → Bool
s : β → β → Bool
l l' : List α
x : α
xs : List α
x' : α
xs' : List α
hl :
  (r x x' = s (f x) (f x') ∧ ∀ (x_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)) ∧
    (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)
h✝ : r x x' = true
⊢ (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧ ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)

Tactic:
exact ⟨hl.2.1, hl.2.2⟩

Result:
no goals

Proof state:
case isTrue
α : Type u_2
β : Type u_1
f : α → β
r : α → α → Bool
s : β → β → Bool
l l' : List α
x : α
xs : List α
x' : α
xs' : List α
hl :
  (r x x' = s (f x) (f x') ∧ ∀ (x_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)) ∧
    (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)
h✝ : r x x' = true
⊢ map f (x :: xs.merge (x' :: xs') r) = f x :: (map f xs).merge (f x' :: map f xs') s

Tactic:
rw [List.map, map_merge, List.map]

Result:
case isTrue
α : Type u_2
β : Type u_1
f : α → β
r : α → α → Bool
s : β → β → Bool
l l' : List α
x : α
xs : List α
x' : α
xs' : List α
hl :
  (r x x' = s (f x) (f x') ∧ ∀ (x_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)) ∧
    (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)
h✝ : r x x' = true
⊢ ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ x' :: xs' → r a b = s (f a) (f b)

Proof state:
α : Type u_2
β : Type u_1
f : α → β
r : α → α → Bool
s : β → β → Bool
l l' : List α
x : α
xs : List α
x' : α
xs' : List α
hl :
  (r x x' = s (f x) (f x') ∧ ∀ (x_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)) ∧
    (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)
⊢ map f (if r x x' = true then x :: xs.merge (x' :: xs') r else x' :: (x :: xs).merge xs' r) =
    if s (f x) (f x') = true then f x :: (map f xs).merge (f x' :: map f xs') s
    else f x' :: (f x :: map f xs).merge (map f xs') s

Tactic:
rw [← hl.1.1]

Result:
α : Type u_2
β : Type u_1
f : α → β
r : α → α → Bool
s : β → β → Bool
l l' : List α
x : α
xs : List α
x' : α
xs' : List α
hl :
  (r x x' = s (f x) (f x') ∧ ∀ (x_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)) ∧
    (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)
⊢ map f (if r x x' = true then x :: xs.merge (x' :: xs') r else x' :: (x :: xs).merge xs' r) =
    if r x x' = true then f x :: (map f xs).merge (f x' :: map f xs') s
    else f x' :: (f x :: map f xs).merge (map f xs') s

Proof state:
case isTrue
α : Type u_2
β : Type u_1
f : α → β
r : α → α → Bool
s : β → β → Bool
l l' : List α
x : α
xs : List α
x' : α
xs' : List α
hl :
  (r x x' = s (f x) (f x') ∧ ∀ (x_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)) ∧
    (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)
h✝ : r x x' = true
⊢ ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ x' :: xs' → r a b = s (f a) (f b)

Tactic:
simp only [List.forall_mem_cons, forall_and]

Result:
case isTrue
α : Type u_2
β : Type u_1
f : α → β
r : α → α → Bool
s : β → β → Bool
l l' : List α
x : α
xs : List α
x' : α
xs' : List α
hl :
  (r x x' = s (f x) (f x') ∧ ∀ (x_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)) ∧
    (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)
h✝ : r x x' = true
⊢ (∀ (x : α), x ∈ xs → r x x' = s (f x) (f x')) ∧ ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs' → r x x_2 = s (f x) (f x_2)