-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Subperm.exists_of_length_lt {l₁ l₂ : List α} (s : l₁ <+~ l₂) (h : length l₁ < length l₂) :
    ∃ a, a :: l₁ <+~ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
s : l₁ <+~ l₂
h : l₁.length < l₂.length
⊢ ∃ a, a :: l₁ <+~ l₂

Tactic:
obtain ⟨l, p, s⟩ := s

Result:
case intro.intro
α : Type u_1
l₁ l₂ : List α
h : l₁.length < l₂.length
l : List α
p : l ~ l₁
s : l <+ l₂
⊢ ∃ a, a :: l₁ <+~ l₂

Proof state:
case intro.intro.cons
α : Type u_1
l₂ l l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝.length < l₂✝.length → ∃ a, a :: l₁✝ <+~ l₂✝
h : l₁✝.length < (a :: l₂✝).length
⊢ ∃ a_1, a_1 :: l₁✝ <+~ a :: l₂✝

Tactic:
match Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h) with
| .inl h => exact (IH h).imp fun a s => s.trans (sublist_cons_self _ _).subperm
| .inr h => exact ⟨a, s.eq_of_length h ▸ .refl _⟩

Result:
no goals

Proof state:
α : Type u_1
l₂ l l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝.length < l₂✝.length → ∃ a, a :: l₁✝ <+~ l₂✝
h✝ : l₁✝.length < (a :: l₂✝).length
h : l₁✝.length = l₂✝.length
⊢ ∃ a_1, a_1 :: l₁✝ <+~ a :: l₂✝

Tactic:
exact ⟨a, s.eq_of_length h ▸ .refl _⟩

Result:
no goals

Proof state:
case intro.intro.slnil
α : Type u_1
l₂ l : List α
h : [].length < [].length
⊢ ∃ a, [a] <+~ []

Tactic:
cases h

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
l₁ l₂ : List α
h : l₁.length < l₂.length
l : List α
p : l ~ l₁
s : l <+ l₂
⊢ l.length < l₂.length → ∃ a, a :: l <+~ l₂

Tactic:
clear h p l₁

Result:
case intro.intro
α : Type u_1
l₂ l : List α
s : l <+ l₂
⊢ l.length < l₂.length → ∃ a, a :: l <+~ l₂

Proof state:
case intro.intro
α : Type u_1
l₁ l₂ : List α
h : l₁.length < l₂.length
l : List α
p : l ~ l₁
s : l <+ l₂
⊢ ∃ a, a :: l₁ <+~ l₂

Tactic:
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

Result:
case intro.intro
α : Type u_1
l₁ l₂ : List α
h : l₁.length < l₂.length
l : List α
p : l ~ l₁
s : l <+ l₂
⊢ l.length < l₂.length → ∃ a, a :: l <+~ l₂

Proof state:
α : Type u_1
l₂ l l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝.length < l₂✝.length → ∃ a, a :: l₁✝ <+~ l₂✝
h✝ : l₁✝.length < (a :: l₂✝).length
h : l₁✝.length < l₂✝.length
⊢ ∃ a_1, a_1 :: l₁✝ <+~ a :: l₂✝

Tactic:
exact (IH h).imp fun a s => s.trans (sublist_cons_self _ _).subperm

Result:
no goals

Proof state:
case intro.intro.cons₂
α : Type u_1
l₂ l l₁✝ l₂✝ : List α
b : α
a✝ : l₁✝ <+ l₂✝
IH : l₁✝.length < l₂✝.length → ∃ a, a :: l₁✝ <+~ l₂✝
h : (b :: l₁✝).length < (b :: l₂✝).length
⊢ ∃ a, a :: b :: l₁✝ <+~ b :: l₂✝

Tactic:
exact (IH <| Nat.lt_of_succ_lt_succ h).imp fun a s =>
  (swap ..).subperm_right.1 <| (subperm_cons _).2 s

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
l₂ l : List α
s : l <+ l₂
⊢ l.length < l₂.length → ∃ a, a :: l <+~ l₂

Tactic:
induction s with intro h
| slnil => cases h
| cons a s IH =>
  match Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h) with
  | .inl h => exact (IH h).imp fun a s => s.trans (sublist_cons_self _ _).subperm
  | .inr h => exact ⟨a, s.eq_of_length h ▸ .refl _⟩
| cons₂ b _ IH =>
  exact (IH <| Nat.lt_of_succ_lt_succ h).imp fun a s =>
    (swap ..).subperm_right.1 <| (subperm_cons _).2 s

Result:
no goals