internlm/Lean-Github huggingface dataset:
Theorem: List.splitOnList_intercalate
Proof state before:
case cons.h
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)

case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
. intro e ein
  apply h
  subst h₂
  simp_all only [find?, mem_cons, ne_eq, not_false_iff, or_true, implies_true, forall_const, forall_true_left,
    forall_eq_or_imp]
Proof state after:
case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Theorem: List.splitOnList_intercalate
Proof state before:
case cons.h₂
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ tail ≠ []

case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
. simp only [h₂, ne_eq, not_false_iff]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Theorem: List.splitOnList_intercalate
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : List α
tail : List (List α)
h₂✝ : head :: tail ≠ []
dhead : α
dtail : List α
ih :
  (∀ (e : List α), e ∈ tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)) →
    tail ≠ [] → splitOnList (dhead :: dtail) (intercalate (dhead :: dtail) tail) = tail
h : ∀ (e : List α), e ∈ head :: tail → ¬dhead :: dtail <:+: e ++ dropLast (dhead :: dtail)
mid : List α
tail₂ : List (List α)
h₂ : tail = mid :: tail₂
⊢ ¬dhead :: dtail <:+: head ++ dropLast (dhead :: dtail)
Tactic:
. intro contr
  apply h head
  apply List.mem_cons_self
  exact contr
Proof state after:
no goals
Theorem: convIf.id
Proof state before:
α : Sort u_1
P : Prop
inst : Decidable P
a : α
⊢ a = convIf P inst (fun x => a) fun x => a
Tactic:
simp[convIf]
Proof state after:
no goals
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
elf : List ℤ
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
Tactic:
if hempty: elf = [] then
  intro contr
  have contr := List.isInfix_length contr
  simp only [List.length_cons, List.length_singleton, elfToString, hempty,
    List.map] at contr
else
  unfold elfToString
  intro contr
  apply List.not_isInfix_intercalate_by_element  ['\n', '\n']  ['\n'] (List.map Int.reprΔ elf)
  . simp only [List.mem_map', forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro a _ contr₂
    cases List.isInfix_append_split_right contr₂ with
    | inl h₁ =>
      cases List.isInfix_append_split_left h₁ with
      | inl h₂ =>
        have h₃ := List.isInfix_drop_of_isInfix_append h₂
        simp only [List.drop, List.singleton_isInfix_iff_mem] at h₃
        apply Int.not_newline_mem_reprΔ h₃
      | inr h₄ =>
        simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero,
          List.singleton_append, List.lastN_one_eq_getLast, List.take, List.length,List.getLast?_cons] at h₄
        rw [Option.to_list_some] at h₄
        have newline_in_repr := List.isInfix_take_of_isInfix_append h₄
        simp only [List.take, List.singleton_isInfix_iff_mem, List.mem_singleton] at newline_in_repr
        rw [List.getLastD_ne_nil] at newline_in_repr
        apply Int.not_newline_mem_reprΔ (n:=a)
        rw [newline_in_repr]
        apply List.getLast_mem
        apply Int.reprΔ_ne_nil a
    | inr h₅ =>
      have hlen := List.isInfix_length h₅
      simp only at hlen
  . simp only
  . simp only [ne_eq, List.map_eq_nil, hempty, not_false_iff]
  . apply List.isInfix_append_right_of_isInfix 
    apply List.isInfix_append_left_of_isInfix 
    exact contr
Proof state after:
no goals
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
elf : List ℤ
hempty : elf = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
Tactic:
intro contr
Proof state after:
elf : List ℤ
hempty : elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
elf : List ℤ
hempty : elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
⊢ False
Tactic:
have contr := List.isInfix_length contr
Proof state after:
elf : List ℤ
hempty : elf = []
contr✝ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
contr : List.length [Char.ofNat 10, Char.ofNat 10] ≤ List.length (elfToString elf)
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
elf : List ℤ
hempty : elf = []
contr✝ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
contr : List.length [Char.ofNat 10, Char.ofNat 10] ≤ List.length (elfToString elf)
⊢ False
Tactic:
simp only [List.length_cons, List.length_singleton, elfToString, hempty,
  List.map] at contr
Proof state after:
no goals
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
elf : List ℤ
hempty : ¬elf = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
Tactic:
unfold elfToString
Proof state after:
elf : List ℤ
hempty : ¬elf = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
elf : List ℤ
hempty : ¬elf = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
Tactic:
intro contr
Proof state after:
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ False
Tactic:
apply List.not_isInfix_intercalate_by_element  ['\n', '\n']  ['\n'] (List.map Int.reprΔ elf)
Proof state after:
case h
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ ∀ (e : List Char),
    e ∈ List.map Int.reprΔ elf → ¬[Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ e ++ [Char.ofNat 10]

case hlen
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.length [Char.ofNat 10, Char.ofNat 10] ≤ 1 + List.length [Char.ofNat 10]

case hne_nil
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.map Int.reprΔ elf ≠ []

case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ ∀ (e : List Char),
    e ∈ List.map Int.reprΔ elf → ¬[Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ e ++ [Char.ofNat 10]

case hlen
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.length [Char.ofNat 10, Char.ofNat 10] ≤ 1 + List.length [Char.ofNat 10]

case hne_nil
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.map Int.reprΔ elf ≠ []

case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Tactic:
. simp only [List.mem_map', forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro a _ contr₂
  cases List.isInfix_append_split_right contr₂ with
  | inl h₁ =>
    cases List.isInfix_append_split_left h₁ with
    | inl h₂ =>
      have h₃ := List.isInfix_drop_of_isInfix_append h₂
      simp only [List.drop, List.singleton_isInfix_iff_mem] at h₃
      apply Int.not_newline_mem_reprΔ h₃
    | inr h₄ =>
      simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero,
        List.singleton_append, List.lastN_one_eq_getLast, List.take, List.length,List.getLast?_cons] at h₄
      rw [Option.to_list_some] at h₄
      have newline_in_repr := List.isInfix_take_of_isInfix_append h₄
      simp only [List.take, List.singleton_isInfix_iff_mem, List.mem_singleton] at newline_in_repr
      rw [List.getLastD_ne_nil] at newline_in_repr
      apply Int.not_newline_mem_reprΔ (n:=a)
      rw [newline_in_repr]
      apply List.getLast_mem
      apply Int.reprΔ_ne_nil a
  | inr h₅ =>
    have hlen := List.isInfix_length h₅
    simp only at hlen
Proof state after:
case hlen
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.length [Char.ofNat 10, Char.ofNat 10] ≤ 1 + List.length [Char.ofNat 10]

case hne_nil
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.map Int.reprΔ elf ≠ []

case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case hlen
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.length [Char.ofNat 10, Char.ofNat 10] ≤ 1 + List.length [Char.ofNat 10]

case hne_nil
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.map Int.reprΔ elf ≠ []

case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Tactic:
. simp only
Proof state after:
case hne_nil
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.map Int.reprΔ elf ≠ []

case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case hne_nil
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ List.map Int.reprΔ elf ≠ []

case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Tactic:
. simp only [ne_eq, List.map_eq_nil, hempty, not_false_iff]
Proof state after:
case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case a
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) ++ [Char.ofNat 10]
Tactic:
. apply List.isInfix_append_right_of_isInfix 
  apply List.isInfix_append_left_of_isInfix 
  exact contr
Proof state after:
no goals
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.inl
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
⊢ False
Tactic:
cases List.isInfix_append_split_left h₁ with
| inl h₂ =>
  have h₃ := List.isInfix_drop_of_isInfix_append h₂
  simp only [List.drop, List.singleton_isInfix_iff_mem] at h₃
  apply Int.not_newline_mem_reprΔ h₃
| inr h₄ =>
  simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero,
    List.singleton_append, List.lastN_one_eq_getLast, List.take, List.length,List.getLast?_cons] at h₄
  rw [Option.to_list_some] at h₄
  have newline_in_repr := List.isInfix_take_of_isInfix_append h₄
  simp only [List.take, List.singleton_isInfix_iff_mem, List.mem_singleton] at newline_in_repr
  rw [List.getLastD_ne_nil] at newline_in_repr
  apply Int.not_newline_mem_reprΔ (n:=a)
  rw [newline_in_repr]
  apply List.getLast_mem
  apply Int.reprΔ_ne_nil a
Proof state after:
no goals
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.inl.inl
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a
⊢ False
Tactic:
have h₃ := List.isInfix_drop_of_isInfix_append h₂
Proof state after:
case h.inl.inl
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a
h₃ : List.drop (List.length [Char.ofNat 10]) [Char.ofNat 10, Char.ofNat 10] <:+: Int.reprΔ a
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.inl.inl
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a
h₃ : List.drop (List.length [Char.ofNat 10]) [Char.ofNat 10, Char.ofNat 10] <:+: Int.reprΔ a
⊢ False
Tactic:
simp only [List.drop, List.singleton_isInfix_iff_mem] at h₃
Proof state after:
case h.inl.inl
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a
h₃ : Char.ofNat 10 ∈ Int.reprΔ a
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.inl.inl
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a
h₃ : Char.ofNat 10 ∈ Int.reprΔ a
⊢ False
Tactic:
apply Int.not_newline_mem_reprΔ h₃
Proof state after:
no goals
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.inl.inr
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₄ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [Char.ofNat 10, Char.ofNat 10] - 1) ([Char.ofNat 10] ++ Int.reprΔ a) ++
      List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
⊢ False
Tactic:
simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero,
  List.singleton_append, List.lastN_one_eq_getLast, List.take, List.length,List.getLast?_cons] at h₄
Proof state after:
case h.inl.inr
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₄ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    Option.toList (some (List.getLastD (Int.reprΔ a) (Char.ofNat 10))) ++ [Char.ofNat 10]
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.inl.inr
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₄ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    Option.toList (some (List.getLastD (Int.reprΔ a) (Char.ofNat 10))) ++ [Char.ofNat 10]
⊢ False
Tactic:
rw [Option.to_list_some] at h₄
Proof state after:
case h.inl.inr
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: [List.getLastD (Int.reprΔ a) (Char.ofNat 10)] ++ [Char.ofNat 10]
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.inl.inr
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: [List.getLastD (Int.reprΔ a) (Char.ofNat 10)] ++ [Char.ofNat 10]
⊢ False
Tactic:
have newline_in_repr := List.isInfix_take_of_isInfix_append h₄
Proof state after:
case h.inl.inr
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
a : ℤ
a✝ : a ∈ elf
contr₂ : [Char.ofNat 10, Char.ofNat 10] <:+: [Char.ofNat 10] ++ Int.reprΔ a ++ [Char.ofNat 10]
h₁ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    [Char.ofNat 10] ++ Int.reprΔ a ++ List.take (List.length [Char.ofNat 10, Char.ofNat 10] - 1) [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: [List.getLastD (Int.reprΔ a) (Char.ofNat 10)] ++ [Char.ofNat 10]
newline_in_repr :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    [List.getLastD (Int.reprΔ a) (Char.ofNat 10)]
⊢ False