Theorem: List.Sublist.exists_intermediate (LeanCamCombi/Mathlib/Data/List/DropRight.lean)

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l₀ <+ l₂
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
Tactic:
induction' l₀ with a l₀ ih generalizing n l₂
State after:
case nil
α : Type u_1
l l' l₁ : List α
a b : α
m : ℕ
l₂ : List α
n : ℕ
hl : [] <+ l₂
h₀ : [].length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, [] <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n

case cons
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
n : ℕ
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n

State before:
case cons
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
n : ℕ
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
Tactic:
cases n
State after:
case cons.zero
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ 0
h₂ : 0 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = 0

case cons.succ
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
h₂ : n✝ + 1 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n✝ + 1

State before:
case cons.succ
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
h₂ : n✝ + 1 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n✝ + 1
Tactic:
cases' l₂ with b l₂
State after:
case cons.succ.nil
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
hl : a :: l₀ <+ []
h₂ : n✝ + 1 ≤ [].length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ [] ∧ l₁.length = n✝ + 1

case cons.succ.cons
α : Type u_1
l l' l₁ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
h₂ : n✝ + 1 ≤ (b :: l₂).length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ b :: l₂ ∧ l₁.length = n✝ + 1

State before:
case cons.succ.cons
α : Type u_1
l l' l₁ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
h₂ : n✝ + 1 ≤ (b :: l₂).length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ b :: l₂ ∧ l₁.length = n✝ + 1
Tactic:
obtain ⟨l₁, h₀₁, h₁₂, rfl⟩ := ih sorry (Nat.succ_le_succ_iff.1 h₀) (Nat.le_of_succ_le h₂)
State after:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1

State before:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1
Tactic:
rw [cons_sublist_cons_iff'] at hl
State after:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ l₂ ∨ a = b ∧ l₀ <+ l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1

State before:
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ l₂ ∨ a = b ∧ l₀ <+ l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1
Tactic:
obtain hl | ⟨rfl, hl⟩ := hl
State after:
case cons.succ.cons.intro.intro.intro.inl
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
hl : a :: l₀ <+ l₂
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1

case cons.succ.cons.intro.intro.intro.inr.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ l₁ : List α
h₀₁ : l₀ <+ l₁
h₀ : (a :: l₀).length ≤ l₁.length + 1
hl : l₀ <+ l₂
h₁₂ : l₁ <+ a :: l₂
h₂ : l₁.length + 1 ≤ (a :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ a :: l₂ ∧ l₁_1.length = l₁.length + 1

State before:
case nil
α : Type u_1
l l' l₁ : List α
a b : α
m : ℕ
l₂ : List α
n : ℕ
hl : [] <+ l₂
h₀ : [].length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, [] <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
Tactic:
exact (exists_sublist_length_eq h₂).imp (fun l₁ h ↦ ⟨nil_sublist _, h⟩)
State after:
no goals

State before:
case cons.zero
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ 0
h₂ : 0 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = 0
Tactic:
cases h₀
State after:
no goals

State before:
case cons.succ.nil
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
hl : a :: l₀ <+ []
h₂ : n✝ + 1 ≤ [].length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ [] ∧ l₁.length = n✝ + 1
Tactic:
cases h₂
State after:
no goals