Theorem: double_newline_not_isInfix_stringToElf (One.lean)

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
State after:
no goals

State before:
elf : List ℤ
hempty : elf = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
Tactic:
intro contr
State after:
elf : List ℤ
hempty : elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
⊢ False

State before:
elf : List ℤ
hempty : elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
⊢ False
Tactic:
have contr := List.isInfix_length contr
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

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
State after:
no goals

State before:
elf : List ℤ
hempty : ¬elf = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString elf
Tactic:
unfold elfToString
State after:
elf : List ℤ
hempty : ¬elf = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)

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
State after:
elf : List ℤ
hempty : ¬elf = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)
⊢ False

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)
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]

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
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]

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
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]

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]
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]

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
State after:
no goals

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
State after:
no goals

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₂
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

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₃
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

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₃
State after:
no goals

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₄
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

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₄
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

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₄
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

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
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

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
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 ≠ []

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)
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 ≠ []

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
⊢ 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:
rw [newline_in_repr]
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
⊢ 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 ≠ []

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
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 ≠ []

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
State after:
no goals

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₅
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

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
State after:
no goals