Theorem: elves_roundtrip (One.lean)

State before:
elves : List (List ℤ)
⊢ stringToElves (elvesToString elves) = elves
Tactic:
induction elves with
| nil => simp only
| cons hd tail ih =>
  unfold elvesToString stringToElves
  cases tail with
  | nil =>
    simp only [beq_iff_eq, List.map, List.intercalate_singleton, ite_false, List.append_eq_nil, and_false]
    rw [List.splitOnList_nonmatching, List.map_singleton, stringToElf_ignoresTrailing, elfToString_roundtrip]
    intro contr
    cases List.isInfix_append_split_left contr with
    | inl h₁ =>
      apply double_newline_not_isInfix_stringToElf hd h₁
    | inr h₂ =>
      simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero] at h₂
      have newline_in_elf := List.isInfix_take_of_isInfix_append h₂
      simp only [List.take, List.length_nil, zero_add, ge_iff_le, List.lastN_one_eq_getLast,List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_def] at newline_in_elf
      apply newline_not_last_elfToString _ newline_in_elf  
  | cons mid tl =>
    simp only [beq_iff_eq, List.map, List.map_eq_nil, IsEmpty.forall_iff,
      List.join, ite_false, List.append_eq_nil, and_false, List.intercalate]
    rw [List.append_assoc, List.append_assoc, ← List.append_assoc, List.splitOnList_progress, List.map_append, 
      List.map_singleton, elfToString_roundtrip, List.singleton_append, ←ih, stringToElves, elvesToString, List.intercalate]
    . simp only [List.map_eq_nil, beq_iff_eq, List.map, ite_false, List.append_eq_nil, and_false]
    . simp only [List.dropLast]
      intro contr
      cases List.isInfix_append_split_left contr with
      | inl h₃ =>
        apply double_newline_not_isInfix_stringToElf hd
        apply h₃
      | inr h₄ =>
        simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero, List.length_nil] at h₄
        have last_contains := List.isInfix_take_of_isInfix_append h₄
        simp only [List.take, ge_iff_le, List.lastN_one_eq_getLast, List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_iff] at last_contains
        apply newline_not_last_elfToString _ last_contains
State after:
no goals

State before:
case nil

⊢ stringToElves (elvesToString []) = []
Tactic:
simp only
State after:
no goals

State before:
case cons
hd : List ℤ
tail : List (List ℤ)
ih : stringToElves (elvesToString tail) = tail
⊢ stringToElves (elvesToString (hd :: tail)) = hd :: tail
Tactic:
unfold elvesToString stringToElves
State after:
case cons
hd : List ℤ
tail : List (List ℤ)
ih : stringToElves (elvesToString tail) = tail
⊢ (if
        ((if (hd :: tail == []) = true then []
            else
              List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if (hd :: tail == []) = true then []
          else
            List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]))) =
    hd :: tail

State before:
case cons
hd : List ℤ
tail : List (List ℤ)
ih : stringToElves (elvesToString tail) = tail
⊢ (if
        ((if (hd :: tail == []) = true then []
            else
              List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if (hd :: tail == []) = true then []
          else
            List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]))) =
    hd :: tail
Tactic:
cases tail with
| nil =>
  simp only [beq_iff_eq, List.map, List.intercalate_singleton, ite_false, List.append_eq_nil, and_false]
  rw [List.splitOnList_nonmatching, List.map_singleton, stringToElf_ignoresTrailing, elfToString_roundtrip]
  intro contr
  cases List.isInfix_append_split_left contr with
  | inl h₁ =>
    apply double_newline_not_isInfix_stringToElf hd h₁
  | inr h₂ =>
    simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero] at h₂
    have newline_in_elf := List.isInfix_take_of_isInfix_append h₂
    simp only [List.take, List.length_nil, zero_add, ge_iff_le, List.lastN_one_eq_getLast,List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_def] at newline_in_elf
    apply newline_not_last_elfToString _ newline_in_elf  
| cons mid tl =>
  simp only [beq_iff_eq, List.map, List.map_eq_nil, IsEmpty.forall_iff,
    List.join, ite_false, List.append_eq_nil, and_false, List.intercalate]
  rw [List.append_assoc, List.append_assoc, ← List.append_assoc, List.splitOnList_progress, List.map_append, 
    List.map_singleton, elfToString_roundtrip, List.singleton_append, ←ih, stringToElves, elvesToString, List.intercalate]
  . simp only [List.map_eq_nil, beq_iff_eq, List.map, ite_false, List.append_eq_nil, and_false]
  . simp only [List.dropLast]
    intro contr
    cases List.isInfix_append_split_left contr with
    | inl h₃ =>
      apply double_newline_not_isInfix_stringToElf hd
      apply h₃
    | inr h₄ =>
      simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero, List.length_nil] at h₄
      have last_contains := List.isInfix_take_of_isInfix_append h₄
      simp only [List.take, ge_iff_le, List.lastN_one_eq_getLast, List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_iff] at last_contains
      apply newline_not_last_elfToString _ last_contains
State after:
no goals

State before:
case cons.nil
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ (if
        ((if ([hd] == []) = true then []
            else List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString [hd]) ++ [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if ([hd] == []) = true then []
          else List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString [hd]) ++ [Char.ofNat 10]))) =
    [hd]
Tactic:
simp only [beq_iff_eq, List.map, List.intercalate_singleton, ite_false, List.append_eq_nil, and_false]
State after:
case cons.nil
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ List.map stringToElf (List.splitOnList [Char.ofNat 10, Char.ofNat 10] (elfToString hd ++ [Char.ofNat 10])) = [hd]

State before:
case cons.nil
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ List.map stringToElf (List.splitOnList [Char.ofNat 10, Char.ofNat 10] (elfToString hd ++ [Char.ofNat 10])) = [hd]
Tactic:
rw [List.splitOnList_nonmatching, List.map_singleton, stringToElf_ignoresTrailing, elfToString_roundtrip]
State after:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]

State before:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
Tactic:
intro contr
State after:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
⊢ False

State before:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
⊢ False
Tactic:
cases List.isInfix_append_split_left contr with
| inl h₁ =>
  apply double_newline_not_isInfix_stringToElf hd h₁
| inr h₂ =>
  simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero] at h₂
  have newline_in_elf := List.isInfix_take_of_isInfix_append h₂
  simp only [List.take, List.length_nil, zero_add, ge_iff_le, List.lastN_one_eq_getLast,List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_def] at newline_in_elf
  apply newline_not_last_elfToString _ newline_in_elf
State after:
no goals

State before:
case cons.nil.h₁.inl
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₁ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ False
Tactic:
apply double_newline_not_isInfix_stringToElf hd h₁
State after:
no goals

State before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [Char.ofNat 10, Char.ofNat 10] - 1) (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Tactic:
simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero] at h₂
State after:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
⊢ False

State before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Tactic:
have newline_in_elf := List.isInfix_take_of_isInfix_append h₂
State after:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [] + 1) (elfToString hd)
⊢ False

State before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [] + 1) (elfToString hd)
⊢ False
Tactic:
simp only [List.take, List.length_nil, zero_add, ge_iff_le, List.lastN_one_eq_getLast,List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_def] at newline_in_elf
State after:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False

State before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False
Tactic:
apply newline_not_last_elfToString _ newline_in_elf
State after:
no goals

State before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ (if
        ((if (hd :: mid :: tl == []) = true then []
            else
              List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: mid :: tl)) ++
                [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if (hd :: mid :: tl == []) = true then []
          else
            List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: mid :: tl)) ++
              [Char.ofNat 10]))) =
    hd :: mid :: tl
Tactic:
simp only [beq_iff_eq, List.map, List.map_eq_nil, IsEmpty.forall_iff,
  List.join, ite_false, List.append_eq_nil, and_false, List.intercalate]
State after:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ List.map stringToElf
      (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
        (elfToString hd ++
            ([Char.ofNat 10, Char.ofNat 10] ++
              List.join
                (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl))) ++
          [Char.ofNat 10])) =
    hd :: mid :: tl

State before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ List.map stringToElf
      (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
        (elfToString hd ++
            ([Char.ofNat 10, Char.ofNat 10] ++
              List.join
                (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl))) ++
          [Char.ofNat 10])) =
    hd :: mid :: tl
Tactic:
rw [List.append_assoc, List.append_assoc, ← List.append_assoc, List.splitOnList_progress, List.map_append, 
  List.map_singleton, elfToString_roundtrip, List.singleton_append, ←ih, stringToElves, elvesToString, List.intercalate]
State after:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ hd ::
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl)) ++
            [Char.ofNat 10])) =
    hd ::
      if
          ((if (mid :: tl == []) = true then []
              else
                List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                  [Char.ofNat 10]) ==
              []) =
            true then
        []
      else
        List.map stringToElf
          (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
            (if (mid :: tl == []) = true then []
            else
              List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                [Char.ofNat 10]))

case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]

State before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ hd ::
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl)) ++
            [Char.ofNat 10])) =
    hd ::
      if
          ((if (mid :: tl == []) = true then []
              else
                List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                  [Char.ofNat 10]) ==
              []) =
            true then
        []
      else
        List.map stringToElf
          (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
            (if (mid :: tl == []) = true then []
            else
              List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                [Char.ofNat 10]))

case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]
Tactic:
. simp only [List.map_eq_nil, beq_iff_eq, List.map, ite_false, List.append_eq_nil, and_false]
State after:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]

State before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]
Tactic:
. simp only [List.dropLast]
  intro contr
  cases List.isInfix_append_split_left contr with
  | inl h₃ =>
    apply double_newline_not_isInfix_stringToElf hd
    apply h₃
  | inr h₄ =>
    simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero, List.length_nil] at h₄
    have last_contains := List.isInfix_take_of_isInfix_append h₄
    simp only [List.take, ge_iff_le, List.lastN_one_eq_getLast, List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_iff] at last_contains
    apply newline_not_last_elfToString _ last_contains
State after:
no goals

State before:
case cons.cons.inl
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₃ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ False
Tactic:
apply double_newline_not_isInfix_stringToElf hd
State after:
case cons.cons.inl
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₃ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd

State before:
case cons.cons.inl
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₃ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
Tactic:
apply h₃
State after:
no goals

State before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [Char.ofNat 10, Char.ofNat 10] - 1) (elfToString hd) ++ [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.length_nil] at h₄
State after:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
⊢ False

State before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Tactic:
have last_contains := List.isInfix_take_of_isInfix_append h₄
State after:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN 1 (elfToString hd)
⊢ False

State before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN 1 (elfToString hd)
⊢ False
Tactic:
simp only [List.take, ge_iff_le, List.lastN_one_eq_getLast, List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_iff] at last_contains
State after:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False

State before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False
Tactic:
apply newline_not_last_elfToString _ last_contains
State after:
no goals