Theorem: newline_not_last_elfToString (One.lean)

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

State before:
elf : List ℤ
hnil : elf = []
⊢ List.getLast? (elfToString elf) ≠ some (Char.ofNat 10)
Tactic:
simp only [hnil, ne_eq]
State after:
no goals

State before:
elf : List ℤ
hnil : ¬elf = []
⊢ List.getLast? (elfToString elf) ≠ some (Char.ofNat 10)
Tactic:
unfold elfToString
State after:
elf : List ℤ
hnil : ¬elf = []
⊢ List.getLast? (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)) ≠ some (Char.ofNat 10)

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

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

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

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

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

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