Theorem: List.isInfix_append_right_of_isInfix (One.lean)

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

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

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

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