-- 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
⊢ Pairwise (fun a b => le a b = true) (l₁.merge (y :: l₂) le)

Tactic:
exact ih₁ _ h₁.tail h₂

Result:
no goals

Proof state:
α : 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₂)
z : α
h : le x y = false
m : z ∈ l₁
⊢ le y x = true

Tactic:
simpa [h] using total x y

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₂)
z : α
m : (z = x ∨ z ∈ l₁) ∨ z ∈ l₂
h : le x y = false
⊢ le y z = true

Tactic:
rcases m with (⟨rfl|m⟩|m)

Result:
case cons.cons.isFalse.a.inl.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
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)
y : α
l₂ : List α
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
z : α
h₁ : Pairwise (fun a b => le a b = true) (z :: l₁)
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((z :: l₁).merge l₂ le)
h : le z y = false
⊢ le y z = true

case cons.cons.isFalse.a.inl.inr
α : 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₂)
z : α
h : le x y = false
m : z ∈ l₁
⊢ le y z = true

case cons.cons.isFalse.a.inr
α : 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₂)
z : α
h : le x y = false
m : z ∈ l₂
⊢ le y z = true

Proof state:
case cons.cons.isFalse.a.inr
α : 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₂)
z : α
h : le x y = false
m : z ∈ l₂
⊢ le y z = true

Tactic:
exact rel_of_pairwise_cons h₂ m

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

Tactic:
exact ih₂ h₂.tail

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
z : α
m : (z = x ∨ z ∈ l₁) ∨ z ∈ l₂
⊢ le y z = true

Tactic:
simp only [Bool.not_eq_true] at h

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₂)
z : α
m : (z = x ∨ z ∈ l₁) ∨ z ∈ l₂
h : le x y = false
⊢ le y z = true

Proof state:
case cons.cons.isFalse.a.inl.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
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)
y : α
l₂ : List α
h₂ : Pairwise (fun a b => le a b = true) (y :: l₂)
z : α
h₁ : Pairwise (fun a b => le a b = true) (z :: l₁)
ih₂ : Pairwise (fun a b => le a b = true) l₂ → Pairwise (fun a b => le a b = true) ((z :: l₁).merge l₂ le)
h : le z y = false
⊢ le y z = true

Tactic:
simpa [h] using total y z

Result:
no goals