-- 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.inr.inl
α : 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₁)
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)
z : α
h₂ : Pairwise (fun a b => le a b = true) (z :: l₂)
h : le x z = true
⊢ le x z = true

Tactic:
exact h

Result:
no goals

Proof state:
case cons.cons
α : 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₂)
⊢ Pairwise (fun a b => le a b = true) (if le x y = true then x :: l₁.merge (y :: l₂) le else y :: (x :: l₁).merge l₂ le)

Tactic:
split <;> rename_i h

Result:
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)

case cons.cons.isFalse
α : 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) (y :: (x :: l₁).merge l₂ le)

Proof state:
case cons.cons.isFalse
α : 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) (y :: (x :: l₁).merge l₂ le)

Tactic:
apply Pairwise.cons

Result:
case cons.cons.isFalse.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' ∈ (x :: l₁).merge l₂ le → le y a' = true

case cons.cons.isFalse.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) ((x :: l₁).merge l₂ le)

Proof state:
case 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
l₂ : List α
h₁ : Pairwise (fun a b => le a b = true) []
h₂ : Pairwise (fun a b => le a b = true) l₂
⊢ Pairwise (fun a b => le a b = true) ([].merge l₂ le)

Tactic:
simpa only [merge]

Result:
no goals

Proof state:
case cons.cons.isFalse.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' ∈ (x :: l₁).merge l₂ le → le y a' = true

Tactic:
intro z m

Result:
case cons.cons.isFalse.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 ∈ (x :: l₁).merge l₂ le
⊢ le y z = true