Theorem: List.not_isInfix_intercalate_by_element
Proof 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]
Proof 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₁