-- 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 isFalse
α : 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
⊢ (∀ (b : α), b ∈ xs' → r x b = s (f x) (f b)) ∧ ∀ (x : α), x ∈ xs → ∀ (b : α), b ∈ xs' → r x b = s (f x) (f b)

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

Result:
no goals

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 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

Tactic:
split

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
⊢ map f (x :: xs.merge (x' :: xs') r) = f x :: (map f xs).merge (f x' :: map f xs') s

case isFalse
α : 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' :: (x :: xs).merge xs' r) = f x' :: (f x :: map f xs).merge (map f xs') s

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_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)
⊢ map f ((x :: xs).merge (x' :: xs') r) = (map f (x :: xs)).merge (map f (x' :: xs')) s

Tactic:
simp only [forall_and] at hl

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 ((x :: xs).merge (x' :: xs') r) = (map f (x :: xs)).merge (map f (x' :: xs')) s

Proof state:
case isFalse
α : 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 ∈ x :: xs → ∀ (b : α), b ∈ xs' → r a b = s (f a) (f b)

Tactic:
simp only [List.forall_mem_cons]

Result:
case isFalse
α : 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
⊢ (∀ (b : α), b ∈ xs' → r x b = s (f x) (f b)) ∧ ∀ (x : α), x ∈ xs → ∀ (b : α), b ∈ xs' → r x b = s (f x) (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 : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x' :: xs' → r a b = s (f a) (f b)
⊢ map f ((x :: xs).merge (x' :: xs') r) = (map f (x :: xs)).merge (map f (x' :: xs')) s

Tactic:
simp only [List.forall_mem_cons] at hl

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_1 : α), x_1 ∈ xs' → r x x_1 = s (f x) (f x_1)
⊢ map f ((x :: xs).merge (x' :: xs') r) = (map f (x :: xs)).merge (map f (x' :: xs')) s

Proof state:
case isFalse
α : 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' :: (x :: xs).merge xs' r) = f x' :: (f x :: map f xs).merge (map f xs') s

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

Result:
case isFalse
α : 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 ∈ x :: xs → ∀ (b : α), b ∈ 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 ((x :: xs).merge (x' :: xs') r) = (map f (x :: xs)).merge (map f (x' :: xs')) s

Tactic:
simp only [List.map, List.cons_merge_cons]

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 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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals