Theorem: List.isInfix_of_isInfix_drop (One.lean)

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

State before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop 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₁ <:+: drop n l₂
s t : List α✝
heq : s ++ l₁ ++ t = drop n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂

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

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