Theorem: List.isPostfix_append_of_isPostfix (One.lean)

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

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₁ <:+ l₃ ++ l₂
Tactic:
rw [← heq]
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₁ <:+ l₃ ++ (s ++ l₁)

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₁ <:+ l₃ ++ (s ++ l₁)
Tactic:
exists l₃ ++ s
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₃ ++ s ++ l₁ = l₃ ++ (s ++ l₁)

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₃ ++ s ++ l₁ = l₃ ++ (s ++ l₁)
Tactic:
rw [append_assoc]
State after:
no goals