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

Tactic:
simpa [← hl₁, ← Nat.add_assoc, Nat.add_right_comm] using
  firstDiffPos_loop_eq (l₁ ++ [a]) (l₂ ++ [a]) r₁ r₂ stop (p + a.utf8Size)
    (by simp [hl₁]) (by simp [hl₂]) (by simp [hstop, ← Nat.add_assoc, Nat.add_right_comm])

Result:
no goals

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₂)
x✝¹ x✝ : List Char
h : ∀ (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 }

Tactic:
rw [dif_neg] <;> simp [hstop, ← hl₁, ← hl₂, -Nat.not_lt, Nat.lt_min]

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
⊢ 0 < utf8Len r₁ → ¬0 < utf8Len r₂

Proof state:
case hnc.intro.intro.intro.intro
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 ≠ []
a : Char
as : List Char
e₁ : r₁ = a :: as
b : Char
bs : List Char
e₂ : r₂ = b :: bs
⊢ False

Tactic:
exact h _ _ _ _ e₁ e₂

Result:
no goals

Proof state:
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 }

Tactic:
next h =>
rw [dif_neg] <;> simp [hstop, ← hl₁, ← hl₂, -Nat.not_lt, Nat.lt_min]
intro h₁ h₂
have : ∀ {cs}, 0 < utf8Len cs → cs ≠ [] := by rintro _ h rfl; simp at h
obtain ⟨a, as, e₁⟩ := List.exists_cons_of_ne_nil (this h₁)
obtain ⟨b, bs, e₂⟩ := List.exists_cons_of_ne_nil (this h₂)
exact h _ _ _ _ e₁ e₂

Result:
no goals

Proof state:
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 }

Tactic:
simp

Result:
no goals

Proof state:
case hnc.intro.intro
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 ≠ []
a : Char
as : List Char
e₁ : r₁ = a :: as
⊢ False

Tactic:
obtain ⟨b, bs, e₂⟩ := List.exists_cons_of_ne_nil (this h₂)

Result:
case hnc.intro.intro.intro.intro
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 ≠ []
a : Char
as : List Char
e₁ : r₁ = a :: as
b : Char
bs : List Char
e₂ : r₂ = b :: bs
⊢ 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₁ r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (a :: r₂))
⊢ stop = min (utf8Len (l₁ ++ [a]) + utf8Len r₁) (utf8Len (l₂ ++ [a]) + utf8Len r₂)

Tactic:
simp [hstop, ← Nat.add_assoc, Nat.add_right_comm]

Result:
no goals

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₂)
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₂
⊢ ∀ {cs : List Char}, 0 < utf8Len cs → cs ≠ []

Tactic:
rintro _ h rfl

Result:
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₂
h : 0 < utf8Len []
⊢ 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₂))
⊢ { byteIdx := p } < { byteIdx := min (p + utf8Len (a :: r₁)) (p + utf8Len (b :: r₂)) }

Tactic:
refine Nat.lt_min.2 ⟨?_, ?_⟩ <;> exact Nat.lt_add_of_pos_right add_utf8Size_pos

Result:
no goals

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

Tactic:
unfold List.takeWhile₂

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