Theorem: List.isInfix_trans (One.lean)

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

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

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

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

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