case nil
h : { data := [] } ≠ ""
⊢ toList { data := [] } = head { data := [] } :: toList (drop { data := [] } 1)

case cons
head✝ : Char
tail✝ : List Char
h : { data := head✝ :: tail✝ } ≠ ""
⊢ toList { data := head✝ :: tail✝ } = head { data := head✝ :: tail✝ } :: toList (drop { data := head✝ :: tail✝ } 1)
s : List Char
h : { data := s } ≠ ""
⊢ toList { data := s } = head { data := s } :: toList (drop { data := s } 1)
cases s
no goals
case nil
h : { data := [] } ≠ ""
⊢ toList { data := [] } = head { data := [] } :: toList (drop { data := [] } 1)
simp only at h
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ toList { data := c :: cs } = head { data := c :: cs } :: toList (drop { data := c :: cs } 1)
case cons
head✝ : Char
tail✝ : List Char
h : { data := head✝ :: tail✝ } ≠ ""
⊢ toList { data := head✝ :: tail✝ } = head { data := head✝ :: tail✝ } :: toList (drop { data := head✝ :: tail✝ } 1)
rename_i c cs
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ c = head { data := c :: cs } ∧ cs = (drop { data := c :: cs } 1).data
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ toList { data := c :: cs } = head { data := c :: cs } :: toList (drop { data := c :: cs } 1)
simp only [toList, List.cons.injEq]
no goals
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ c = head { data := c :: cs } ∧ cs = (drop { data := c :: cs } 1).data
constructor <;> [rfl; simp [drop_eq]]