internlm/Lean-Github huggingface dataset:
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)))
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
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)
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₁
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)))
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
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 + (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 + (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
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
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]
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
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 _)
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₁ <:+:
    [] ++ drop (length delim + 1 - length l₁) delim ++ drop (1 - length l₁) (intercalate delim (mid :: tail) ++ delim)
not_inf : ¬l₁ <:+: delim ++ head ++ delim
⊢ l₁ ≠ []
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₁ <:+:
    [] ++ 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
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₁ <:+:
    [] ++ 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
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₁ <:+:
    [] ++ 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
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
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
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)
e : List α
ein : e ∈ mid :: tail
⊢ ¬l₁ <:+: delim ++ e ++ 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
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
Proof 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
Theorem: List.not_isInfix_intercalate_by_element
Proof 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]
Proof 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
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof 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
Theorem: List.not_isInfix_intercalate_by_element
Proof 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
Proof state after:
no goals
Theorem: List.isInfix_length
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ length l₁ ≤ length l₂
Tactic:
have ⟨s,t, heq⟩ := h
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ length l₁ ≤ length l₂
Theorem: List.isInfix_length
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ length l₁ ≤ length l₂
Tactic:
apply_fun @length α at heq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₂
Theorem: List.isInfix_length
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₂
Tactic:
rw [← heq]
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length (s ++ l₁ ++ t)
Theorem: List.isInfix_length
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length (s ++ l₁ ++ t)
Tactic:
rw [length_append, length_append,  add_comm (length s), add_assoc]
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₁ + (length s + length t)
Theorem: List.isInfix_length
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
s t : List α
heq : length (s ++ l₁ ++ t) = length l₂
⊢ length l₁ ≤ length l₁ + (length s + length t)
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
⊢ l₁ = l₂
Tactic:
have ⟨s, t, heq⟩ := h
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ l₁ = l₂
Tactic:
have len_sum_eq := congr_arg length heq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length (s ++ l₁ ++ t) = length l₂
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length (s ++ l₁ ++ t) = length l₂
⊢ l₁ = l₂
Tactic:
simp only [append_assoc, length_append] at len_sum_eq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length s + (length l₁ + length t) = length l₂
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length s + (length l₁ + length t) = length l₂
⊢ l₁ = l₂
Tactic:
rw [add_comm (length l₁), add_comm, add_comm (length t), add_assoc] at len_sum_eq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ l₁ = l₂
Tactic:
have len_eq : length l₁ = length l₂ := by
  apply ge_antisymm len_ge
  rw [← len_sum_eq]
  apply Nat.le_add_right
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂
Tactic:
rw [len_eq] at len_sum_eq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₂ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₂ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂
Tactic:
simp only [add_right_eq_self, zero_le, ge_iff_le, nonpos_iff_eq_zero, add_eq_zero_iff] at len_sum_eq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
⊢ l₁ = l₂
Tactic:
have ⟨teq, seq⟩ := len_sum_eq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : length s = 0
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : length s = 0
⊢ l₁ = l₂
Tactic:
rw [List.length_eq_zero] at seq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : s = []
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : s = []
⊢ l₁ = l₂
Tactic:
rw [List.length_eq_zero] at teq
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : t = []
seq : s = []
⊢ l₁ = l₂
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : t = []
seq : s = []
⊢ l₁ = l₂
Tactic:
subst_vars
Proof state after:
α : Type u_1
l₁ : List α
len_sum_eq : length [] = 0 ∧ length [] = 0
h : l₁ <:+: [] ++ l₁ ++ []
len_ge : length l₁ ≥ length ([] ++ l₁ ++ [])
len_eq : length l₁ = length ([] ++ l₁ ++ [])
⊢ l₁ = [] ++ l₁ ++ []
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ : List α
len_sum_eq : length [] = 0 ∧ length [] = 0
h : l₁ <:+: [] ++ l₁ ++ []
len_ge : length l₁ ≥ length ([] ++ l₁ ++ [])
len_eq : length l₁ = length ([] ++ l₁ ++ [])
⊢ l₁ = [] ++ l₁ ++ []
Tactic:
simp only [append_nil, nil_append]
Proof state after:
no goals
Theorem: List.eq_of_isInfix_len_ge
Proof state before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ = length l₂
Tactic:
apply ge_antisymm len_ge
Proof state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₂