internlm/Lean-Github huggingface dataset:
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]
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
Tactic:
simp only [List.take, List.singleton_isInfix_iff_mem, List.mem_singleton] at newline_in_repr
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 : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (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]
newline_in_repr : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
⊢ False
Tactic:
rw [List.getLastD_ne_nil] at newline_in_repr
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✝ : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
newline_in_repr : Char.ofNat 10 = List.getLast (Int.reprΔ a) ?h.inl.inr
⊢ False

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 : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
⊢ Int.reprΔ a ≠ []
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]
newline_in_repr✝ : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
newline_in_repr : Char.ofNat 10 = List.getLast (Int.reprΔ a) ?h.inl.inr
⊢ False

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 : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
⊢ Int.reprΔ a ≠ []
Tactic:
apply Int.not_newline_mem_reprΔ (n:=a)
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✝ : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
newline_in_repr : Char.ofNat 10 = List.getLast (Int.reprΔ a) ?h.inl.inr
⊢ Char.ofNat 10 ∈ Int.reprΔ a

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 : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
⊢ Int.reprΔ a ≠ []
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]
newline_in_repr : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
⊢ Int.reprΔ a ≠ []

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 : Char.ofNat 10 = List.getLastD (Int.reprΔ a) (Char.ofNat 10)
⊢ Int.reprΔ a ≠ []
Tactic:
apply Int.reprΔ_ne_nil a
Proof state after:
no goals
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.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]
⊢ False
Tactic:
have hlen := List.isInfix_length h₅
Proof state after:
case h.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]
hlen : List.length [Char.ofNat 10, Char.ofNat 10] ≤ List.length [Char.ofNat 10]
⊢ False
Theorem: double_newline_not_isInfix_stringToElf
Proof state before:
case h.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]
hlen : List.length [Char.ofNat 10, Char.ofNat 10] ≤ List.length [Char.ofNat 10]
⊢ False
Tactic:
simp only at hlen
Proof state after:
no goals
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
⊢ List.getLast? (elfToString elf) ≠ some (Char.ofNat 10)
Tactic:
if hnil: elf = [] then
  simp only [hnil, ne_eq]
else
  unfold elfToString
  intro contr
  have h₂ := List.getLast?_some contr
  rw [List.getLast_intercalate] at h₂
  . simp only [List.getLast_map _ hnil] at h₂
    revert h₂
    generalize_proofs hnil'
    intro h₂
    have mem := List.getLast_mem hnil'
    rw [h₂] at mem
    apply Int.not_newline_mem_reprΔ
    apply mem
  . intro contr
    have gl := List.getLast?_some contr
    rw [List.getLast_map] at gl
    apply Int.reprΔ_ne_nil
    apply gl
    apply hnil
  . exact '\n'
Proof state after:
no goals
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
hnil : elf = []
⊢ List.getLast? (elfToString elf) ≠ some (Char.ofNat 10)
Tactic:
simp only [hnil, ne_eq]
Proof state after:
no goals
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
hnil : ¬elf = []
⊢ List.getLast? (elfToString elf) ≠ some (Char.ofNat 10)
Tactic:
unfold elfToString
Proof state after:
elf : List ℤ
hnil : ¬elf = []
⊢ List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) ≠ some (Char.ofNat 10)
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
hnil : ¬elf = []
⊢ List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) ≠ some (Char.ofNat 10)
Tactic:
intro contr
Proof state after:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
⊢ False
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
⊢ False
Tactic:
have h₂ := List.getLast?_some contr
Proof state after:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ False
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ False
Tactic:
rw [List.getLast_intercalate] at h₂
Proof state after:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂✝ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
h₂ :
  List.getLast (List.getLast (List.map Int.reprΔ elf) (_ : List.map Int.reprΔ elf = [] → False))
      (_ : List.getLast (List.map Int.reprΔ elf) (_ : List.map Int.reprΔ elf = [] → False) = [] → False) =
    Char.ofNat 10
⊢ False

case not_nil
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ List.getLast? (List.map Int.reprΔ elf) ≠ some []

elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ Char
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂✝ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
h₂ :
  List.getLast (List.getLast (List.map Int.reprΔ elf) (_ : List.map Int.reprΔ elf = [] → False))
      (_ : List.getLast (List.map Int.reprΔ elf) (_ : List.map Int.reprΔ elf = [] → False) = [] → False) =
    Char.ofNat 10
⊢ False

case not_nil
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ List.getLast? (List.map Int.reprΔ elf) ≠ some []

elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ Char
Tactic:
. simp only [List.getLast_map _ hnil] at h₂
  revert h₂
  generalize_proofs hnil'
  intro h₂
  have mem := List.getLast_mem hnil'
  rw [h₂] at mem
  apply Int.not_newline_mem_reprΔ
  apply mem
Proof state after:
case not_nil
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ List.getLast? (List.map Int.reprΔ elf) ≠ some []

elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ Char
Theorem: newline_not_last_elfToString
Proof state before:
case not_nil
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ List.getLast? (List.map Int.reprΔ elf) ≠ some []

elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ Char
Tactic:
. intro contr
  have gl := List.getLast?_some contr
  rw [List.getLast_map] at gl
  apply Int.reprΔ_ne_nil
  apply gl
  apply hnil
Proof state after:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ Char
Theorem: newline_not_last_elfToString
Proof state before:
elf : List ℤ
hnil : ¬elf = []
contr : List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) = some (Char.ofNat 10)
h₂ :
  List.getLast (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf))
      (_ : ¬List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf) = []) =
    Char.ofNat 10
⊢ Char
Tactic:
. exact '\n'
Proof state after:
no goals
Theorem: stringToElf_ignoresTrailing
Proof state before:
s : List Char
⊢ stringToElf (s ++ [Char.ofNat 10]) = stringToElf s
Tactic:
simp only [stringToElf, ne_eq, decide_not, List.find?, List.not_mem_nil, beq_iff_eq, IsEmpty.forall_iff,
  forall_const, List.splitOn_last, List.filter_append, decide_True, Bool.not_true, not_false_iff,
  List.filter_cons_of_neg, List.filter_nil, List.append_nil]
Proof state after:
no goals
Theorem: List.intercalate_singleton
Proof state before:
α : Type u_1
sep elem : List α
⊢ intercalate sep [elem] = elem
Tactic:
rw [List.intercalate, List.intersperse_singleton, List.join_cons, List.join_nil, List.append_nil]
Proof state after:
no goals
Theorem: elfToString_roundtrip
Proof state before:
elf : List ℤ
⊢ stringToElf (elfToString elf) = elf
Tactic:
if h:elf = [] then
  simp only [h]
else
  unfold stringToElf elfToString
  rw [List.splitOn_intercalate, List.filter_eq_self.2, List.map_map]
  . unfold Function.comp
    simp only [String.toIntΔ_inv_IntreprΔ, List.map_id'']
  . simp only [List.mem_map', ne_eq, decide_not, Bool.not_eq_true', decide_eq_false_iff_not, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂, Int.reprΔ_ne_nil, not_false_iff, implies_true, forall_const]
  . simp only [List.mem_map', forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro a _
    apply Int.not_newline_mem_reprΔ
  . simp only [ne_eq, List.map_eq_nil, h, not_false_iff]
Proof state after:
no goals
Theorem: elfToString_roundtrip
Proof state before:
elf : List ℤ
h : elf = []
⊢ stringToElf (elfToString elf) = elf
Tactic:
simp only [h]
Proof state after:
no goals
Theorem: elfToString_roundtrip
Proof state before:
elf : List ℤ
h : ¬elf = []
⊢ stringToElf (elfToString elf) = elf
Tactic:
unfold stringToElf elfToString
Proof state after:
elf : List ℤ
h : ¬elf = []
⊢ List.map String.toIntΔ
      (List.filter (fun x => decide (x ≠ []))
        (List.splitOn (Char.ofNat 10) (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)))) =
    elf
Theorem: elfToString_roundtrip
Proof state before:
elf : List ℤ
h : ¬elf = []
⊢ List.map String.toIntΔ
      (List.filter (fun x => decide (x ≠ []))
        (List.splitOn (Char.ofNat 10) (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)))) =
    elf
Tactic:
rw [List.splitOn_intercalate, List.filter_eq_self.2, List.map_map]
Proof state after:
elf : List ℤ
h : ¬elf = []
⊢ List.map (String.toIntΔ ∘ Int.reprΔ) elf = elf

elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Theorem: elfToString_roundtrip
Proof state before:
elf : List ℤ
h : ¬elf = []
⊢ List.map (String.toIntΔ ∘ Int.reprΔ) elf = elf

elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. unfold Function.comp
  simp only [String.toIntΔ_inv_IntreprΔ, List.map_id'']
Proof state after:
elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Theorem: elfToString_roundtrip
Proof state before:
elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. simp only [List.mem_map', ne_eq, decide_not, Bool.not_eq_true', decide_eq_false_iff_not, forall_exists_index,
    and_imp, forall_apply_eq_imp_iff₂, Int.reprΔ_ne_nil, not_false_iff, implies_true, forall_const]
Proof state after:
case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Theorem: elfToString_roundtrip
Proof state before:
case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. simp only [List.mem_map', forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro a _
  apply Int.not_newline_mem_reprΔ
Proof state after:
case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Theorem: elfToString_roundtrip
Proof state before:
case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. simp only [ne_eq, List.map_eq_nil, h, not_false_iff]
Proof state after:
no goals
Theorem: elves_roundtrip
Proof 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
Proof state after:
no goals
Theorem: elves_roundtrip
Proof state before:
case nil

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