[GOAL]
as bs : List Char
⊢ length ({ data := as } ++ { data := bs }) = length { data := as } + length { data := bs }
[PROOFSTEP]
rw [congr_append]
[GOAL]
as bs : List Char
⊢ length { data := { data := as }.data ++ { data := bs }.data } = length { data := as } + length { data := bs }
[PROOFSTEP]
simp only [String.length]
[GOAL]
as bs : List Char
⊢ List.length (as ++ bs) = List.length as + List.length bs
[PROOFSTEP]
exact List.length_append as bs
[GOAL]
n : ℕ
c : Char
⊢ length (replicate n c) = n
[PROOFSTEP]
simp only [String.length, String.replicate, List.length_replicate]
[GOAL]
l : List Char
⊢ length { data := l } = List.length l
[PROOFSTEP]
simp only [String.length]
[GOAL]
n : ℕ
c : Char
s : List Char
⊢ length (leftpad n c { data := s }) = max n (length { data := s })
[PROOFSTEP]
simp only [leftpad, String.length, List.leftpad_length]
[GOAL]
n : ℕ
c : Char
l : List Char
⊢ isPrefix (replicate (n - length { data := l }) c) (leftpad n c { data := l })
[PROOFSTEP]
simp only [isPrefix, replicate, leftpad, String.length, List.leftpad_prefix]
[GOAL]
n : ℕ
c : Char
l : List Char
⊢ isSuffix { data := l } (leftpad n c { data := l })
[PROOFSTEP]
simp only [isSuffix, replicate, leftpad, String.length, List.leftpad_suffix]
