-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.2 ≤ y.2),
    (merge xs ys (zipIdxLE le)).map (·.1) = merge (xs.map (·.1)) (ys.map (·.1)) le
  | [], ys, _ => by simp [merge]
  | xs, [], _ => by simp [merge]
  | (i, x) :: xs, (j, y) :: ys, h => by
    simp only [merge, zipIdxLE, map_cons]
    split <;> rename_i w
    · rw [if_pos (by simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)])]
      simp only [map_cons, cons.injEq, true_and]
      rw [merge_stable, map_cons]
      exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
    · simp only [↓reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]
      rw [merge_stable, map_cons]
      exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)

Proof state:
α : Type u_1
le : α → α → Bool
xs : List (α × Nat)
x✝ : ∀ (x y : α × Nat), x ∈ xs → y ∈ [] → x.snd ≤ y.snd
⊢ map (fun x => x.fst) (xs.merge [] (zipIdxLE le)) = (map (fun x => x.fst) xs).merge (map (fun x => x.fst) []) le

Tactic:
simp [merge]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ (if le j i = true then decide (x ≤ y) else true) = true

Tactic:
simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)]

Result:
no goals

Proof state:
case isFalse.x
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : ¬le i j = true
⊢ ∀ (x_1 y : α × Nat), x_1 ∈ (i, x) :: xs → y ∈ ys → x_1.snd ≤ y.snd

Tactic:
exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)

Result:
no goals

Proof state:
case isFalse
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : ¬le i j = true
⊢ map (fun x => x.fst) (((i, x) :: xs).merge ys (zipIdxLE le)) =
    (i :: map (fun x => x.fst) xs).merge (map (fun x => x.fst) ys) le

Tactic:
rw [merge_stable, map_cons]

Result:
case isFalse.x
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : ¬le i j = true
⊢ ∀ (x_1 y : α × Nat), x_1 ∈ (i, x) :: xs → y ∈ ys → x_1.snd ≤ y.snd

Proof state:
case isTrue
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ map (fun x => x.fst) (xs.merge ((j, y) :: ys) (zipIdxLE le)) =
    (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le

Tactic:
rw [merge_stable, map_cons]

Result:
case isTrue.x
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ ∀ (x y_1 : α × Nat), x ∈ xs → y_1 ∈ (j, y) :: ys → x.snd ≤ y_1.snd

Proof state:
case isTrue
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ map (fun x => x.fst) ((i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)) =
    i :: (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le

Tactic:
simp only [map_cons, cons.injEq, true_and]

Result:
case isTrue
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ map (fun x => x.fst) (xs.merge ((j, y) :: ys) (zipIdxLE le)) =
    (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le

Proof state:
α : Type u_1
le : α → α → Bool
ys : List (α × Nat)
x✝ : ∀ (x y : α × Nat), x ∈ [] → y ∈ ys → x.snd ≤ y.snd
⊢ map (fun x => x.fst) ([].merge ys (zipIdxLE le)) = (map (fun x => x.fst) []).merge (map (fun x => x.fst) ys) le

Tactic:
simp [merge]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
⊢ map (fun x => x.fst) (((i, x) :: xs).merge ((j, y) :: ys) (zipIdxLE le)) =
    (map (fun x => x.fst) ((i, x) :: xs)).merge (map (fun x => x.fst) ((j, y) :: ys)) le

Tactic:
simp only [merge, zipIdxLE, map_cons]

Result:
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
⊢ map (fun x => x.fst)
      (if (if le i j = true then if le j i = true then decide (x ≤ y) else true else false) = true then
        (i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)
      else (j, y) :: ((i, x) :: xs).merge ys (zipIdxLE le)) =
    if le i j = true then i :: (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le
    else j :: (i :: map (fun x => x.fst) xs).merge (map (fun x => x.fst) ys) le

Proof state:
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
⊢ map (fun x => x.fst)
      (if (if le i j = true then if le j i = true then decide (x ≤ y) else true else false) = true then
        (i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)
      else (j, y) :: ((i, x) :: xs).merge ys (zipIdxLE le)) =
    if le i j = true then i :: (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le
    else j :: (i :: map (fun x => x.fst) xs).merge (map (fun x => x.fst) ys) le

Tactic:
split <;> rename_i w

Result:
case isTrue
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ map (fun x => x.fst)
      (if (if le j i = true then decide (x ≤ y) else true) = true then (i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)
      else (j, y) :: ((i, x) :: xs).merge ys (zipIdxLE le)) =
    i :: (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le

case isFalse
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : ¬le i j = true
⊢ map (fun x => x.fst)
      (if false = true then (i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)
      else (j, y) :: ((i, x) :: xs).merge ys (zipIdxLE le)) =
    j :: (i :: map (fun x => x.fst) xs).merge (map (fun x => x.fst) ys) le

Proof state:
case isTrue
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ map (fun x => x.fst)
      (if (if le j i = true then decide (x ≤ y) else true) = true then (i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)
      else (j, y) :: ((i, x) :: xs).merge ys (zipIdxLE le)) =
    i :: (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le

Tactic:
rw [if_pos (by simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)])]

Result:
case isTrue
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ map (fun x => x.fst) ((i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)) =
    i :: (map (fun x => x.fst) xs).merge (j :: map (fun x => x.fst) ys) le