-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem append_sublist_of_sublist_right {xs ys zs : List α} (h : zs <+ ys) :
    xs ++ ys <+ zs ↔ xs = [] ∧ ys = zs

Proof state:
α : Type u_1
xs ys zs : List α
h : zs <+ ys
⊢ xs ++ ys <+ zs ↔ xs = [] ∧ ys = zs

Tactic:
constructor

Result:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
⊢ xs ++ ys <+ zs → xs = [] ∧ ys = zs

case mpr
α : Type u_1
xs ys zs : List α
h : zs <+ ys
⊢ xs = [] ∧ ys = zs → xs ++ ys <+ zs

Proof state:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : xs.length + ys.length ≤ zs.length
⊢ xs = [] ∧ ys = zs

Tactic:
have : xs.length = 0 := by omega

Result:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : xs.length + ys.length ≤ zs.length
this : xs.length = 0
⊢ xs = [] ∧ ys = zs

Proof state:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
⊢ xs = [] ∧ ys = zs

Tactic:
have hl' := h'.length_le

Result:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : (xs ++ ys).length ≤ zs.length
⊢ xs = [] ∧ ys = zs

Proof state:
case mpr
α : Type u_1
xs ys zs : List α
h : zs <+ ys
⊢ xs = [] ∧ ys = zs → xs ++ ys <+ zs

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case mpr.intro
α : Type u_1
ys : List α
h : ys <+ ys
⊢ [] ++ ys <+ ys

Proof state:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : xs.length + ys.length ≤ zs.length
this : xs.length = 0
⊢ xs = [] ∧ ys = zs

Tactic:
simp_all only [Nat.zero_add, length_eq_zero, true_and, append_nil]

Result:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : [] ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : ys.length ≤ zs.length
this : xs = []
⊢ ys = zs

Proof state:
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : xs.length + ys.length ≤ zs.length
⊢ xs.length = 0

Tactic:
omega

Result:
no goals

Proof state:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : [] ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : ys.length ≤ zs.length
this : xs = []
⊢ ys = zs

Tactic:
exact Sublist.eq_of_length_le h' hl

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
ys : List α
h : ys <+ ys
⊢ [] ++ ys <+ ys

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
⊢ xs = [] ∧ ys = zs

Tactic:
have hl := h.length_le

Result:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
⊢ xs = [] ∧ ys = zs

Proof state:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : (xs ++ ys).length ≤ zs.length
⊢ xs = [] ∧ ys = zs

Tactic:
simp only [length_append] at hl'

Result:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
hl : zs.length ≤ ys.length
hl' : xs.length + ys.length ≤ zs.length
⊢ xs = [] ∧ ys = zs

Proof state:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
⊢ xs ++ ys <+ zs → xs = [] ∧ ys = zs

Tactic:
intro h'

Result:
case mp
α : Type u_1
xs ys zs : List α
h : zs <+ ys
h' : xs ++ ys <+ zs
⊢ xs = [] ∧ ys = zs