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

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

Tactic:
intro h'

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

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

Tactic:
exact Sublist.eq_of_length_le h' hl

Result:
no goals

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

Tactic:
omega

Result:
no goals

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

Tactic:
have hl := h.length_le

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

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

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

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

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

Tactic:
rintro ⟨rfl, rfl⟩

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp only [length_append] at hl'

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

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

Tactic:
have hl' := h'.length_le

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

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

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

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

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

Tactic:
constructor

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

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