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

Proof state:
case cons.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
l₂ : List α
a : α
l₁ : List α
ih : ∀ {r : List α}, l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
r₁ : List α
h₁ : a ∈ r₁
s₁ s₂ : List α
h₂ : l₁ ++ l₂ <+ s₁ ++ s₂
t₁ : l₁ <+ s₁
t₂ : l₂ <+ s₂
⊢ [a] ++ l₁ <+ r₁ ++ s₁

Tactic:
exact Sublist.append (by simpa) t₁

Result:
no goals

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

Tactic:
exact Sublist.append h₁ h₂

Result:
no goals

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
intro w

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

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

Tactic:
constructor

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

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

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

Tactic:
rintro ⟨r₁, r₂, rfl, h₁, h₂⟩

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

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

Tactic:
exact sublist_append_of_sublist_right w₂

Result:
no goals

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

Tactic:
rw [cons_append, cons_sublist_iff]

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

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

Tactic:
rw [← singleton_append]

Result:
case cons.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
l₂ : List α
a : α
l₁ : List α
ih : ∀ {r : List α}, l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
r₁ : List α
h₁ : a ∈ r₁
s₁ s₂ : List α
h₂ : l₁ ++ l₂ <+ s₁ ++ s₂
t₁ : l₁ <+ s₁
t₂ : l₂ <+ s₂
⊢ [a] ++ l₁ <+ r₁ ++ s₁

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

Tactic:
rintro ⟨r₁, r₂, rfl, -, w₂⟩

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

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

Tactic:
rintro ⟨r₁, r₂, rfl, h₁, h₂⟩

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

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

Tactic:
refine ⟨r₁ ++ s₁, s₂, by simp, ?_, t₂⟩

Result:
case cons.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
l₂ : List α
a : α
l₁ : List α
ih : ∀ {r : List α}, l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
r₁ : List α
h₁ : a ∈ r₁
s₁ s₂ : List α
h₂ : l₁ ++ l₂ <+ s₁ ++ s₂
t₁ : l₁ <+ s₁
t₂ : l₂ <+ s₂
⊢ a :: l₁ <+ r₁ ++ s₁

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

Tactic:
obtain ⟨s₁, s₂, rfl, t₁, t₂⟩ := ih.1 h₂

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

Proof state:
α : Type u_1
l₂ : List α
a : α
l₁ : List α
ih : ∀ {r : List α}, l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
r₁ : List α
h₁ : a ∈ r₁
s₁ s₂ : List α
h₂ : l₁ ++ l₂ <+ s₁ ++ s₂
t₁ : l₁ <+ s₁
t₂ : l₂ <+ s₂
⊢ [a] <+ r₁

Tactic:
simpa

Result:
no goals

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

Tactic:
simp only [nil_append]

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
constructor

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

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

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

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

Result:
no goals