-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem sorted_merge
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a)
    (l₁ l₂ : List α) (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge l₁ l₂ le).Pairwise le

Proof state:
case cons.cons.isTrue.a
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
y : α
l₂ : List α
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((x :: l₁).merge l₂ le)
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
h : le x y = true
⊢ ∀ (a' : α), a' ∈ l₁.merge (y :: l₂) le → le x a' = true

Tactic:
intro z m

Result:
case cons.cons.isTrue.a
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
y : α
l₂ : List α
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((x :: l₁).merge l₂ le)
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
h : le x y = true
z : α
m : z ∈ l₁.merge (y :: l₂) le
⊢ le x z = true

Proof state:
case cons.nil
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
h₂ : Pairwise (fun a b => le a b = true) []
⊢ Pairwise (fun a b => le a b = true) ((x :: l₁).merge [] le)

Tactic:
simpa only [merge]

Result:
no goals

Proof state:
case cons.cons.isTrue
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
y : α
l₂ : List α
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((x :: l₁).merge l₂ le)
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
h : le x y = true
⊢ Pairwise (fun a b => le a b = true) (x :: l₁.merge (y :: l₂) le)

Tactic:
apply Pairwise.cons

Result:
case cons.cons.isTrue.a
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
y : α
l₂ : List α
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((x :: l₁).merge l₂ le)
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
h : le x y = true
⊢ ∀ (a' : α), a' ∈ l₁.merge (y :: l₂) le → le x a' = true

case cons.cons.isTrue.a
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
y : α
l₂ : List α
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((x :: l₁).merge l₂ le)
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
h : le x y = true
⊢ Pairwise (fun a b => le a b = true) (l₁.merge (y :: l₂) le)

Proof state:
case cons.cons.isTrue.a
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
y : α
l₂ : List α
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((x :: l₁).merge l₂ le)
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
h : le x y = true
z : α
m : z ∈ l₁.merge (y :: l₂) le
⊢ le x z = true

Tactic:
rw [mem_merge, mem_cons] at m

Result:
case cons.cons.isTrue.a
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
x : α
l₁ : List α
ih₁ :
  ∀ (l₂ : List α),
    Pairwise (fun a b => le a b = true) l₁ →
      Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
h₁ : Pairwise (fun a b => le a b = true) (x :: l₁)
y : α
l₂ : List α
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((x :: l₁).merge l₂ le)
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
h : le x y = true
z : α
m : z ∈ l₁ ∨ z = y ∨ z ∈ l₂
⊢ le x z = true