-- 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 hnc
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
h : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
⊢ 0 < utf8Len r₁ → ¬0 < utf8Len r₂

Tactic:
intro h₁ h₂

Result:
case hnc
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
h : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
h₁ : 0 < utf8Len r₁
h₂ : 0 < utf8Len r₂
⊢ False

Proof state:
case hnc
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
h : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
h₁ : 0 < utf8Len r₁
h₂ : 0 < utf8Len r₂
⊢ False

Tactic:
have : ∀ {cs}, 0 < utf8Len cs → cs ≠ [] := by rintro _ h rfl; simp at h

Result:
case hnc
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
h : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
h₁ : 0 < utf8Len r₁
h₂ : 0 < utf8Len r₂
this : ∀ {cs : List Char}, 0 < utf8Len cs → cs ≠ []
⊢ False

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 h : { byteIdx := p } < { byteIdx := stop } then
      if ({ data := l₁ ++ a :: r₁ }.get { byteIdx := p } != { data := l₂ ++ b :: r₂ }.get { byteIdx := p }) = 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 })
    else { 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:
rw [
  dif_pos <| by
    rw [hstop, ← hl₁, ← hl₂]
    refine Nat.lt_min.2 ⟨?_, ?_⟩ <;> exact Nat.lt_add_of_pos_right add_utf8Size_pos,
  show get ⟨l₁ ++ a :: r₁⟩ ⟨p⟩ = a by simp [hl₁, get_of_valid],
  show get ⟨l₂ ++ b :: r₂⟩ ⟨p⟩ = b by simp [hl₂, get_of_valid]]

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) = 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 }

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₂))
⊢ p + a.utf8Size = utf8Len (l₂ ++ [a])

Tactic:
simp [hl₂]

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

Tactic:
split

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

case isFalse
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
⊢ { 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₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
⊢ { data := l₂ ++ b :: r₂ }.get { byteIdx := p } = b

Tactic:
simp [hl₂, get_of_valid]

Result:
no goals

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 (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).fst + a.utf8Size) }

Tactic:
subst b

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 }
      ({ data := l₁ ++ a :: r₁ }.next { byteIdx := p }) =
    { byteIdx := p + (utf8Len (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).fst + a.utf8Size) }