Theorem: List.isInfix_append_split_left (One.lean)

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

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split : l₁ <:+: take (length l₂) (l₂ ++ l₃) ∨ l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
simp only [take_left, ge_iff_le]  at split
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split : l₁ <:+: l₂ ∨ l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split : l₁ <:+: l₂ ∨ l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
cases split with
| inl h₁ =>
  left; assumption
| inr h₂ =>
  right
  if hzero: l₁.length = 0 then
    simp [List.length_eq_zero.1 hzero]
  else
    rw [List.drop_append_of_le_length] at h₂
    . rw [lastN]
      convert h₂ using 3
      rw [Nat.sub_sub_eq_add_sub_of_le]
      rw [Nat.succ_le, pos_iff_ne_zero]
      apply hzero
    . simp only [ge_iff_le, tsub_le_iff_right, add_le_add_iff_left]
      rw [Nat.succ_le, pos_iff_ne_zero]
      apply hzero
State after:
no goals

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

State before:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₁ : l₁ <:+: l₂
⊢ l₁ <:+: l₂
Tactic:
assumption
State after:
no goals

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

State before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
if hzero: l₁.length = 0 then
  simp [List.length_eq_zero.1 hzero]
else
  rw [List.drop_append_of_le_length] at h₂
  . rw [lastN]
    convert h₂ using 3
    rw [Nat.sub_sub_eq_add_sub_of_le]
    rw [Nat.succ_le, pos_iff_ne_zero]
    apply hzero
  . simp only [ge_iff_le, tsub_le_iff_right, add_le_add_iff_left]
    rw [Nat.succ_le, pos_iff_ne_zero]
    apply hzero
State after:
no goals

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : length l₁ = 0
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
simp [List.length_eq_zero.1 hzero]
State after:
no goals

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

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

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) l₂ ++ l₃
hzero : ¬length l₁ = 0
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃

α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ length l₂ + 1 - length l₁ ≤ length l₂
Tactic:
. rw [lastN]
  convert h₂ using 3
  rw [Nat.sub_sub_eq_add_sub_of_le]
  rw [Nat.succ_le, pos_iff_ne_zero]
  apply hzero
State after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ length l₂ + 1 - length l₁ ≤ length l₂

State before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ length l₂ + 1 - length l₁ ≤ length l₂
Tactic:
. simp only [ge_iff_le, tsub_le_iff_right, add_le_add_iff_left]
  rw [Nat.succ_le, pos_iff_ne_zero]
  apply hzero
State after:
no goals