Theorem: List.not_isInfix_intercalate_by_element (One.lean)

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
h : ∀ (e : List α), e ∈ l₂ → ¬l₁ <:+: delim ++ e ++ delim
hlen : length l₁ ≤ 1 + length delim
hne_nil : l₂ ≠ []
⊢ ¬l₁ <:+: delim ++ intercalate delim l₂ ++ delim
Tactic:
match hl: l₂ with
| [] =>  simp only [ne_eq, not_true] at hne_nil
| [elem] => 
  intro ⟨s,t, heq⟩
  simp [List.intercalate] at heq
  apply h elem (List.mem_singleton_self elem)
  simp [← heq]
  exists s, t
  simp only [append_assoc]
| head::mid::tail =>
  intro contr
  simp [intercalate, intersperse_cons_cons] at contr
  cases isInfix_split contr (length (delim ++ head ++ delim)) with
  | inl hinf=>
    rw [← append_assoc, ← append_assoc, take_left] at hinf
    apply h head ?_ hinf
    simp only [mem_cons, true_or]
  | inr hinf =>
    
    rw [length_append, length_append, add_assoc, add_assoc,
      ← append_assoc,← append_assoc, ← intercalate, drop_append_eq_append_drop, 
      drop_append_eq_append_drop, drop_length_le, length_append, Nat.sub_sub,
      Nat.add_comm (length l₁), ← Nat.add_assoc, ←Nat.sub_sub, Nat.add_sub_self_left,
      Nat.sub_sub, Nat.add_comm (length l₁),← Nat.sub_sub, length_append,length_append,
      ← Nat.sub_sub, ← Nat.sub_sub, Nat.add_assoc, Nat.add_sub_self_left, Nat.add_sub_self_left,
      Nat.add_sub_self_left] at hinf
    have not_inf := h head (by simp only [mem_cons, true_or])
    have hge: 1 ≤ length l₁ := by 
      apply Nat.succ_le_of_lt ( length_pos_of_ne_nil _)
      intro x; simp [x] at not_inf
    simp only [Nat.sub_eq_zero_of_le hge, tsub_le_iff_right, ge_iff_le, nil_append, drop] at hinf
    have tail_notin :∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim := by
      intro e ein
      apply h
      rw [mem_cons]; right; exact ein
    apply not_isInfix_intercalate_by_element l₁ delim (mid::tail) tail_notin _
    . simp only [ne_eq, not_false_iff]
    . apply isInfix_trans hinf
      exists take (length delim + 1 - length l₁) delim, []
      rw [← append_assoc, take_append_drop, append_nil, append_assoc]
    . exact hlen
    . simp [length_append, tsub_le_iff_right, ge_iff_le]
      apply Nat.le_sub_of_add_le
      rw [add_assoc]
      apply Nat.add_le_add_left
      apply Nat.add_le_add_left
      rw [add_comm]
      exact hlen
State after:
no goals

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
h : ∀ (e : List α), e ∈ [] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [] ≠ []
hl : l₂ = []
⊢ ¬l₁ <:+: delim ++ intercalate delim [] ++ delim
Tactic:
simp only [ne_eq, not_true] at hne_nil
State after:
no goals

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
⊢ ¬l₁ <:+: delim ++ intercalate delim [elem] ++ delim
Tactic:
intro ⟨s,t, heq⟩
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ l₁ ++ t = delim ++ intercalate delim [elem] ++ delim
⊢ False

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ l₁ ++ t = delim ++ intercalate delim [elem] ++ delim
⊢ False
Tactic:
simp [List.intercalate] at heq
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ False

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ False
Tactic:
apply h elem (List.mem_singleton_self elem)
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ l₁ <:+: delim ++ elem ++ delim

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ l₁ <:+: delim ++ elem ++ delim
Tactic:
simp [← heq]
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ l₁ <:+: s ++ (l₁ ++ t)

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ l₁ <:+: s ++ (l₁ ++ t)
Tactic:
exists s, t
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ s ++ l₁ ++ t = s ++ (l₁ ++ t)

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
elem : List α
h : ∀ (e : List α), e ∈ [elem] → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : [elem] ≠ []
hl : l₂ = [elem]
s t : List α
heq : s ++ (l₁ ++ t) = delim ++ (elem ++ delim)
⊢ s ++ l₁ ++ t = s ++ (l₁ ++ t)
Tactic:
simp only [append_assoc]
State after:
no goals

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
⊢ ¬l₁ <:+: delim ++ intercalate delim (head :: mid :: tail) ++ delim
Tactic:
intro contr
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ intercalate delim (head :: mid :: tail) ++ delim
⊢ False

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ intercalate delim (head :: mid :: tail) ++ delim
⊢ False
Tactic:
simp [intercalate, intersperse_cons_cons] at contr
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
⊢ False

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
⊢ False
Tactic:
cases isInfix_split contr (length (delim ++ head ++ delim)) with
| inl hinf=>
  rw [← append_assoc, ← append_assoc, take_left] at hinf
  apply h head ?_ hinf
  simp only [mem_cons, true_or]
| inr hinf =>
  
  rw [length_append, length_append, add_assoc, add_assoc,
    ← append_assoc,← append_assoc, ← intercalate, drop_append_eq_append_drop, 
    drop_append_eq_append_drop, drop_length_le, length_append, Nat.sub_sub,
    Nat.add_comm (length l₁), ← Nat.add_assoc, ←Nat.sub_sub, Nat.add_sub_self_left,
    Nat.sub_sub, Nat.add_comm (length l₁),← Nat.sub_sub, length_append,length_append,
    ← Nat.sub_sub, ← Nat.sub_sub, Nat.add_assoc, Nat.add_sub_self_left, Nat.add_sub_self_left,
    Nat.add_sub_self_left] at hinf
  have not_inf := h head (by simp only [mem_cons, true_or])
  have hge: 1 ≤ length l₁ := by 
    apply Nat.succ_le_of_lt ( length_pos_of_ne_nil _)
    intro x; simp [x] at not_inf
  simp only [Nat.sub_eq_zero_of_le hge, tsub_le_iff_right, ge_iff_le, nil_append, drop] at hinf
  have tail_notin :∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim := by
    intro e ein
    apply h
    rw [mem_cons]; right; exact ein
  apply not_isInfix_intercalate_by_element l₁ delim (mid::tail) tail_notin _
  . simp only [ne_eq, not_false_iff]
  . apply isInfix_trans hinf
    exists take (length delim + 1 - length l₁) delim, []
    rw [← append_assoc, take_append_drop, append_nil, append_assoc]
  . exact hlen
  . simp [length_append, tsub_le_iff_right, ge_iff_le]
    apply Nat.le_sub_of_add_le
    rw [add_assoc]
    apply Nat.add_le_add_left
    apply Nat.add_le_add_left
    rw [add_comm]
    exact hlen
State after:
no goals

State before:
case inl
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    take (length (delim ++ head ++ delim))
      (delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim))))
⊢ False
Tactic:
rw [← append_assoc, ← append_assoc, take_left] at hinf
State after:
case inl
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf : l₁ <:+: delim ++ head ++ delim
⊢ False

State before:
case inl
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf : l₁ <:+: delim ++ head ++ delim
⊢ False
Tactic:
apply h head ?_ hinf
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf : l₁ <:+: delim ++ head ++ delim
⊢ head ∈ head :: mid :: tail

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf : l₁ <:+: delim ++ head ++ delim
⊢ head ∈ head :: mid :: tail
Tactic:
simp only [mem_cons, true_or]
State after:
no goals

State before:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length (delim ++ head ++ delim) + 1 - length l₁)
      (delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim))))
⊢ False
Tactic:
rw [length_append, length_append, add_assoc, add_assoc,
  ← append_assoc,← append_assoc, ← intercalate, drop_append_eq_append_drop, 
  drop_append_eq_append_drop, drop_length_le, length_append, Nat.sub_sub,
  Nat.add_comm (length l₁), ← Nat.add_assoc, ←Nat.sub_sub, Nat.add_sub_self_left,
  Nat.sub_sub, Nat.add_comm (length l₁),← Nat.sub_sub, length_append,length_append,
  ← Nat.sub_sub, ← Nat.sub_sub, Nat.add_assoc, Nat.add_sub_self_left, Nat.add_sub_self_left,
  Nat.add_sub_self_left] at hinf
State after:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
have not_inf := h head (by simp only [mem_cons, true_or])
State after:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
have hge: 1 ≤ length l₁ := by 
  apply Nat.succ_le_of_lt ( length_pos_of_ne_nil _)
  intro x; simp [x] at not_inf
State after:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
simp only [Nat.sub_eq_zero_of_le hge, tsub_le_iff_right, ge_iff_le, nil_append, drop] at hinf
State after:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
have tail_notin :∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim := by
  intro e ein
  apply h
  rw [mem_cons]; right; exact ein
State after:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ False

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
apply not_isInfix_intercalate_by_element l₁ delim (mid::tail) tail_notin _
State after:
case inr.hne_nil
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ mid :: tail ≠ []

case inr.a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ l₁ <:+: delim ++ intercalate delim (mid :: tail) ++ delim

α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ length l₁ ≤ 1 + length delim

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr.hne_nil
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ mid :: tail ≠ []

case inr.a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ l₁ <:+: delim ++ intercalate delim (mid :: tail) ++ delim

α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ length l₁ ≤ 1 + length delim

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
. simp only [ne_eq, not_false_iff]
State after:
case inr.a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ l₁ <:+: delim ++ intercalate delim (mid :: tail) ++ delim

α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ length l₁ ≤ 1 + length delim

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr.a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ l₁ <:+: delim ++ intercalate delim (mid :: tail) ++ delim

α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ length l₁ ≤ 1 + length delim

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
. apply isInfix_trans hinf
  exists take (length delim + 1 - length l₁) delim, []
  rw [← append_assoc, take_append_drop, append_nil, append_assoc]
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ length l₁ ≤ 1 + length delim

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
tail_notin : ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
⊢ length l₁ ≤ 1 + length delim

case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
. exact hlen
State after:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁

State before:
case inr
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    drop (length delim + (length head + (length delim + 1)) - length l₁) (delim ++ head) ++
        drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head)) delim ++
      drop (length delim + (length head + (length delim + 1)) - length l₁ - length (delim ++ head ++ delim))
        (intercalate delim (mid :: tail) ++ delim)
⊢ length (delim ++ head) ≤ length delim + (length head + (length delim + 1)) - length l₁
Tactic:
. simp [length_append, tsub_le_iff_right, ge_iff_le]
  apply Nat.le_sub_of_add_le
  rw [add_assoc]
  apply Nat.add_le_add_left
  apply Nat.add_le_add_left
  rw [add_comm]
  exact hlen
State after:
no goals

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
⊢ head ∈ head :: mid :: tail
Tactic:
simp only [mem_cons, true_or]
State after:
no goals

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
⊢ 1 ≤ length l₁
Tactic:
apply Nat.succ_le_of_lt ( length_pos_of_ne_nil _)
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
⊢ l₁ ≠ []

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
⊢ l₁ ≠ []
Tactic:
intro x
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
x : l₁ = []
⊢ False

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
hinf :
  l₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
x : l₁ = []
⊢ False
Tactic:
simp [x] at not_inf
State after:
no goals

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
⊢ ∀ (e : List α), e ∈ mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
Tactic:
intro e ein
State after:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ ¬l₁ <:+: delim ++ e ++ delim

State before:
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ ¬l₁ <:+: delim ++ e ++ delim
Tactic:
apply h
State after:
case a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ e ∈ head :: mid :: tail

State before:
case a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ e ∈ head :: mid :: tail
Tactic:
rw [mem_cons]
State after:
case a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ e = head ∨ e ∈ mid :: tail

State before:
case a
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ e = head ∨ e ∈ mid :: tail
Tactic:
right
State after:
case a.h
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ e ∈ mid :: tail

State before:
case a.h
α : Type u_1
l₁ delim : List α
l₂ : List (List α)
hlen : length l₁ ≤ 1 + length delim
head mid : List α
tail : List (List α)
h : ∀ (e : List α), e ∈ head :: mid :: tail → ¬l₁ <:+: delim ++ e ++ delim
hne_nil : head :: mid :: tail ≠ []
hl : l₂ = head :: mid :: tail
contr : l₁ <:+: delim ++ (head ++ (delim ++ (join (intersperse delim (mid :: tail)) ++ delim)))
not_inf : ¬l₁ <:+: delim ++ head ++ delim
hge : 1 ≤ length l₁
hinf : l₁ <:+: drop (length delim + 1 - length l₁) delim ++ (intercalate delim (mid :: tail) ++ delim)
e : List α
ein : e ∈ mid :: tail
⊢ e ∈ mid :: tail
Tactic:
exact ein
State after:
no goals