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
⊢ List.getLast (Int.reprΔ a) ?h.inl.inr ∈ 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 ≠ []

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 List.getLast_mem
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)
⊢ 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 ≠ []