Theorem: List.isInfix_drop_of_isInfix_append (One.lean)

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

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
have l₁split := List.take_append_drop (length l₂) l₁
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ l₁ ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ l₁ ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
rw [← l₁split] at ih
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
apply_fun List.drop (length l₂) at ih
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) (s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t) = drop (length l₂) (l₂ ++ l₃)
⊢ drop (length l₂) l₁ <:+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) (s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t) = drop (length l₂) (l₂ ++ l₃)
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
simp only [take_append_drop, drop_append_eq_append_drop, ge_iff_le, tsub_le_iff_right,
drop_length, le_refl, tsub_eq_zero_of_le, nil_append, List.drop, List.length_append, Nat.sub_add_eq] at ih
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂) l₁ <:+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
suffices drop (length l₂ - length s) l₁ <:+: l₃ by
  apply List.isInfix_trans _ this
  apply List.drop_isInfix_drop
  apply Nat.sub_le
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂ - length s) l₁ <:+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂ - length s) l₁ <:+: l₃
Tactic:
exists (drop (length l₂) s), (drop (length l₂ - length s - length l₁) t)
State after:
no goals

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
apply List.isInfix_trans _ this
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ drop (length l₂) l₁ <:+: drop (length l₂ - length s) l₁

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ drop (length l₂) l₁ <:+: drop (length l₂ - length s) l₁
Tactic:
apply List.drop_isInfix_drop
State after:
case h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ length l₂ ≥ length l₂ - length s

State before:
case h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ length l₂ ≥ length l₂ - length s
Tactic:
apply Nat.sub_le
State after:
no goals