Theorem: List.isPrefix_of_append_isPrefix_append (One.lean)

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
⊢ l₂ <+: l₃
Tactic:
have ⟨t, heq⟩ := h
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₁ ++ l₂ ++ t = l₁ ++ l₃
⊢ l₂ <+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₁ ++ l₂ ++ t = l₁ ++ l₃
⊢ l₂ <+: l₃
Tactic:
simp only [append_assoc, append_cancel_left_eq] at heq
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₂ ++ t = l₃
⊢ l₂ <+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₂ ++ t = l₃
⊢ l₂ <+: l₃
Tactic:
exact ⟨t, heq⟩
State after:
no goals