-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem sublist_mergeSort
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a) :
    ∀ {c : List α} (_ : c.Pairwise le) (_ : c <+ l),
    c <+ mergeSort l le
  | _, _, .slnil => nil_sublist _
  | c, hc, @Sublist.cons _ _ l a h => by
    obtain ⟨l₁, l₂, h₁, h₂, -⟩ := mergeSort_cons trans total a l
    rw [h₁]
    have h' := sublist_mergeSort trans total hc h
    rw [h₂] at h'
    exact h'.middle a
  | _, _, @Sublist.cons₂ _ l₁ l₂ a h => by
    rename_i hc
    obtain ⟨l₃, l₄, h₁, h₂, h₃⟩ := mergeSort_cons trans total a l₂
    rw [h₁]
    have h' := sublist_mergeSort trans total hc.tail h
    rw [h₂] at h'
    simp only [Bool.not_eq_true', tail_cons] at h₃ h'
    exact
      sublist_append_of_sublist_right (Sublist.cons₂ a
        ((fun w => Sublist.of_sublist_append_right w h') fun b m₁ m₃ =>
          (Bool.eq_not_self true).mp ((rel_of_pairwise_cons hc m₁).symm.trans (h₃ b m₃))))

Proof state:
case intro.intro.intro.intro
α : Type u_1
le : α → α → Bool
l✝ : List α
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
c : List α
hc : Pairwise (fun a b => le a b = true) c
l : List α
a : α
h : c <+ l
l₁ l₂ : List α
h₁ : (a :: l).mergeSort le = l₁ ++ a :: l₂
h₂ : l.mergeSort le = l₁ ++ l₂
⊢ c <+ (a :: l).mergeSort le

Tactic:
rw [h₁]

Result:
case intro.intro.intro.intro
α : Type u_1
le : α → α → Bool
l✝ : List α
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
c : List α
hc : Pairwise (fun a b => le a b = true) c
l : List α
a : α
h : c <+ l
l₁ l₂ : List α
h₁ : (a :: l).mergeSort le = l₁ ++ a :: l₂
h₂ : l.mergeSort le = l₁ ++ l₂
⊢ c <+ l₁ ++ a :: l₂

Proof state:
case intro.intro.intro.intro
α : Type u_1
le : α → α → Bool
l : List α
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
a : α
l₁ : List α
hc : Pairwise (fun a b => le a b = true) (a :: l₁)
l₂ : List α
h : l₁ <+ l₂
l₃ l₄ : List α
h₁ : (a :: l₂).mergeSort le = l₃ ++ a :: l₄
h₂ : l₂.mergeSort le = l₃ ++ l₄
h₃ : ∀ (b : α), b ∈ l₃ → (!le a b) = true
h' : (a :: l₁).tail <+ l₃ ++ l₄
⊢ a :: l₁ <+ l₃ ++ a :: l₄

Tactic:
simp only [Bool.not_eq_true', tail_cons] at h₃ h'

Result:
case intro.intro.intro.intro
α : Type u_1
le : α → α → Bool
l : List α
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
a : α
l₁ : List α
hc : Pairwise (fun a b => le a b = true) (a :: l₁)
l₂ : List α
h : l₁ <+ l₂
l₃ l₄ : List α
h₁ : (a :: l₂).mergeSort le = l₃ ++ a :: l₄
h₂ : l₂.mergeSort le = l₃ ++ l₄
h' : l₁ <+ l₃ ++ l₄
h₃ : ∀ (b : α), b ∈ l₃ → le a b = false
⊢ a :: l₁ <+ l₃ ++ a :: l₄

Proof state:
case intro.intro.intro.intro
α : Type u_1
le : α → α → Bool
l : List α
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
a : α
l₁ : List α
hc : Pairwise (fun a b => le a b = true) (a :: l₁)
l₂ : List α
h : l₁ <+ l₂
l₃ l₄ : List α
h₁ : (a :: l₂).mergeSort le = l₃ ++ a :: l₄
h₂ : l₂.mergeSort le = l₃ ++ l₄
h₃ : ∀ (b : α), b ∈ l₃ → (!le a b) = true
⊢ a :: l₁ <+ (a :: l₂).mergeSort le

Tactic:
rw [h₁]

Result:
case intro.intro.intro.intro
α : Type u_1
le : α → α → Bool
l : List α
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
a : α
l₁ : List α
hc : Pairwise (fun a b => le a b = true) (a :: l₁)
l₂ : List α
h : l₁ <+ l₂
l₃ l₄ : List α
h₁ : (a :: l₂).mergeSort le = l₃ ++ a :: l₄
h₂ : l₂.mergeSort le = l₃ ++ l₄
h₃ : ∀ (b : α), b ∈ l₃ → (!le a b) = true
⊢ a :: l₁ <+ l₃ ++ a :: l₄

Proof state:
case intro.intro.intro.intro
α : Type u_1
le : α → α → Bool
l : List α
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
a : α
l₁ : List α
hc : Pairwise (fun a b => le a b = true) (a :: l₁)
l₂ : List α
h : l₁ <+ l₂
l₃ l₄ : List α
h₁ : (a :: l₂).mergeSort le = l₃ ++ a :: l₄
h₂ : l₂.mergeSort le = l₃ ++ l₄
h' : l₁ <+ l₃ ++ l₄
h₃ : ∀ (b : α), b ∈ l₃ → le a b = false
⊢ a :: l₁ <+ l₃ ++ a :: l₄

Tactic:
exact
  sublist_append_of_sublist_right (Sublist.cons₂ a
    ((fun w => Sublist.of_sublist_append_right w h') fun b m₁ m₃ =>
      (Bool.eq_not_self true).mp ((rel_of_pairwise_cons hc m₁).symm.trans (h₃ b m₃))))

Result:
no goals