Theorem: List.isInfix_first_match (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
have ⟨s, t, heq⟩ := h
State after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
cases hinf: List.isInfixOf l₁ (s ++ dropLast l₁) with
| true => 
  simp [List.isInfixOf_ext] at hinf
  have _ : length s + (length l₁ - 1) < length l₂ := by 
    rw[← heq]
    simp only [length_append, length_dropLast, tsub_le_iff_right, ge_iff_le, append_assoc, add_lt_add_iff_left]
    apply Nat.lt_add_right
    apply Nat.sub_lt
    . apply Nat.pos_of_ne_zero
      simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, hne, not_false_iff]
    . simp only
  
  have  ⟨s₁, ih⟩  := List.isInfix_first_match _ _ hinf hne
  exists s₁
  apply And.intro
  . rw [← heq]
    apply isPrefix_trans ih.left
    exists (l₁.lastN 1) ++ t
    rw [dropLast_eq_take, lastN, Nat.pred_eq_sub_one]
    simp only [tsub_le_iff_right, ge_iff_le, append_assoc, append_cancel_left_eq]
    rw [← append_assoc, List.take_append_drop (length l₁ - 1) l₁]
    
  . exact ih.right
| false =>
  exists s
  apply And.intro
  . exists t
  . simp only [←isInfixOf_ext, hinf, not_false_iff]
State after:
no goals

State before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = true
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
simp [List.isInfixOf_ext] at hinf
State after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁

State before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
have _ : length s + (length l₁ - 1) < length l₂ := by 
  rw[← heq]
  simp only [length_append, length_dropLast, tsub_le_iff_right, ge_iff_le, append_assoc, add_lt_add_iff_left]
  apply Nat.lt_add_right
  apply Nat.sub_lt
  . apply Nat.pos_of_ne_zero
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, hne, not_false_iff]
  . simp only
State after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁

State before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
have  ⟨s₁, ih⟩  := List.isInfix_first_match _ _ hinf hne
State after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁

State before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
exists s₁
State after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁

State before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
Tactic:
apply And.intro
State after:
case true.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂

case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁

State before:
case true.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂

case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁
Tactic:
. rw [← heq]
  apply isPrefix_trans ih.left
  exists (l₁.lastN 1) ++ t
  rw [dropLast_eq_take, lastN, Nat.pred_eq_sub_one]
  simp only [tsub_le_iff_right, ge_iff_le, append_assoc, append_cancel_left_eq]
  rw [← append_assoc, List.take_append_drop (length l₁ - 1) l₁]
State after:
case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁

State before:
case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁
Tactic:
. exact ih.right
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length s + (length l₁ - 1) < length l₂
Tactic:
rw[← heq]
State after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length s + (length l₁ - 1) < length (s ++ l₁ ++ t)

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length s + (length l₁ - 1) < length (s ++ l₁ ++ t)
Tactic:
simp only [length_append, length_dropLast, tsub_le_iff_right, ge_iff_le, append_assoc, add_lt_add_iff_left]
State after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁ + length t

State before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁ + length t
Tactic:
apply Nat.lt_add_right
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁
Tactic:
apply Nat.sub_lt
State after:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < length l₁

case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1

State before:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < length l₁

case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1
Tactic:
. apply Nat.pos_of_ne_zero
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, hne, not_false_iff]
State after:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1

State before:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1
Tactic:
. simp only
State after:
no goals

State before:
case false
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
exists s
State after:
case false
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁

State before:
case false
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
apply And.intro
State after:
case false.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂

case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁

State before:
case false.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂

case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
. exists t
State after:
case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁

State before:
case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
. simp only [←isInfixOf_ext, hinf, not_false_iff]
State after:
no goals