case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
cases' e : split l with l₁ l₂
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
fst_eq✝ : a :: l₂ = l₁'
snd_eq✝ : l₁ = l₂'
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
injection (split_cons_of_eq _ e).symm.trans h
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
⊢ length (a :: l₂) ≤ length (a :: l) ∧ length l₁ ≤ length (a :: l)
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
fst_eq✝ : a :: l₂ = l₁'
snd_eq✝ : l₁ = l₂'
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
substs l₁' l₂'
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
h₁ : length l₁ ≤ length l
h₂ : length l₂ ≤ length l
⊢ length (a :: l₂) ≤ length (a :: l) ∧ length l₁ ≤ length (a :: l)
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
⊢ length (a :: l₂) ≤ length (a :: l) ∧ length l₁ ≤ length (a :: l)
cases' length_split_le e with h₁ h₂
no goals
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
h₁ : length l₁ ≤ length l
h₂ : length l₂ ≤ length l
⊢ length (a :: l₂) ≤ length (a :: l) ∧ length l₁ ≤ length (a :: l)
exact ⟨Nat.succ_le_succ h₂, Nat.le_succ_of_le h₁⟩