Theorem: List.isInfix_append_split_right (One.lean)

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
have split := List.isInfix_split h (l₂.length + (l₁.length -1))
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
if hzero: l₁.length = 0 then
    simp only [List.length_eq_zero.1 hzero, length_nil, ge_iff_le, tsub_eq_zero_of_le, append_nil, nil_isInfix, or_self]
else
  cases split with
  | inl h₁ =>
    left
    rw [List.take_append] at h₁
    exact h₁
  | inr h₂ =>
    right
    rw [add_assoc, Nat.sub_add_cancel, Nat.add_sub_cancel, ←Nat.add_zero l₂.length, List.drop_append, List.drop] at h₂
    . exact h₂
    . rw [Nat.succ_le_iff, Nat.pos_iff_ne_zero]
      exact hzero
State after:
no goals

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
hzero : length l₁ = 0
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
simp only [List.length_eq_zero.1 hzero, length_nil, ge_iff_le, tsub_eq_zero_of_le, append_nil, nil_isInfix, or_self]
State after:
no goals

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
cases split with
| inl h₁ =>
  left
  rw [List.take_append] at h₁
  exact h₁
| inr h₂ =>
  right
  rw [add_assoc, Nat.sub_add_cancel, Nat.add_sub_cancel, ←Nat.add_zero l₂.length, List.drop_append, List.drop] at h₂
  . exact h₂
  . rw [Nat.succ_le_iff, Nat.pos_iff_ne_zero]
    exact hzero
State after:
no goals

State before:
case inl
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
left
State after:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃

State before:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
Tactic:
rw [List.take_append] at h₁
State after:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃

State before:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
Tactic:
exact h₁
State after:
no goals

State before:
case inr
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
right
State after:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₃

State before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₃
Tactic:
rw [add_assoc, Nat.sub_add_cancel, Nat.add_sub_cancel, ←Nat.add_zero l₂.length, List.drop_append, List.drop] at h₂
State after:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: l₃
⊢ l₁ <:+: l₃

case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁

State before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: l₃
⊢ l₁ <:+: l₃

case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁
Tactic:
. exact h₂
State after:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁

State before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁
Tactic:
. rw [Nat.succ_le_iff, Nat.pos_iff_ne_zero]
  exact hzero
State after:
no goals