no goals
a b : String
⊢ firstDiffPos a b = { byteIdx := utf8Len (List.takeWhile₂ (fun x x_1 => decide (x = x_1)) a.data b.data).fst }
simpa [firstDiffPos] using
  firstDiffPos_loop_eq [] [] a.1 b.1 ((utf8Len a.1).min (utf8Len b.1)) 0 rfl rfl (by simp)
no goals
a b : String
⊢ Nat.min (utf8Len a.data) (utf8Len b.data) = min (utf8Len [] + utf8Len a.data) (utf8Len [] + utf8Len b.data)
simp