Theorem: List.isInfix_of_isInfix_take (One.lean)

State before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
⊢ l₁ <:+: l₂
Tactic:
rw [← List.take_append_drop n l₂]
State after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂

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

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

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