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

Tactic:
exact trans _ _ _ h (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
z : α
m : z ∈ (x :: l₁).merge l₂ le
⊢ le y z = true

Tactic:
rw [mem_merge, mem_cons] at 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 ∨ z ∈ l₁) ∨ z ∈ l₂
⊢ le y z = true

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

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

Result:
case cons.cons.isTrue.a.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₁)
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₁
⊢ le x z = true

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

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

Proof state:
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

Tactic:
exact trans _ _ _ (by simpa [h] using total x y) (rel_of_pairwise_cons h₁ m)

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

Tactic:
simp only [merge]

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

Proof state:
case cons.cons.isTrue.a.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₁)
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₁
⊢ le x z = true

Tactic:
exact rel_of_pairwise_cons h₁ m

Result:
no goals