-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p)
    (hl₁ : p = utf8Len l₁) (hl₂ : p = utf8Len l₂)
    (hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)) :
    firstDiffPos.loop ⟨l₁ ++ r₁⟩ ⟨l₂ ++ r₂⟩ ⟨stop⟩ ⟨p⟩ =
      ⟨p + utf8Len (List.takeWhile₂ (· = ·) r₁ r₂).1⟩

Proof state:
case isTrue
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (a :: r₂))
⊢ firstDiffPos.loop { data := l₁ ++ a :: r₁ } { data := l₂ ++ a :: r₂ } { byteIdx := stop }
      ({ data := l₁ ++ a :: r₁ }.next { byteIdx := p }) =
    { byteIdx := p + (utf8Len (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).fst + a.utf8Size) }

Tactic:
rw [show next ⟨l₁ ++ a :: r₁⟩ ⟨p⟩ = ⟨utf8Len l₁ + a.utf8Size⟩ by simp [hl₁, next_of_valid]]

Result:
case isTrue
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (a :: r₂))
⊢ firstDiffPos.loop { data := l₁ ++ a :: r₁ } { data := l₂ ++ a :: r₂ } { byteIdx := stop }
      { byteIdx := utf8Len l₁ + a.utf8Size } =
    { byteIdx := p + (utf8Len (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).fst + a.utf8Size) }

Proof state:
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
⊢ { byteIdx := p } < { byteIdx := stop }

Tactic:
rw [hstop, ← hl₁, ← hl₂]

Result:
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
⊢ { byteIdx := p } < { byteIdx := min (p + utf8Len (a :: r₁)) (p + utf8Len (b :: r₂)) }

Proof state:
l₁ l₂ r₁ r₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)
⊢ firstDiffPos.loop { data := l₁ ++ r₁ } { data := l₂ ++ r₂ } { byteIdx := stop } { byteIdx := p } =
    {
      byteIdx :=
        p +
          utf8Len
            (match r₁, r₂ with
              | a :: as, b :: bs =>
                if decide (a = b) = true then
                  match List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) as bs with
                  | (as', bs') => (a :: as', b :: bs')
                else ([], [])
              | x, x_1 => ([], [])).fst }

Tactic:
split <;> unfold firstDiffPos.loop

Result:
case h_1
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a✝ : Char
as✝ : List Char
b✝ : Char
bs✝ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a✝ :: as✝)) (utf8Len l₂ + utf8Len (b✝ :: bs✝))
⊢ (if h : { byteIdx := p } < { byteIdx := stop } then
      if
          ({ data := l₁ ++ a✝ :: as✝ }.get { byteIdx := p } != { data := l₂ ++ b✝ :: bs✝ }.get { byteIdx := p }) =
            true then
        { byteIdx := p }
      else
        let_fun this := ⋯;
        firstDiffPos.loop { data := l₁ ++ a✝ :: as✝ } { data := l₂ ++ b✝ :: bs✝ } { byteIdx := stop }
          ({ data := l₁ ++ a✝ :: as✝ }.next { byteIdx := p })
    else { byteIdx := p }) =
    {
      byteIdx :=
        p +
          utf8Len
            (if decide (a✝ = b✝) = true then
                match List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) as✝ bs✝ with
                | (as', bs') => (a✝ :: as', b✝ :: bs')
              else ([], [])).fst }

case h_2
l₁ l₂ r₁ r₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)
x✝² x✝¹ : List Char
x✝ : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
⊢ (if h : { byteIdx := p } < { byteIdx := stop } then
      if ({ data := l₁ ++ r₁ }.get { byteIdx := p } != { data := l₂ ++ r₂ }.get { byteIdx := p }) = true then
        { byteIdx := p }
      else
        let_fun this := ⋯;
        firstDiffPos.loop { data := l₁ ++ r₁ } { data := l₂ ++ r₂ } { byteIdx := stop }
          ({ data := l₁ ++ r₁ }.next { byteIdx := p })
    else { byteIdx := p }) =
    { byteIdx := p + utf8Len ([], []).fst }

Proof state:
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (a :: r₂))
⊢ { data := l₁ ++ a :: r₁ }.next { byteIdx := p } = { byteIdx := utf8Len l₁ + a.utf8Size }

Tactic:
simp [hl₁, next_of_valid]

Result:
no goals

Proof state:
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
⊢ (if (a != b) = true then { byteIdx := p }
    else
      let_fun this := ⋯;
      firstDiffPos.loop { data := l₁ ++ a :: r₁ } { data := l₂ ++ b :: r₂ } { byteIdx := stop }
        ({ data := l₁ ++ a :: r₁ }.next { byteIdx := p })) =
    {
      byteIdx :=
        p +
          utf8Len
            (if decide (a = b) = true then
                match List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂ with
                | (as', bs') => (a :: as', b :: bs')
              else ([], [])).fst }

Tactic:
simp only [bne_iff_ne, ne_eq, ite_not, decide_eq_true_eq]

Result:
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
⊢ (if a = b then
      firstDiffPos.loop { data := l₁ ++ a :: r₁ } { data := l₂ ++ b :: r₂ } { byteIdx := stop }
        ({ data := l₁ ++ a :: r₁ }.next { byteIdx := p })
    else { byteIdx := p }) =
    {
      byteIdx :=
        p +
          utf8Len
            (if a = b then
                (a :: (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).fst,
                  b :: (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).snd)
              else ([], [])).fst }

Proof state:
case isTrue
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
h✝ : a = b
⊢ firstDiffPos.loop { data := l₁ ++ a :: r₁ } { data := l₂ ++ b :: r₂ } { byteIdx := stop }
      ({ data := l₁ ++ a :: r₁ }.next { byteIdx := p }) =
    {
      byteIdx :=
        p +
          utf8Len
            (a :: (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).fst,
                b :: (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).snd).fst }

Tactic:
simp only [utf8Len_cons]

Result:
case isTrue
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
h✝ : a = b
⊢ firstDiffPos.loop { data := l₁ ++ a :: r₁ } { data := l₂ ++ b :: r₂ } { byteIdx := stop }
      ({ data := l₁ ++ a :: r₁ }.next { byteIdx := p }) =
    { byteIdx := p + (utf8Len (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).fst + a.utf8Size) }