-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_append_iff {l : List α} :
    l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂

Proof state:
case cons.mpr.intro.intro.intro.intro.cons₂
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₂ : List α
w₂ : l₂ <+ r₂
l₁✝ : List α
w₁ : l₁✝ <+ r₁
⊢ r :: l₁✝ ++ l₂ <+ r :: r₁ ++ r₂

Tactic:
rename_i l

Result:
case cons.mpr.intro.intro.intro.intro.cons₂
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₂ : List α
w₂ : l₂ <+ r₂
l : List α
w₁ : l <+ r₁
⊢ r :: l ++ l₂ <+ r :: r₁ ++ r₂

Proof state:
case cons.mp
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
⊢ l <+ r :: r₁ ++ r₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Tactic:
intro w

Result:
case cons.mp
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
w : l <+ r :: r₁ ++ r₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Proof state:
case cons.mp.cons₂
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁✝ : List α
w : l₁✝ <+ r₁ ++ r₂
⊢ ∃ l₁ l₂, r :: l₁✝ = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Tactic:
rename_i l

Result:
case cons.mp.cons₂
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
w : l <+ r₁ ++ r₂
⊢ ∃ l₁ l₂, r :: l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Proof state:
case cons.mp.cons₂
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
w : l <+ r₁ ++ r₂
⊢ ∃ l₁ l₂, r :: l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Tactic:
obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w

Result:
case cons.mp.cons₂.intro.intro.intro.intro
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w : l₁ ++ l₂ <+ r₁ ++ r₂
w₁ : l₁ <+ r₁
w₂ : l₂ <+ r₂
⊢ ∃ l₁_1 l₂_1, r :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ l₁_1 <+ r :: r₁ ∧ l₂_1 <+ r₂

Proof state:
case cons.mp.cons
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
w : l <+ r₁ ++ r₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Tactic:
obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w

Result:
case cons.mp.cons.intro.intro.intro.intro
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w : l₁ ++ l₂ <+ r₁ ++ r₂
w₁ : l₁ <+ r₁
w₂ : l₂ <+ r₂
⊢ ∃ l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l₁_1 <+ r :: r₁ ∧ l₂_1 <+ r₂

Proof state:
case cons.mpr
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂) → l <+ r :: r₁ ++ r₂

Tactic:
rintro ⟨l₁, l₂, rfl, w₁, w₂⟩

Result:
case cons.mpr.intro.intro.intro.intro
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w₁ : l₁ <+ r :: r₁
w₂ : l₂ <+ r₂
⊢ l₁ ++ l₂ <+ r :: r₁ ++ r₂

Proof state:
case cons.mp.cons.intro.intro.intro.intro
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w : l₁ ++ l₂ <+ r₁ ++ r₂
w₁ : l₁ <+ r₁
w₂ : l₂ <+ r₂
⊢ ∃ l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l₁_1 <+ r :: r₁ ∧ l₂_1 <+ r₂

Tactic:
exact ⟨l₁, l₂, rfl, Sublist.cons r w₁, w₂⟩

Result:
no goals

Proof state:
case cons.mpr.intro.intro.intro.intro
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w₁ : l₁ <+ r :: r₁
w₂ : l₂ <+ r₂
⊢ l₁ ++ l₂ <+ r :: r₁ ++ r₂

Tactic:
cases w₁ with
| cons _ w₁ =>
  exact Sublist.cons _ (Sublist.append w₁ w₂)
| cons₂ _ w₁ =>
  rename_i l
  exact Sublist.cons₂ _ (Sublist.append w₁ w₂)

Result:
no goals

Proof state:
case cons.mp
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
w : l <+ r :: (r₁ ++ r₂)
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Tactic:
cases w with
| cons _ w =>
  obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
  exact ⟨l₁, l₂, rfl, Sublist.cons r w₁, w₂⟩
| cons₂ _ w =>
  rename_i l
  obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
  refine ⟨r :: l₁, l₂, by simp, cons_sublist_cons.mpr w₁, w₂⟩

Result:
no goals

Proof state:
α : Type u_1
r₂ l : List α
w : l <+ [] ++ r₂
⊢ l = [] ++ l ∧ [] <+ [] ∧ l <+ r₂

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w : l₁ ++ l₂ <+ r₁ ++ r₂
w₁ : l₁ <+ r₁
w₂ : l₂ <+ r₂
⊢ r :: (l₁ ++ l₂) = r :: l₁ ++ l₂

Tactic:
simp

Result:
no goals

Proof state:
case nil.mp
α : Type u_1
r₂ l : List α
⊢ l <+ [] ++ r₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ [] ∧ l₂ <+ r₂

Tactic:
intro w

Result:
case nil.mp
α : Type u_1
r₂ l : List α
w : l <+ [] ++ r₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ [] ∧ l₂ <+ r₂

Proof state:
case nil
α : Type u_1
r₂ l : List α
⊢ l <+ [] ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ [] ∧ l₂ <+ r₂

Tactic:
constructor

Result:
case nil.mp
α : Type u_1
r₂ l : List α
⊢ l <+ [] ++ r₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ [] ∧ l₂ <+ r₂

case nil.mpr
α : Type u_1
r₂ l : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ [] ∧ l₂ <+ r₂) → l <+ [] ++ r₂

Proof state:
case cons
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
⊢ l <+ r :: r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Tactic:
constructor

Result:
case cons.mp
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
⊢ l <+ r :: r₁ ++ r₂ → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

case cons.mpr
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂) → l <+ r :: r₁ ++ r₂

Proof state:
case nil.mpr
α : Type u_1
r₂ l : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ [] ∧ l₂ <+ r₂) → l <+ [] ++ r₂

Tactic:
rintro ⟨l₁, l₂, rfl, w₁, w₂⟩

Result:
case nil.mpr.intro.intro.intro.intro
α : Type u_1
r₂ l₁ l₂ : List α
w₁ : l₁ <+ []
w₂ : l₂ <+ r₂
⊢ l₁ ++ l₂ <+ [] ++ r₂

Proof state:
case nil.mp
α : Type u_1
r₂ l : List α
w : l <+ [] ++ r₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ [] ∧ l₂ <+ r₂

Tactic:
refine ⟨[], l, by simp_all⟩

Result:
no goals

Proof state:
case nil.mpr.intro.intro.intro.intro
α : Type u_1
r₂ l₁ l₂ : List α
w₁ : l₁ <+ []
w₂ : l₂ <+ r₂
⊢ l₁ ++ l₂ <+ [] ++ r₂

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.mp.cons₂.intro.intro.intro.intro
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w : l₁ ++ l₂ <+ r₁ ++ r₂
w₁ : l₁ <+ r₁
w₂ : l₂ <+ r₂
⊢ ∃ l₁_1 l₂_1, r :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ l₁_1 <+ r :: r₁ ∧ l₂_1 <+ r₂

Tactic:
refine ⟨r :: l₁, l₂, by simp, cons_sublist_cons.mpr w₁, w₂⟩

Result:
no goals