no goals
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
x✝¹ x✝ : Sorted r []
⊢ Sorted r (List.merge r [] [])
simp [List.merge]
no goals
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
b : α
l' : List α
x✝ : Sorted r []
h₂ : Sorted r (b :: l')
⊢ Sorted r (List.merge r [] (b :: l'))
simpa [List.merge] using h₂
no goals
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
h₁ : Sorted r (a :: l)
x✝ : Sorted r []
⊢ Sorted r (List.merge r (a :: l) [])
simpa [List.merge] using h₁
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
⊢ Sorted r (List.merge r (a :: l) (b :: l'))

case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
by_cases h : a ≼ b
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
⊢ ∀ (b' : α), b' ∈ List.merge r l (b :: l') → r a b'
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
suffices ∀ (b' : α) (_ : b' ∈ List.merge r l (b :: l')), r a b' by
  simpa [List.merge, h, h₁.of_cons.merge h₂]
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
⊢ r a b'
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
⊢ ∀ (b' : α), b' ∈ List.merge r l (b :: l') → r a b'
intro b' bm
case pos.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
be : b' = b
⊢ r a b'

case pos.inr.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
bl : b' ∈ l
⊢ r a b'

case pos.inr.inr
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
bl' : b' ∈ l'
⊢ r a b'
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
⊢ r a b'
rcases show b' = b ∨ b' ∈ l ∨ b' ∈ l' by
    simpa [or_left_comm] using (perm_merge _ _ _).subset bm with
  (be | bl | bl')
no goals
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
this : ∀ (b' : α), b' ∈ List.merge r l (b :: l') → r a b'
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
simpa [List.merge, h, h₁.of_cons.merge h₂]
no goals
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
⊢ b' = b ∨ b' ∈ l ∨ b' ∈ l'
simpa [or_left_comm] using (perm_merge _ _ _).subset bm
case pos.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
bm : b ∈ List.merge r l (b :: l')
⊢ r a b
case pos.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
be : b' = b
⊢ r a b'
subst b'
no goals
case pos.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
bm : b ∈ List.merge r l (b :: l')
⊢ r a b
assumption
no goals
case pos.inr.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
bl : b' ∈ l
⊢ r a b'
exact rel_of_sorted_cons h₁ _ bl
no goals
case pos.inr.inr
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
bl' : b' ∈ l'
⊢ r a b'
exact _root_.trans h (rel_of_sorted_cons h₂ _ bl')
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
⊢ ∀ (b' : α), b' ∈ List.merge r (a :: l) l' → r b b'
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
suffices ∀ (b' : α) (_ : b' ∈ List.merge r (a :: l) l'), r b b' by
  simpa [List.merge, h, h₁.merge h₂.of_cons]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
⊢ r b b'
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
⊢ ∀ (b' : α), b' ∈ List.merge r (a :: l) l' → r b b'
intro b' bm
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
⊢ r b b'
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
⊢ r b b'
have ba : b ≼ a := (total_of r _ _).resolve_left h
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
this : b' = a ∨ b' ∈ l ∨ b' ∈ l'
⊢ r b b'
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
⊢ r b b'
have : b' = a ∨ b' ∈ l ∨ b' ∈ l' := by simpa using (perm_merge _ _ _).subset bm
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
be : b' = a
⊢ r b b'

case neg.inr.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
bl : b' ∈ l
⊢ r b b'

case neg.inr.inr
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
bl' : b' ∈ l'
⊢ r b b'
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
this : b' = a ∨ b' ∈ l ∨ b' ∈ l'
⊢ r b b'
rcases this with (be | bl | bl')
no goals
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
this : ∀ (b' : α), b' ∈ List.merge r (a :: l) l' → r b b'
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
simpa [List.merge, h, h₁.merge h₂.of_cons]
no goals
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
⊢ b' = a ∨ b' ∈ l ∨ b' ∈ l'
simpa using (perm_merge _ _ _).subset bm
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
ba : r b a
bm : a ∈ List.merge r (a :: l) l'
⊢ r b a
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
be : b' = a
⊢ r b b'
subst b'
no goals
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
ba : r b a
bm : a ∈ List.merge r (a :: l) l'
⊢ r b a
assumption
no goals
case neg.inr.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
bl : b' ∈ l
⊢ r b b'
exact _root_.trans ba (rel_of_sorted_cons h₁ _ bl)
no goals
case neg.inr.inr
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
bl' : b' ∈ l'
⊢ r b b'
exact rel_of_sorted_cons h₂ _ bl'