Theorem: List.isPrefix_append (One.lean)

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

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂ ∧ drop (length l₂) l₁ <+: l₃
Tactic:
apply And.intro
State after:
case left
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂

case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃

State before:
case left
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂

case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃
Tactic:
. apply_fun take (length l₂) at heq
  simp only [take_append_eq_append_take, tsub_le_iff_right, ge_iff_le, take_length, Nat.sub_self, zero_le,
    nonpos_iff_eq_zero, le_refl, tsub_eq_zero_of_le, append_nil, take] at heq
  conv => right; rw [← heq]
  apply isPrefix_self_append
State after:
case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃

State before:
case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃
Tactic:
. apply_fun drop (length l₂) at heq
  simp only [drop_append_eq_append_drop, tsub_le_iff_right, ge_iff_le, drop_length, Nat.sub_self, zero_le,
    nonpos_iff_eq_zero, le_refl, tsub_eq_zero_of_le, nil_append, drop] at heq
  conv => right; rw [← heq]
  apply isPrefix_self_append
State after:
no goals