Theorem: List.isPrefix_trans (One.lean)

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

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

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

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