internlm/Lean-Github huggingface dataset:
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof state after:
no goals
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof state after:
no goals
Theorem: List.not_isInfix_intercalate_by_element
Proof 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⟩
Proof 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
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof 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
Theorem: List.not_isInfix_intercalate_by_element
Proof 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)
Proof 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
Theorem: List.not_isInfix_intercalate_by_element
Proof 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]
Proof 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)
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof 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)
Theorem: List.not_isInfix_intercalate_by_element
Proof 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]
Proof state after:
no goals
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
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 ++ intercalate delim (head :: mid :: tail) ++ delim
⊢ False
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
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)))
⊢ False
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof state after:
no goals
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof 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
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
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)))
hinf : l₁ <:+: delim ++ head ++ delim
⊢ head ∈ head :: mid :: tail
Theorem: List.not_isInfix_intercalate_by_element
Proof 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]
Proof state after:
no goals
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof 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₁
Theorem: List.not_isInfix_intercalate_by_element
Proof 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])
Proof 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₁
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof 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₁
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof 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₁