Theorem: List.isInfix_split (One.lean)

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
have ⟨s, hPre⟩ := h
State after:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
cases append_isPrefix_split hPre n with
| inl => left; exists s
| inr => right; exists (drop (n + 1 - length l₁) s)
State after:
no goals

State before:
case inl
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : s ++ l₁ <+: take n l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
left
State after:
case inl.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : s ++ l₁ <+: take n l₂
⊢ l₁ <:+: take n l₂

State before:
case inl.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : s ++ l₁ <+: take n l₂
⊢ l₁ <:+: take n l₂
Tactic:
exists s
State after:
no goals

State before:
case inr
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
right
State after:
case inr.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
⊢ l₁ <:+: drop (n + 1 - length l₁) l₂

State before:
case inr.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
⊢ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
exists (drop (n + 1 - length l₁) s)
State after:
no goals