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