Theorem: List.isInfix_append_left_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₁ <:+: l₃ ++ (s ++ l₁ ++ t)

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: l₃ ++ (s ++ l₁ ++ t)
Tactic:
exists l₃ ++ s, t
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₃ ++ (s ++ l₁ ++ t)

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₃ ++ (s ++ l₁ ++ t)
Tactic:
simp only [append_assoc]
State after:
no goals