α : Type uu
β : Type vv
l₁✝ l₂✝ l₁ l₂ l : List α
p : l ~ l₁
s : l <+ l₂
h : length l₁ < length l₂
⊢ length l < length l₂ → ∃ a, a :: l <+~ l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ l₁ l₂ l : List α
p : l ~ l₁
s : l <+ l₂
h : length l₁ < length l₂
⊢ ∃ a, a :: l₁ <+~ l₂
suffices length l < length l₂ → ∃ a : α, a :: l <+~ l₂ from
  (this <| p.symm.length_eq ▸ h).imp fun a => (p.cons a).subperm_right.1
α : Type uu
β : Type vv
l₁ l₂✝ l₂ l : List α
s : l <+ l₂
⊢ length l < length l₂ → ∃ a, a :: l <+~ l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ l₁ l₂ l : List α
p : l ~ l₁
s : l <+ l₂
h : length l₁ < length l₂
⊢ length l < length l₂ → ∃ a, a :: l <+~ l₂
clear h p l₁
case slnil
α : Type uu
β : Type vv
l₁ l₂✝ l₂ l : List α
h : length [] < length []
⊢ ∃ a, [a] <+~ []

case cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ l₂✝ l l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : length l₁ < length l₂ → ∃ a, a :: l₁ <+~ l₂
h : length l₁ < length (a :: l₂)
⊢ ∃ a_1, a_1 :: l₁ <+~ a :: l₂

case cons₂
α : Type uu
β : Type vv
l₁ l₂✝¹ l₂ l l₁✝ l₂✝ : List α
b : α
a✝ : l₁✝ <+ l₂✝
IH : length l₁✝ < length l₂✝ → ∃ a, a :: l₁✝ <+~ l₂✝
h : length (b :: l₁✝) < length (b :: l₂✝)
⊢ ∃ a, a :: b :: l₁✝ <+~ b :: l₂✝
α : Type uu
β : Type vv
l₁ l₂✝ l₂ l : List α
s : l <+ l₂
⊢ length l < length l₂ → ∃ a, a :: l <+~ l₂
induction' s with l₁ l₂ a s IH _ _ b _ IH <;> intro h
no goals
case slnil
α : Type uu
β : Type vv
l₁ l₂✝ l₂ l : List α
h : length [] < length []
⊢ ∃ a, [a] <+~ []
cases h
case cons.inl
α : Type uu
β : Type vv
l₁✝ l₂✝¹ l₂✝ l l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : length l₁ < length l₂ → ∃ a, a :: l₁ <+~ l₂
h✝ : length l₁ < length (a :: l₂)
h : length l₁ < length l₂
⊢ ∃ a_1, a_1 :: l₁ <+~ a :: l₂

case cons.inr
α : Type uu
β : Type vv
l₁✝ l₂✝¹ l₂✝ l l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : length l₁ < length l₂ → ∃ a, a :: l₁ <+~ l₂
h✝ : length l₁ < length (a :: l₂)
h : length l₁ = length l₂
⊢ ∃ a_1, a_1 :: l₁ <+~ a :: l₂
case cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ l₂✝ l l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : length l₁ < length l₂ → ∃ a, a :: l₁ <+~ l₂
h : length l₁ < length (a :: l₂)
⊢ ∃ a_1, a_1 :: l₁ <+~ a :: l₂
cases' lt_or_eq_of_le (Nat.le_of_lt_succ h : length l₁ ≤ length l₂) with h h
no goals
case cons.inl
α : Type uu
β : Type vv
l₁✝ l₂✝¹ l₂✝ l l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : length l₁ < length l₂ → ∃ a, a :: l₁ <+~ l₂
h✝ : length l₁ < length (a :: l₂)
h : length l₁ < length l₂
⊢ ∃ a_1, a_1 :: l₁ <+~ a :: l₂
exact (IH h).imp fun a s => s.trans (sublist_cons _ _).subperm
no goals
case cons.inr
α : Type uu
β : Type vv
l₁✝ l₂✝¹ l₂✝ l l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : length l₁ < length l₂ → ∃ a, a :: l₁ <+~ l₂
h✝ : length l₁ < length (a :: l₂)
h : length l₁ = length l₂
⊢ ∃ a_1, a_1 :: l₁ <+~ a :: l₂
exact ⟨a, s.eq_of_length h ▸ Subperm.refl _⟩
no goals
case cons₂
α : Type uu
β : Type vv
l₁ l₂✝¹ l₂ l l₁✝ l₂✝ : List α
b : α
a✝ : l₁✝ <+ l₂✝
IH : length l₁✝ < length l₂✝ → ∃ a, a :: l₁✝ <+~ l₂✝
h : length (b :: l₁✝) < length (b :: l₂✝)
⊢ ∃ a, a :: b :: l₁✝ <+~ b :: l₂✝
exact (IH <| Nat.lt_of_succ_lt_succ h).imp fun a s =>
    (swap _ _ _).subperm_right.1 <| (subperm_cons _).2 s